> ## Documentation Index
> Fetch the complete documentation index at: https://docs.stateset.com/llms.txt
> Use this file to discover all available pages before exploring further.
# Formal Verification
> Machine-checked Lean 4 proofs covering the decision gate, rule engine, token matcher, and the lifting lemma — with an explicit account of what they don't cover.
# Formal Verification
Four parts of NSR carry machine-checked proofs in Lean 4: the **verified-decision outcome gate**,
the **rule engine**, the **target-binding token matcher**, and the **lifting lemma** that carries
the engine results from a ground model to the first-order engine that actually ships.
**58 theorems and supporting lemmas across four modules. Zero `sorry`.** Every proof but one is
constructive.
```bash theme={null}
formal/scripts/verify-proofs.sh
```
That checks every proof, prints each result's axiom dependencies, fails on any `sorryAx`, and fails
if any of the three exported conformance corpora has drifted from the model.
The proofs are not the interesting claim on their own — the [differential conformance
harnesses](#what-ties-the-proofs-to-the-shipped-code) are. They are what makes these theorems
statements about production rather than about a model.
## What is proved
### The outcome gate
Machine-checked properties of the decision logic:
| Property | Guarantee |
| ---------------------------------- | ----------------------------------------------------------------- |
| **Safety dominance** | A safety signal overrides every other input |
| **Deny precedence** | A fired deny beats a fired permit; deny absorbs |
| **Review outranks permit** | A review effect is not overridden by a permit |
| **No approval without grounding** | An approval requires full grounding |
| **Refuse by default** | Absent a proving rule, the outcome is `refused` |
| **Approval has a source** | An approval traces to a cited rule |
| **Cited deny never approves** | |
| **Mismatched effect is inert** | An effect that doesn't bind the request contributes nothing |
| **Target binding only downgrades** | Binding signals can never upgrade an outcome |
| **Gate totality** | The gate returns an outcome for every input — no undefined states |
### The rule engine
| Property | Guarantee |
| --------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| **Truncation under-approximates** | Stopping at `max_iterations` loses inferences but never changes ones already made |
| **Budget soundness** | Whatever the match budget cuts, every fact a budgeted pass produces is also produced by an unbudgeted pass. The budget is modelled as an *arbitrary* predicate, so a crafted join can lose inferences under load — never gain a false one |
| **Multi-tenant isolation** | If every seed fact and rule head belongs to org `o`, every derivable fact at any depth belongs to org `o`. No chaining leaks across a tenant boundary |
| **Fixpoint stability** | Once a pass adds nothing, no later pass adds anything |
| **Proof-object soundness** | Any proof passing the independent checker names a goal genuinely in the model — a verified decision's proof cannot lie |
| **Negation fails closed** | When search was truncated by depth or budget, **no** negation-as-failure step validates. A resource-exhausted engine cannot silently authorise |
| **Rule steps cite real rules** | A proof cannot cite a rule the tenant does not have |
Budget soundness and fail-closed negation are the two that matter most operationally. Together they
mean **an overloaded engine degrades into refusing, not into approving** — the failure mode you
want when the alternative is an unauthorised action.
### The token matcher
`text_mentions_target` decides whether a rule's conclusion actually refers to the thing the request
is about. It is the primitive underneath the gate's binding heuristics, so a fragment match here
would be an authorization bug.
| Property | Guarantee |
| ------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| **Never binds a fragment** | An accepted needle is one of the text's maximal word runs. `ord` cannot match `order`; `order 94` cannot match `order 941`. This is the fail-open direction — the one that decides authorization |
| **Never misses a token** | The binding guard cannot over-refuse a request that genuinely does name its target |
| **Exact characterisation** | For a non-empty alphanumeric needle, `text_mentions_target` **is** whole-token membership — not an approximation of it, equal to it |
| **A distinguishing token blocks the bind** | If a fired conclusion carries an argument with a token the request never names, the head does not bind, so the rule's effect is inert. This is exactly the `ord-9` vs `ord-4` case |
The last one is the security property. Combined with **mismatched effect is inert** on the gate, it
means a rule that fired about a *different* order contributes no signal of any polarity — it cannot
approve, and it cannot deny either.
### The lifting lemma
The engine properties above were originally proved about a **ground** model — variable-free rules.
The shipped engine runs with variables, unification, and substitutions. The lifting lemma closes
that distance.
| Property | Guarantee |
| --------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| **Matching soundness** | A successful match yields a substitution making the pattern *equal* to the fact it matched. The Rust's `Substitution` is a witness, not a guess |
| **Body-matching soundness** | Every substitution the body matcher returns grounds each body atom to a fact genuinely in the fact base |
| **The lifting lemma** | Every fact a first-order pass derives is already known, or is the head of a real ground instance of an enabled rule whose entire body is satisfied. Running with variables derives **nothing** the ground engine would not derive — so the engine results transfer to the shipped engine |
| **First-order provenance** | The engine with variables cannot invent a fact either |
| **Isolation lifts** | First-order derivation cannot cross a tenant boundary either |
This is the theorem that upgrades the engine proofs from "true about a simplified model" to "true
about what runs". Before it, multi-tenant isolation was proved only for rules without variables —
which is not the engine anyone deploys.
## Trust base
| Rests on | Meaning |
| ----------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------- |
| `propext`, `Quot.sound` | Two of Lean's three standard logical axioms — unavoidable and uncontroversial |
| `Classical.choice` | Classical logic. Used by **exactly one** theorem — the token matcher's distinguishing-token property. Every other proof is constructive |
| `Lean.ofReduceBool` | Trusts the Lean compiler's evaluation of a *closed* boolean term. Used by exactly two theorems, both regression locks on literal predicate strings |
| `sorryAx` | **Absent** — the verify script fails the build if it appears |
The verify script prints the axiom dependencies of every result, so this table is reproducible rather
than asserted.
## What ties the proofs to the shipped code
A proof about a model is decoration if nobody checks the model against the code. Three differential
harnesses replay the Lean models through the real Rust functions and assert agreement on every row:
| Harness | Corpus | Result |
| ---------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------- |
| **Gate** | 384 rows — every combination of the seven boolean signals × three answer-flag states | 384/384 agree |
| **Token matcher** | 4,719 rows — **exhaustive**: every text over `{a, b, -}` of length ≤ 4 × every non-empty needle of length ≤ 3 | 4,719/4,719 agree |
| **First-order engine** | 150 deterministically generated scenarios — knowledge bases plus safe positive Horn rules with variables, labelled with the model's saturation; 68 derive facts | 150/150 agree |
For the axes those corpora cover the models are not idealisations — they are exact descriptions of
the shipped functions, and the theorems transfer to production directly.
The token corpus's three-character alphabet is deliberate, not a shortcut: `a` and `b` are word
characters and `-` is a delimiter, so an exhaustive sweep saturates the boundary, overlapping-match
and repeated-prefix cases a hand-written suite reaches only by luck.
The verify script regenerates all three corpora and **fails if any differs from the committed
copy** — so the model and the tests cannot silently drift apart. CI runs the script and all three
harnesses on every push.
```bash theme={null}
formal/scripts/verify-proofs.sh
cargo test --lib --features postgres gate_matches_the_lean_model
cargo test --lib --features postgres text_mentions_target_matches_the_lean_model
cargo test --lib --features postgres forward_chain_matches_the_lean_model
```
## What the proofs do not cover
Two of the original gaps have since been closed and one narrowed. The rest are real, and none is
hidden inside a theorem statement.
**Closed:** the engine model is no longer ground — the lifting lemma covers variables, matching, and
substitution. **Narrowed:** the gate's binding heuristics are no longer opaque booleans — the
primitive underneath them is now characterised exactly.
1. **Backward-chaining unification is still outside the result.** The lifting lemma covers the
*forward* matching the engine uses to derive facts. Two-way unification with the occurs check
(`Unifier::unify`), used for goal/head unification in backward chaining, is not covered, and
constant↔entity-name coercion is modelled as plain constant equality. Unsafe rules — a head with
variables its body does not bind — are out of scope.
2. **Confidence is not modelled.** Rules carry an `f32` confidence multiplied along a derivation;
the model is boolean, derivable or not. Nothing here constrains confidence arithmetic or the
float comparison in proof sorting.
3. **The derivation replay is not modelled.** The token results say a wrong token blocks the bind.
They do **not** say the replay that reconstructs the fired head (`build_derivation`,
`cited_rule_ground_heads`) reconstructs the right head in the first place. The matcher is also
proved over characters, so UTF-8 byte indexing in the Rust is abstracted — the exhaustive corpus
is ASCII.
4. **Multi-conclusion rules are argued, not proved.** The Rust iterates `rule.conclusions`; the
model has a single head. Because the Rust ORs the flags across conclusions the multi-conclusion
case reduces to repeated single-conclusion rules — but that reduction is informal.
5. **Negation is absent from the lifting model.** The ground engine model *does* handle negation,
including fail-closed truncation, but the bridge to the first-order engine is proved for positive
rules only.
6. **The proof checker is Lean's, not the Rust's.** The proof-object theorems establish that the
*checking discipline* is sound. The Rust emits a flattened `Vec`; nothing proves it is
faithfully reconstructible into the tree the model's checker consumes. This is the one gap with a
clear next step — a Rust checker written against that discipline would make emitted proofs
independently verifiable end to end.
7. **Concurrency, billing, and persistence are entirely out of scope.** These proofs say nothing
about billing races, quota accounting, durability, or cross-pod rule convergence. That is a
different modelling problem — TLA+ or Kani would fit it better than Lean.
8. **Ablation switches are not modelled.** The proofs describe the production configuration; the
ablation study's alternate paths are out of scope by design.
## How to state this accurately
The precise claim, which is strong enough without overreach:
> NSR's decision gate, rule engine, token matcher, and the lifting lemma connecting them are
> **machine-checked in Lean 4** with zero `sorry`. Three differential conformance harnesses bind
> those models to the shipped Rust — the gate across its entire decision table, the token matcher
> exhaustively over a saturating alphabet, and first-order forward chaining across 150 generated
> scenarios. The engine's soundness properties, including multi-tenant isolation and fail-closed
> degradation under budget exhaustion, hold for the engine that actually runs, not only for a
> simplified model of it.
What it is **not**: an end-to-end formal verification of NSR. The proofs cover decision logic,
engine soundness, and target binding. They do not cover the neural layer, the HTTP surface,
persistence, billing, or concurrency — and the emitted proof objects are not yet independently
checkable by a Rust verifier.
## Why this is unusual
Most AI platforms offer benchmark scores. A smaller number offer audit logs. Machine-checked proofs
that an approval cannot occur without grounding — and that an overloaded engine refuses rather than
approves — is a different category of claim, because it holds for inputs nobody tested.
Paired with the [1,260-case soundness corpus](/stateset-nsr-decisions#soundness-guarantees), the
picture is: proofs for the properties that can be stated formally, adversarial testing for the rest.
## Related
* [Verified Decisions API](/stateset-nsr-decisions) — the endpoint these proofs are about
* [Policy Engine & Decision Gate](/next-temporal/policy-engine) — how the gate is used
* [Neuro-Symbolic Architecture](/stateset-nsr)