Research · Papers · Formal verification and machine-checked proof · MF-093
Formal verification of end-to-end output equality for XAGs in Lean
Lean 4.28 proves equivalence between a 30,003-gate reference hierarchy and a 20,002-gate optimized hierarchy using zero axioms
Published 2026-08-29
For everyone
Plain summary
CourtXAG is a prototype checker built in Lean for validating optimized XOR-and-AND circuits (XAGs). It takes an original circuit, an optimized circuit, a mapping between their external ports, and local proofs that modified sections behave identically. From these inputs, it produces a single formal theorem showing that whole-circuit outputs match while satisfying exact structural and cost bounds. The Lean kernel checks this theorem without assuming unproven axioms.
The prototype verified equivalence between a 30,003-gate reference circuit and a 20,002-gate optimized circuit, with replay verified in independent checker processes. It also checked a fixed scale test of 22,215 allocations and 22,215 constraints. Canary tests rejected incorrect gate costs, inverted outputs, and cyclic or backward wiring. The scope is specific: the benchmark repeats a single local rewrite hierarchically, the scale run replays a fixed envelope, and circuit parsing, flattening, port mapping, and local proof generation remain outside the verified kernel. CourtXAG extends MF-016 and makes no prior-art claims.
Result
CourtXAG compiles local equivalence proofs and an explicit port mapping into a single Lean theorem establishing end-to-end output equality alongside exact structural and cost invariants.
A self-contained Lean 4.28 implementation proves equivalence between a 30,003-gate reference hierarchy and a 20,002-gate optimized hierarchy using zero axioms. Both modules replay in independent leanchecker processes. Running on a 128 MiB worker stack, the system validates a pinned envelope of 22,215 allocations and 22,215 constraints with exact cost, balance, semantic soundness, and identity-C theorems.
Court Zero canary tests reject false costs, complemented results, and cyclic or backward gate dependencies while accepting valid local rewrites. These results validate the prototype and canary rules; they do not constitute an equivalence checker for arbitrary, unstructured 20,000-gate flat circuits.
Setting and definitions
An XAG is a logic network composed of XOR and AND gates. The reference XAG defines baseline functionality, while the optimized XAG provides the candidate implementation. The explicit port correspondence maps externally visible inputs and outputs between the two designs. Local equivalence evidence establishes functional identity across rewritten subcircuits, and end-to-end output equality proves identical input-output behavior across all matching ports.
The emitted theorem validates exact structural and cost properties, including gate count, balance, semantic soundness, and identity-C invariants within the pinned envelope. Court Zero executes structural legality checks on exported circuits. Lean 4.28 and standalone leanchecker processes provide the trusted checking environment.
Method
CourtXAG serves as a proof-carrying verification layer over existing equivalence solvers. The input bundle contains the reference XAG, the optimized XAG, the port correspondence map, and local equivalence proofs for modified regions. CourtXAG generates a Lean theorem connecting the local proofs and port mappings to global output equality and cost invariants, which the Lean kernel validates.
In the Lean 4.28 prototype, the 30,003-gate reference hierarchy was proved equivalent to the 20,002-gate optimized hierarchy without axioms, confirmed across isolated leanchecker executions. A separate scale-envelope replay verified 22,215 allocations and 22,215 constraints under exact cost, balance, semantic soundness, and identity-C invariants using a 128 MiB stack.
Court Zero canaries confirmed error detection: the checker rejected false costs, inverted outputs, and backward or cyclic gates, while admitting valid rewrites. Structural evaluation on a 4,540-product, 16-round XAG demonstrated that arbitrary 128-row linear cuts yielded a median of 2,835 imported signals, with every gate in full 128-row blocks escaping the partition boundary. Consequently, sound certificate boundaries require semantic or source-level boundaries or recovered structural equivalents.
The complete verification sources, canary test suites, structural analysis scripts, and execution receipts are available in this paper's downloadable evidence pack.
Discussion
CourtXAG provides a proof-carrying wrapper that links local equivalence certificates and explicit port correspondences to end-to-end equality and cost invariants. Extending MF-016, the entry does not introduce an independent solver algorithm and asserts no prior-art claims.
Trust boundaries remain bounded. The prototype does not evaluate arbitrary unstructured 20,000-gate pairs: the large benchmark consists of a single verified local rewrite repeated across a hierarchy, and the 22,215-row run is a replay of a pinned scale envelope. Circuit parsing, flattening passes, port-map generation, and local proof synthesis remain outside the trusted Lean kernel.
Structural analysis on the 4,540-product network explains why fixed-size linear partitioning fails and justifies certificate packaging along semantic and structural boundaries. No corrections are recorded for MF-093.
For everyone — the takeaway
What this means
CourtXAG produces a machine-checked guarantee that an optimized circuit matches its original design. By linking verified local edits to complete circuit behavior, it lets the Lean kernel confirm that whole-circuit outputs match and cost tracking is exact. Built-in checks catch corrupted costs, inverted outputs, and invalid loops. The implementation verifies a 30,003-gate to 20,002-gate comparison and a 22,215-constraint scale envelope, but it relies on repeating one verified pattern and leaves frontend parsing and proof discovery outside the checker. It builds on MF-016 without prior-art claims.
Register references
- Entry: MF-093.
- Receipt artifacts:
06-lean-certified-optimization/LocalRewrite.lean,ScaleEnvelope.lean,analyze_xag.py,benchmark-run-receipt.json,scale-envelope-receipt.json,court-zero-receipt.json,round0-structure-receipt.json,rounds16-structure-receipt.json,canaries/,run_court_zero.py. - Prior-art work: MF-016.
- Prior-art claim: the register does not record this.
Every artifact named above is bundled in, or hashed by, this paper's evidence pack below.
Evidence pack
Everything needed to check this entry against its receipts: the register text, a manifest with a SHA-256 hash for every named receipt, and 9 of 9 receipt files bundled (13 KB). Anything not bundled is still hashed in the manifest and lives in the compute-box working trees.
Changelog
Last reviewed 2026-08-29
- 2026-08-29Published on this site.