AlphaProof Code Proved Signal's Crypto Correct — at the Level of the Compiled Binary

Six and a half million lines of Lean, produced in four weeks, by agent teams that no human helped write. That is the headline number G​oogle DeepMind published on 10 November 2026 for AlphaProof Code, an agentic framework for formal verification that the lab used to machine-check the cryptographic core of the Signal protocol — and, unusually, to check it at the level of the compiled AArch64 binary rather than the design document above it. The models that did the work are a different question. one API key at provider list price with 0% markup The proof agents' engine is not something we serve.

The framework is not a model you can call. It is a harness: human experts decide what must be true, a mixture of models turns those goals into Lean specifications, and then teams of proof-writing agents — the blog names G​emini Carbon as the engine — fill in the proofs until Lean's kernel accepts them. What shipped alongside the announcement is the artifact set, at github.com/google-deepmind/code-verification, and a technical paper that is far more candid about the boundaries of the result than the blog post is. Most of what follows comes from that paper, because the paper is where the interesting numbers live.

What was actually proved, and against what

The target is libsignal v0.105.4 with spqr v1.6.0, built by stock rustc 1.98.1, statically linked against musl, and emitted as a single AArch64 Linux executable. That detail matters more than any benchmark: the proofs are about the bytes that would run on a phone, not about a Rust function that a compiler is trusted to translate faithfully. The team verified roughly 560 KB of libsignal source, about 140,000 AArch64 instructions, and they did it by writing a Lean model of the instruction set — 467 instructions and 31 system calls, in 7,578 lines — and then proving that the real ELF image, loaded and executed under that model, preserves the security properties.

The properties are the ones a protocol engineer would ask for. Ten symbolic theorems cover forward secrecy, post-compromise security, initiator and responder secrecy, authentication, and five corollaries of PQXDH's Theorem 1. The main result is named signal_session_secure_placed. There is also a computational track with a concrete bound, and the two tracks use different adversary models: the symbolic side (Dolev–Yao, via the DyLean framework) even covers a quantum attacker who breaks Diffie–Hellman after the handshake, while the computational side covers classical adversaries only.

Where the six million lines go

"Over six million lines" is the blog's phrasing and it is accurate but coarse. The paper's breakdown is the useful one, and it is worth reading as a cost table rather than a flex:

• Proofs for the binary — 5.3 million lines, the bulk of the work, covering the machine-code semantics and the refinement from the symbolic model down to the executable.

• Computational proofs — about 860,000 lines.

• Symbolic proofs — about 350,000 lines.

• Bug-refutation proofs — about 140,000 lines, for the two deliberately reintroduced vulnerabilities described below.

• Allocator proofs — about 70,000 lines.

Nearly seven million lines if you count comments and blank lines, which the paper does and the blog does not. Either way the ratio that matters is between the proof and the thing proved: 6.5 million lines of Lean to establish properties of a 560 KB binary. That ratio is the honest measure of how far this technique is from being routine, and it is the number to quote when someone asks whether formal verification has become cheap.

The trusted base is smaller than the proof, and that is the point

A proof is only as good as what it assumes. The paper is specific about this, and the specificity is what separates it from a press release. The trusted specs are about 18,000 lines (28,000 with documentation), the AArch64 semantics about 8,000, and the Lean encoding of the machine code around 95,000. Thirty-seven routines are replaced by contracts rather than verified — SHA-256 and SHA-512 compression, AES-256-CBC, X25519, the Edwards curve operations, Kyber1024 and ML-KEM-768, and libcrux HMAC. Eighteen panic entry points are likewise assumed rather than proved.

So the claim is not "everything is proved." The claim is that the cryptographic protocol logic, the session state machine, and the refinement from that logic to the instructions actually executed are proved, while the primitives underneath are trusted the way every verification project trusts its primitives. The Rust compiler, notably, is not in the trusted base — the team avoided needing to trust it by reasoning at the machine-code level, which is the same trick that lets them sidestep a verified compiler entirely. For context on scale, the paper cites seL4 at roughly 20 person-years and CompCert at about 6.

Two bugs, put back on purpose

A verification system that only ever says "correct" is untestable. So the team took two vulnerabilities that had previously been found and fixed in Signal's code — a weak-state bug and a small-subgroup bug — reintroduced them into an isolated copy, and re-ran the pipeline. In both cases AlphaProof Code produced a machine-checked proof that the buggy version fails the security theorem: the symbolic statement resolves to ¬Sec(Asm_bug).

The paper adds a caveat that a marketing page would have cut: refuting the computational theorem for those bugs is "much harder" and was left open. In other words, the negative test works cleanly on the symbolic track and does not yet work on the computational one. That is exactly the sort of asymmetry a reader should know about before treating the framework as a bug detector.

How the agents were run

Five researchers over four weeks, each running agents nonstop. The proof-writing itself was done by teams of 40 to 80 agents, running between 24 and 72 hours on a single machine per team, with a supervising agent above the team orchestrator. A gatekeeper agent checks each submission with comparator against a held-out copy of the specification and against Lean's kernel — a defence against an agent proving a subtly weakened version of what was asked.

The human work was front-loaded on specifications. Every specification was reviewed by an expert before proof work began, and the agents' own audit pass flagged about 1% of the codebase for human attention. No human wrote proof code. The paper is also blunt about the engineering: a clean build can take several hours, early on a minor source edit or a recompiled binary forced large proof repairs, and there is "substantial room for optimization" in both the AI-generated proofs and the proof techniques themselves.

What the proofs do not cover

The limitations are long enough to be the most important section of the paper, and they are stated plainly. No post-quantum guarantee is established for SPQR's healing property — the ratchet theorems assume the attacker chooses SPQR keys. Payload privacy is not proved. Responder authentication is not proved for the first message of a handshake that is never promoted. The model permits one session per promotion, fixed message lengths, no multi-device state, and trust-on-first-use identity keys.

There is also a bound that goes vacuous. The 8-byte MAC forgery term is at least 2⁻⁶⁴ per attempt and grows quadratically in messages and epochs, which means the bound stops saying anything for a single session of roughly 25,000 messages, or for 2²⁰ sessions of 2¹⁰ messages. And the subject of the proof is the team's build of libsignal-cli running as a fresh process — not the Signal app on your phone. Several environment assumptions are argued informally rather than proved.

There is no API, no price, and no model to call

This is the part that will disappoint anyone arriving from a model leaderboard. AlphaProof Code is a research framework and a published artifact set. There is no endpoint, no per-token rate card, no waitlist, and no weights: the repository contains the Lean development, the AArch64 semantics, the libsignal binding and the specifications, not a checkpoint. The blog says the artifacts are open-sourced; the landing page states no licence, which is worth checking before anyone plans to build on top of it.

The models that did the work are a different question. The paper names G​emini 4 Carbon for the proof agents and says Claude Opus 5.5 was used alongside other models for drafting and reviewing specifications. Claude Opus 5.5 is on OrcaRouter's catalogue today at $4 per million input tokens and $20 per million output, with provider list price passed through at 0% markup — so if the practical takeaway you want is "run a spec-drafting loop with the model the paper used," that part is a normal API call, and a vendor price change lands on our side the same day. The proof agents' engine is not something we serve, and nothing here implies we host AlphaProof Code itself.

Why this is a bigger deal than the Signal result

The Signal verification is impressive on its own terms — the first formal verification of a widely deployed protocol's implementation by any method, with or without AI, according to DeepMind, and the first time AI has verified a deployed cryptographic protocol at this depth. But the transferable claim is the workflow. A team of five, in four weeks, with a specification-review step and an agent gatekeeper, produced a proof corpus that would previously have been a multi-year project. If that ratio holds even loosely, the set of systems that can afford verification changes: medical device firmware, power grid software, the sort of code that currently gets a code review and a prayer.

Whether it holds is untested. Signal's crypto is unusually well specified, the team had Signal's own engineers reviewing methodology, and the primitives were contracted out rather than verified. The next system will not be so accommodating. The paper's own framing — pair formal verification with automated defence agents like CodeMender — is the honest shape of the pitch: verification tells you what is true, and something else has to fix what is not.

What to watch

Three things would move this from a landmark paper to an industrial technique. A second, independent codebase verified by someone outside G​oogle, ideally one where the specification had to be written from scratch rather than adapted from an existing analysis. A cost figure — agent-hours, accelerator-hours, dollars — because four weeks and 40-to-80-agent teams is not a unit any engineering manager can budget against. And the computational-track bug refutation, which the paper leaves open and which is the difference between a system that proves properties and a system that can also tell you, computationally, that a specific binary is broken.

Until then, read the artifact repository rather than the announcement. The proofs are there, Lean checks them, and the paper tells you exactly what they assume.