For decades, formal verification had a pricing problem. Verifying the seL4 microkernel
took roughly twenty person-years; the CompCert verified compiler took six (figures as reported in the AlphaProof Code paper). That math confined mathematical proof — the strongest assurance software can carry — to a handful of mission-critical systems. Most production systems instead depend on testing, review, static analysis, and selective formal methods.
Google DeepMind's AlphaProof Code, announced November 10, attacks the labor side of that equation. A team of AI agents, guided by human experts, produced about 6.5 million lines of machine-checked Lean proof about a dedicated AArch64 Linux executable — libsignal-cli — that wraps the unmodified libsignal v0.105.4 and spqr v1.6.0 crates, compiled with the stock Rust compiler. The campaign took about four weeks, per DeepMind's announcement.
The interesting question for enterprise architects is not whether the agents were clever. It is where the trust now sits — because AlphaProof Code does not eliminate the trust boundary in verification. It moves it, shrinks it, and makes it auditable. That is the part of this result that should change how production-readiness standards are written.
What was actually proved
Prior formal analyses of Signal verified protocol models: mathematical descriptions of the PQXDH handshake and the ratchet, separated from the code that runs in production. Models can be right while implementations are wrong, and real vulnerabilities can arise in exactly the gap between a verified protocol design and its implementation.
AlphaProof Code closed that gap for a defined scope. The theorems concern the compiled libsignal-cli binary — covering its init, send, and recv operations, with keygen excluded — and establish forward secrecy, authentication, and post-compromise security for the PQXDH handshake and Triple Ratchet in one-to-one sessions, in both the symbolic (Dolev–Yao) and computational models. One caveat belongs beside the result, not buried under it: handshake secrecy against a quantum adversary is established only in the symbolic model; the computational proof addresses classical attackers, and proves neither post-quantum healing nor multi-device security. As a control, the team reintroduced two previously fixed libsignal bugs and produced machine-checked disproofs of the symbolic security theorem for the mutated binaries — the specifications catch real defects, not just compliant code.
Two further scope limits belong in any honest summary. The theorems are about that scoped executable, not the shipping Signal phone app or every device build. And group messaging is explicitly future work; the computational setting is simplified (single sessions, fixed message lengths, no multi-device state, identity keys trusted on first use). This is a proof about Signal's core cryptography under stated conditions.
The trust boundary moved; it did not vanish
Here is the architectural core of the result. The 6.5 million lines of agent-generated proof are untrusted: nobody has to believe them, because they are checked. A gatekeeper process uses a deterministic comparator to confirm each proof establishes exactly the held-out, human-approved specification — no quietly weakened restatement — and Lean's kernel validates the proof itself.
What must be trusted is much smaller, and it is worth being precise about its shape. The headline count is about 26,000 lines: roughly 18,000 lines of specification statements and definitions, plus about 8,000 lines of AArch64 machine-code semantics. But that count is not the whole trusted computing base. Three categories of trusted model and contract sit at its center, and the full base extends beyond them:
- The specification itself. A proof is only as strong as what it states. A specification that weakens the attacker's capabilities, or asserts too little about outputs, can be "proved" of buggy code. AI agents helped draft the specifications; human experts guided, reviewed, and approved every trusted statement, and adjudicated every amendment that changed a trusted assumption. DeepMind's team hardened the specs with skeptical reviewer agents, vacuity checks, and mutation testing. But a specification's faithfulness cannot itself be machine-checked — this is a human judgment, permanently.
- The machine-code semantics. The AArch64 model must faithfully describe real hardware and the Linux kernel — something that cannot be proved, only kept small and tested hard (here, in lockstep against two independent oracles). If the semantics diverge from silicon, the proof describes a machine that does not exist.
- The contracts for what was not verified. Low-level cryptographic primitives enter the result through trusted contracts — their security is assumed (or idealized), not proved — as do some library routines the executable calls. The Lean kernel and the checking machinery themselves are also part of the trusted base. The compiler, notably, is not: because the theorems are stated over the compiled binary, a compiler bug that violated one of the specified properties, under the formal machine model, would make the proof fail rather than silently pass.
Read that list again as an architect. It is a familiar shape: a small, explicitly enumerated trusted base, surrounded by machinery that checks everything else.
AlphaProof Code's real contribution to production practice may be that it makes the trusted base legible — a substantially smaller body of specifications and semantics becomes the primary human-audit surface, even though auditing it adequately still demands expert review.
What this changes for production-readiness standards
Three implications follow, none of which require believing AI hype. (These are Decision Crafters analysis, drawn from the paper's reported results — not findings of the paper itself.)
First, "formally verified" becomes a claim that needs a scope statement, not a badge. The useful questions are the ones this paper answers well: verified what — model, source, or binary? Against which specification, drafted and approved by whom? What sits inside the trusted base, and what was assumed by contract? A vendor who cannot produce those answers has a marketing claim, not an assurance case. Architecture review boards should start asking for the trusted-base inventory the way they ask for a bill of materials.
Second, the human job in assurance shifts from writing proofs to governing specifications. DeepMind's researchers wrote no proofs; they decided scope, chose models, approved trusted statements, and judged amendments. That is a governance role, and it is the scarce skill. Organizations that want this class of assurance will not primarily need more provers — they will need engineers who can state, precisely and adversarially, what "secure" means for their system, and reviewers who can tell a strong specification from a vacuous one.
Third, the result justifies evaluating verification feasibility for systems previously out of reach — not assuming favorable economics. A four-week research campaign is a striking signal, but it is one data point: repeatability, independent reproduction, specification labor, compute cost (undisclosed), and CI integration all remain unmeasured. What changes today is that cryptographic libraries, protocol implementations, firmware, and isolation boundaries now deserve a serious feasibility question. Ordinary business logic still does not — there, the specification problem is usually "we do not actually know what this should do," and no prover can fix that.
The decision to take away
DeepMind describes this as the first verification of a widely deployed cryptographic protocol implementation at this depth, and the result earns the attention. But its most transferable lesson is not "agents can do proofs." It is that proof moves the argument, it doesn't end it — from "did we test enough?" to "is this specification the right one, and is the trusted base small enough to defend?"
That is a better argument to have. It is also an argument only humans in the room can settle. The agents generated the 6.5 million lines. The far smaller set of statements that decides whether those proofs mean anything was approved by people — and that ratio, not the headline, is the assurance question this work makes concrete.