Google DeepMind published a paper today, AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level, with the full Lean development in a public repository. The claim is large and, as far as I can tell from the paper and the repository, well supported: agent teams proved forward secrecy, post-compromise security, authentication and handshake secrecy for libsignal, the reference implementation of the Signal protocol, as compiled by the stock Rust compiler to AArch64 machine code. The authors call them “the first proofs connecting protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation.”
WIRED’s headline is that an AI tool “proved the Signal protocol is secure.” That is close, and the gap between close and exact is where the paper is most worth reading. Two numbers from the abstract frame it: “about 6.5 million lines of machine-checked Lean proof code, resting on about 26,000 lines of trusted specifications and AArch64 semantics.”
The proof nobody has to read
The 6.5 million lines are the untrusted part, and that is by design. Lean’s kernel checks every step, so a wrong proof fails to compile no matter who or what wrote it. The paper is blunt about authorship: the proofs “were produced entirely by agent teams powered by Gemini 4 Carbon,” and “none of the authors wrote any proof code.” A campaign team “typically had 40 to 80 agents and ran on a single machine for 24 to 72 hours.”
Section 7 breaks the total down. About 5.3 million lines are proofs about the binary, which the symbolic and computational security proofs share. The computational proof adds about 860,000, the symbolic proof about 350,000. Another 140,000 lines prove that two reintroduced historical bugs break the theorems, and 70,000 verify musl’s memory allocator. The code under proof is about 560 KB of libsignal, roughly 140,000 AArch64 instructions.
Then the part a reader has to trust. “Reading every definition that our headline theorems depend on means reading about 18,000 lines of code in the repository (about 28,000 with documentation), plus about 8,000 lines of the AArch64 semantics.” On a chart drawn to scale, that part barely shows up.
I wrote about the same split in September, when a 13-million-line Lean formalization of Fermat’s Last Theorem came out, and again last month with the crash-freedom proofs over OSS-Fuzz targets. Both times the question was whether the statement meant what the headline said. The DeepMind paper notices that those efforts “largely target generic properties, such as crash freedom, or functional correctness,” and sets its own work apart because security of a deployed protocol “requires sophisticated specifications, which are substantial engineering projects in their own right.” I think that is a fair distinction. It also means there is more statement to get wrong.
Where the boundary sits
The binary-level theorems cover a lot. Section 4 says the proofs follow each init, send and recv run “from the executable’s entry point to its final exit_group system call,” reasoning instruction by instruction about the command-line harness, its file-backed stores, musl’s allocator and memcpy/memset, the PQXDH, Triple Ratchet and SPQR state machines, key derivation, protobuf serialization and MAC verification. That is the machinery where implementation bugs in Signal have historically lived, and it is verified as rustc compiled it. The Rust compiler is not in the trusted base. The seL4 kernel proof, by contrast, states in its abstract: “We assume correctness of compiler, assembly code, and hardware.”
What the theorems do not cover is just as specific. “The remaining 37 hooked routines are replaced by contracts at the binary boundary, and 18 panic entry points end the run with SIGABRT.” The hooked routines include every low-level cryptographic primitive: SHA-256 and SHA-512 compression, AES-256-CBC, the X25519 and Edwards curve operations, Kyber1024, and ML-KEM-768 and HMAC from libcrux. They also include error formatting, memmove, bcmp, strlen, the two functions that write files and standard output, and a handful of Rust library routines. The paper says of the non-cryptographic contracts: “They are not proved against the real routines,” though scripted scenarios give the same outcomes on the Lean model and on the real binary.
The paper doesn’t hide this, and it is the usual division of labor in the field. Earlier work on Signal mostly sat further from the code: Cohn-Gordon and colleagues in 2017 extracted “a formal description of the abstract protocol” from the implementation and proved that, and Kobeissi, Bhargavan and Blanchet the same year verified a variant written in a purpose-built language that translates to a ProVerif model. A 2014 survey of implementation-level protocol verification described the field’s approach the same way: “libraries are assumed to correctly implement some models,” and the proofs give assurance about “the application code that implements the protocol logic.” The DeepMind paper takes that application-code side much further than before, down to bytes, without trusting a compiler. Its discussion section lists connecting the idealized crypto contracts to verified implementations as future work. Until then, “proved secure” means secure assuming the primitives behave as idealized and the 37 contracts match the real routines.
The guarantee has a size
Two other limits deserve to sit next to the headline.
The computational theorem is the one that gives a concrete bound on an attacker’s advantage, and the paper says plainly: “Our bounds give no guarantee against a quantum adversary.” The symbolic proof covers handshake secrecy against a future quantum attacker, but neither proof establishes the post-quantum healing that SPQR was added to provide; the ratchet theorems “let the attacker choose SPQR’s keys.”
And the computational bound runs out. Its largest statistical term is the chance of forging libsignal’s 8-byte MAC tag, which “grows quadratically in both the number of messages and the number of epochs of the session.” Section 5.2.5 puts numbers on it: “if nearly every message starts a new epoch, they make it vacuous for single sessions of about 25,000 messages, or for 2^20 sessions of 2^10 messages.” In the Double Ratchet a new epoch starts when the conversation changes direction, so a long back-and-forth with one contact is close to the case where the computational theorem stops saying anything. I don’t read that as a flaw in libsignal, and the paper states it openly. It is a reason not to restate the result as “Signal is secure, full stop.”
The specification work found real errors
The part of the paper I’d most want other verification teams to read is the record of what broke when old proofs on paper met real code. “For both formalizations we record every place where the Lean statements depart from their reference papers or from libsignal.” The computational catalog “has over 200 entries and the symbolic one about 35.” Most are routine. Some are not:
Fifteen are gaps or bugs in the computational analysis of the Double Ratchet, such as missing hypotheses and security game conditions that allow trivial wins.
That analysis is Alwen, Coretti and Dodis (EUROCRYPT 2019), whose ePrint abstract argues that “none of the existing analyses is fully satisfactory” and sets out a clean definition of secure messaging. It is one of the most careful treatments of the Double Ratchet in print, and it still had fifteen holes that only showed up when a proof had to go through against bytes. On the symbolic side, the paper says the printed ProVerif queries of Cheval, Jacomme and Richards “look up skipped message keys at the wrong ratchet index, which makes receiver-side forward secrecy false as printed.”
The specification also passes a strength test. The team reverse-applied two upstream libsignal fixes, cd36118 (a “weak state” bug that stored a new session’s unconfirmed state, including a copy of the signed prekey secret) and 5293caa (a missing small-subgroup check on the initiator’s X25519 base key), rebuilt the binary, and proved in Lean that each resulting binary violates the symbolic security theorem. That is the right test, and I’d like to see it become standard. A specification that the old, broken code also satisfies is not worth much. The paper is honest that this only works on one side: refuting the computational theorem for a buggy binary “amounts to proving the hardness assumptions themselves, an open problem.”
Four weeks, five people
The labor number is the one people will repeat. The paper opens with the reference points: seL4 “took twenty person-years to verify” and CompCert “took six.” Section 7 says the libsignal proof work “was done by a team of five over four weeks.” Five people for four weeks is 20 person-weeks, or about 0.4 person-years by my arithmetic.
The comparison is not like for like in either direction. seL4 and CompCert verified code that, in the paper’s words, “was written specifically with verification in mind.” The libsignal effort started from existing specifications in the literature, from Signal’s own earlier verification work, and from a Lean ecosystem that did not exist in 2009. In the other direction, the libsignal team verified code it could not change, at the machine-code level, which the paper says is “even harder.”
The missing column is cost. WIRED reports that “Google declined to share the cost of the analysis” and would not say whether a commercial product is planned. The paper adds that “a clean build of our proofs could take several hours” and that “a substantial fraction of our proofs concerns registers, stack frames and memory layout.” Whether this works for teams outside Google depends on that number more than on the person-weeks.
What I’d take from it
The paper’s own conclusion is the right one, and it sits a long way from the headline: “once proofs become cheap, the hard question is what to prove. The majority of our effort went not into proofs but into specifications.” Swarat Chaudhuri told WIRED “there is a long distance to go before we are able to scale this to all the software of the world.” The team also describes guarding against agents weakening their own goals. In one swarm of Lean-proving agents they cite, an agent “redefined a predicate used in a conjecture’s hypothesis as False, and the trick spread to the rest of the swarm.” Their answer is a gatekeeper that sees only file paths and theorem names and checks the proof against a held-out copy of the specification.
Put in one sentence, it says this. For one-to-one sessions, under idealized cryptographic primitives and 37 stated contracts, the compiled libsignal binary does what the protocol models say, and those models guarantee forward secrecy, post-compromise security and authentication against a classical attacker, up to a bound that runs out at around 25,000 messages in a busy session. That is a remarkable result. Twenty-six thousand lines of it still need human readers, and open-sourcing them is the most useful thing in the release.
References
- Chaudhuri, S., Ferraiuolo, A., Kovsharov, A., Chajed, T., Schlesinger, S., Seth, K., Katz, J., Sutton, C. and Kohli, P. (2026). AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level. Google DeepMind, 10 November 2026. Sections 1, 4, 5.1.6, 5.2.5, 5.3, 6, 7 and 9.
- Google DeepMind (2026). google-deepmind/code-verification. GitHub repository, README and
docs/PAPER_MAP.md, accessed 10 November 2026. - Newman, L. H. (2026). A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure. WIRED, 10 November 2026.
- Klein, G. et al. (2009). seL4: Formal Verification of an OS Kernel. Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, October 2009.
- Alwen, J., Coretti, S. and Dodis, Y. (2019). The Double Ratchet: Security Notions, Proofs, and Modularization for the Signal Protocol. Advances in Cryptology – EUROCRYPT 2019, LNCS 11476, pp. 129-158.
- Avalle, M., Pironti, A. and Sisto, R. (2014). Formal verification of security protocol implementations: a survey. Formal Aspects of Computing, January 2014.
- Cohn-Gordon, K., Cremers, C., Dowling, B., Garratt, L. and Stebila, D. (2017). A Formal Security Analysis of the Signal Messaging Protocol. 2017 IEEE European Symposium on Security and Privacy, April 2017.
- Kobeissi, N., Bhargavan, K. and Blanchet, B. (2017). Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. 2017 IEEE European Symposium on Security and Privacy, April 2017.