Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911741181427712 |
|---|---|
| author | Falda, Pierre |
| author_facet | Falda, Pierre |
| contents | 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 |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2606_02019 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems Falda, Pierre Logic in Computer Science Computational Engineering, Finance, and Science Emerging Technologies 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 |
| title | Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems |
| topic | Logic in Computer Science Computational Engineering, Finance, and Science Emerging Technologies |
| url | https://arxiv.org/abs/2606.02019 |