Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems
2026-06-01 • Logic in Computer Science
Logic in Computer ScienceComputational Engineering, Finance, and ScienceEmerging Technologies
AI summaryⓘ
The authors propose a new way to do formal verification by combining different proof tools instead of using just one. Their system lets proofs in one tool reference equivalent proofs in another, ensures consistency across tools, and uses AI to help search for proofs without fully trusting it. They tested this approach on parts of a high-frequency trading platform and showed it can simplify complex verification tasks significantly. This method helps verify software correctness more efficiently by working across multiple verification systems.
formal verificationproof assistantTLA+Raft consensuscross-backend citationpolyglot proof systemCI (continuous integration)algorithmic verificationhigh-frequency tradingAI proof search
Authors
Pierre Falda
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