Skip to main content

​
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.
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 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:

​
The rule engine

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.
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.
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

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: 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.

​
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<ProofStep>; 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, the picture is: proofs for the properties that can be stated formally, adversarial testing for the rest.