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

翻译：暂无翻译