要点
- On 10 November 2026, Google DeepMind published a blog by Pushmeet Kohli and Swarat Chaudhuri introducing AlphaProof Code, together with a paper, "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level."
- A team of five, over four weeks, directed agents so that teams powered by Gemini 4 Carbon wrote about 6.5 million lines of Lean proofs. Lean is a language and checker for mathematical proofs that a computer can verify. None of the authors wrote proof code. A proof was accepted only if Lean's kernel checked it.
- The statements a reader must still trust are about 18,000 lines of trusted specifications in the repository, about 28,000 with documentation, plus about 8,000 lines of AArch64 semantics, a formal account of the 64-bit ARM instruction set. The blog's claim that humans needed to review only "one percent of the codebase" does not appear in the paper, so we do not repeat it as a fact.
- The object of the proofs is unmodified libsignal v0.105.4, the Signal protocol's reference implementation, compiled with the ordinary rustc compiler to AArch64 and run in a small command-line harness. The properties concern the PQXDH handshake and the Triple Ratchet, in both the symbolic and computational models. Variants of the protocol are used in WhatsApp, Messenger, and Google Messages, but those other implementations were not verified.
- Two previously fixed libsignal bugs, small-subgroup and weak-state, first reported by Cheval, Jacomme and Richards, were put back into isolated binaries. Lean proofs show that the symbolic security theorem fails on those binaries. The computational theorem is classical, and the ratchet theorems let the attacker choose SPQR keys, so the work does not prove the post-quantum healing that the Sparse Post-Quantum Ratchet is designed to provide.
On 10 November 2026, Google DeepMind said that AI agents, guided by its researchers, had mathematically proved key security properties of the compiled code behind the Signal protocol. The blog, signed by Pushmeet Kohli and Swarat Chaudhuri, presents this as formal proofs, down to the machine code, meaning the actual processor instructions in the compiled binary, for an unmodified, widely used cryptographic implementation. The paper, "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level," is more precise, and it is the account we follow where the two disagree. The checkable claim is not that Signal, WhatsApp, or Google Messages are now unconditionally secure. It is that a team of five, over four weeks, used AlphaProof Code so Gemini 4 Carbon agents wrote about 6.5 million lines of Lean proofs, accepted only if Lean's kernel checked them, covering key properties of unmodified libsignal compiled with stock rustc to AArch64.
[1][2]What was actually proved
libsignal is the reference implementation of the Signal protocol, the end-to-end encryption design that protects conversations in the Signal app. The paper notes that variants of the protocol are also deployed in WhatsApp, Meta's Messenger, and Google Messages. DeepMind did not verify those other codebases. It linked unmodified libsignal v0.105.4, with the SPQR crate at v1.6.0, into a small command-line program, libsignal-cli, and compiled it with stock rustc to AArch64 Linux. PQXDH is Signal's current handshake, the first key agreement when two parties start a session, and it includes a post-quantum step. The Triple Ratchet is how Signal updates keys as messages are sent, combining the older Double Ratchet with the Sparse Post-Quantum Ratchet, or SPQR.
The team proved properties of those components in two standard models. In the symbolic model, cryptographic operations are treated as perfect black boxes. In the computational model, an efficient attacker's success is bounded by the hardness of the underlying mathematical problems. The paper says the proofs establish forward secrecy, meaning earlier messages stay protected if a device is later compromised; authentication; post-compromise security, meaning later messages can become protected again once new keys are exchanged; and handshake secrecy on the compiled binary. In the symbolic model, it also claims handshake secrecy against a future quantum attacker.
[1][2]Who wrote the proofs, and what must still be trusted
Humans chose the scope, approved every trusted statement, and reviewed amendments. Specifications were drafted with agents powered by Gemini 4 Carbon and Claude Opus 5.5, then approved by the authors. The proofs were produced entirely by agent teams powered by Gemini 4 Carbon. None of the authors wrote proof code.
The paper, rather than the blog's looser "over six million lines," says the repository contains nearly 7 million lines of Lean, counting blanks and comments. About 6.5 million of them are proofs: 5.3 million about the binary, shared by both security proofs, about 860,000 for the computational proof, and about 350,000 for the symbolic proof. Another 140,000 lines prove the reintroduced bugs, and 70,000 verify the memory allocator. The verified libsignal code is about 560 KB, or about 140,000 AArch64 instructions.
Lean's kernel checks the proofs. What must still be trusted is the specification: about 18,000 lines of code in the repository, about 28,000 with documentation, plus about 8,000 lines of AArch64 semantics. Those results also depend on Lean's kernel, the security of the cryptographic primitives, and contracts, meaning assumed behavior, for some hooked low-level cryptographic routines. In the computational proof, the assumptions are mostly standard, plus two joint-security assumptions, because one Curve25519 key is used both for X25519 key agreement and for XEdDSA signatures. The symbolic proofs assume perfect cryptography. The Rust compiler is not trusted: a compiler bug, or a bug in the Rust source, that broke a formalized property would make the proof fail. The blog's "one percent of the codebase" human-review claim does not appear in the paper, and we do not treat it as established.
[1][2]The bugs that were put back in
To test the specifications, the authors reintroduced two previously fixed libsignal bugs found by Cheval, Jacomme and Richards, by reverse-applying the upstream fix commits to v0.105.4 and recompiling. The small-subgroup bug left the PQXDH responder without a check that the initiator's X25519 base key was torsion-free and in range, so a replayed handshake with a mangled base key could create a second session with the same shared secret. The weak-state bug stored a new session's unconfirmed state, including a copy of the signed prekey secret, after a prekey message failed on that session but decrypted against an older one. For both, Lean proofs show that the symbolic security theorem fails on the bug-injected binary. The paper also records 15 gaps or bugs in a Double Ratchet computational analysis by Alwen, Coretti and Dodis, plus errors in the printed ProVerif queries of Cheval, Jacomme and Richards, and in a PQXDH reading by Bhargavan and colleagues.
[1][2]What the theorems do not cover
The assembly-level symbolic theorem is narrower than the model. Identity keys are already pinned, so libsignal's trust-on-first-use path, where a contact's identity key is accepted the first time it is seen, is not exercised. The harness gives two honest parties one session per session file. One-time Kyber prekeys, single-use post-quantum keys that can appear in a prekey bundle, are not covered. Side channels, and other secrets sitting in memory, are out of scope. The results concern this build of libsignal-cli, not Signal's own applications. The work does not cover group messaging, sealed sender, or server-side protocols.
The computational theorem is classical, so it gives no guarantee against a quantum adversary. As in Cheval et al., the ratchet theorems let the attacker choose the SPQR keys, and so show that the Triple Ratchet is no weaker than the Double Ratchet, not the post-quantum healing that SPQR is designed to add. Signal's chief technology officer, Ehren Kret, is quoted on the blog as saying the work gives "even greater confidence in our code's privacy guarantees." The paper thanks Signal's Rolfe Schmidt, Michael Rosenberg, and Ehren Kret for feedback on the specifications, which is not an independent audit of the proofs.
[1][2]The fair case
The fair reading starts from cost. The paper recalls that the seL4 microkernel took twenty person-years to verify, and the CompCert C compiler took six, and that those systems were written with verification in mind. Here, five people working for four weeks directed agents to produce machine-checked proofs about a widely used cryptographic library, and they showed that the symbolic theorem fails when known bugs are put back in. The honest limit sits beside that achievement. The proofs bind only the properties that were specified, on this harnessed build, under these assumptions. They still trust Lean's kernel, standard cryptographic assumptions, and contracts for some hooked routines. They do not turn Signal, or the apps that reuse variants of its protocol, into unconditionally secure software.
[1][2]Who should care, and what to watch
Anyone who ships or depends on libsignal should care, as should readers of headlines about Signal being "proved secure." The artifacts are open at https://google-deepmind.github.io/code-verification. The paper says the authors want to use the same workflow to verify new libsignal releases before they ship. In the next six months, the tests are whether independent readers audit the 18,000 trusted specification lines and find them as strong as claimed, whether later work proves the post-quantum healing that SPQR is designed to provide, and whether the method moves from libsignal-cli to the applications and features, including group messaging, that users actually run.
[1][2]Close
A small team, in a month, obtained machine-checked proofs about compiled libsignal for the properties they chose to specify. It is not a certificate that the apps sitting on phones are unconditionally secure, or that the post-quantum part of the ratchet does the healing it was designed to do. Those remain open claims, and they can now be checked against the artifacts the authors have published.
[1][2]