Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems
Pierre Falda
cs.LO
Jun 1, 2026 · v1
cs.CE cs.ET
TL;DR
Lean 4 is one of the external kernels in dual-citation gates: TLA+ obligations are re-proved in Lean 4 and Coq, and closure is checked via #print axioms in CI.
Abstract
We propose a federated architecture for production formal verification. Rather than forcing all obligations into a single proof-assistant kernel, the architecture treats a verification campaign as a polyglot proof system composed of three mechanisms: cross-backend citation discharges a TLA+ obligation by citing an equivalent theorem in a structurally distinct kernel, with build- system-level drift-resistance enforced through kernel-level closure-assertion directives; cross-axis convergence composes per-obligation verdicts across independent verifiers into operational kernel-agreement gates; the AI layer is untrusted proof-search labour inside a trusted CI envelope. We validate the architecture on two production subsystems of the Mercury high-frequency-trading platform: a Raft consensus subsystem with full algorithmic scope and a financial-arithmetic invariant layer (balance accounting, automated-market-maker curve invariants, isolated-margin, lock-tracking settlement). The validation campaign reduced a 26-axiom Raft census to zero in 17 active hours of single-session wallclock
Problem
Production formal verification of distributed consensus and financial arithmetic rarely fits within a single proof-assistant kernel. Prior Raft verifications cover limited algorithmic scope.
Approach
A federated architecture lets a TLA+ obligation be discharged by citing an equivalent theorem in a distinct kernel, such as Coq, Lean 4, Why3, Apalache, Z3 or CBMC. The build system re-checks each cited theorem on every commit using closure-assertion directives such as Lean 4 #print axioms. Verdicts from independent verifiers are composed into multi-axis agreement gates, for example dual Coq and Lean 4 citation. Untrusted AI specialist agents are dispatched in parallel waves to author the per-backend proofs inside a CI envelope.
Results
The architecture was applied to the Raft subsystem and financial-arithmetic invariant layer of the Mercury HFT platform. A 26-axiom Raft census was reduced to zero in 17 active hours, which the authors report as roughly a 60× per-axiom reduction against their prior TLAPS baseline. Across the campaign, 18 obligations converged across three to eight independent axes.
| Convergence | Count |
|---|
| 3-axis | 4 |
| 4-axis | 5 |
| 5-axis | 5 |
| 6-axis | 3 |
| 8-axis | 1 |
Cross-axis convergence counts
