AlphaProof Code: Google DeepMind's agents proved four properties of Signal's code, not the whole app

In short

• According to Google DeepMind, agents powered by Gemini 4 Carbon wrote about 6.5 million lines of Lean proofs about the machine code of libsignal 0.105.4: forward secrecy, authentication, post-compromise security, handshake secrecy [S2, p. 1 and 25].
• The humans, a team of five over four weeks, chose what to prove and approved the statements. What a reader has to read and accept comes to about 26,000 lines [S2, p. 1, 3, 25 and 27].
• Not proven: the Signal apps, group chats, the ratchet's post-quantum protection, the basic cryptographic building blocks (assumed), side channels. No cost published [S2, p. 8, 11, 19, 23 and 30].

The blog post says "Signal", the technical paper says "libsignal-cli"

I opened the PDF over coffee. Formal verification means writing down what a program must guarantee, the specification, then proving that it guarantees it in every case, instead of testing it on examples [S2, p. 1]. The proof is written in Lean, a language in which the computer checks every step (the one in which Claude agents formalized Fermat according to Anthropic: see my article on Claude Fable 5.2 and Mythos 5.2).

The exact scope: the one-to-one conversation part of libsignal, Signal's reference library, version 0.105.4 [S2, p. 9]. The team plugged it, unmodified, into a small tool, libsignal-cli, compiled into a program for AArch64 processors, the architecture of nearly all Android phones and all iPhones [S2, p. 9 and 11]. Three actions are covered: starting a session, sending, receiving. Key generation is not [S2, p. 9].

The detail that made me put my cup down: the proof is about the machine code, so a bug in the Rust compiler that broke security would make the proof fail [S2, p. 24].

Four properties proved on libsignal's machine code

Signal works in two stages: a handshake, PQXDH, in which Alice and Bob agree on a shared secret, then the Triple Ratchet, which makes a fresh key for every message [S2, p. 6 and 7].

According to the paper, the proofs establish four properties [S2, p. 1]. Forward secrecy: if someone steals your device's state today, your old messages stay unreadable. Post-compromise security: the thief is locked out at the next key exchange, as long as they stay passive during that exchange [S2, p. 7]. Authentication. And handshake secrecy. The proofs are carried out in two frameworks that don't give the same guarantees. The symbolic model assumes perfect cryptography and proves, among other things, handshake secrecy against a future quantum attacker. The computational model bounds a classical attacker's chances against the confidentiality and authenticity of messages [S2, p. 3, 8 and 12].

Humans choose the question, agents write the proof

The specifications came out of back-and-forth between the researchers and agents powered by Gemini 4 Carbon and Claude Opus 5.5, then were approved by the humans [S2, p. 25 to 27]. The proofs came entirely from teams of Gemini 4 Carbon agents: none of the authors wrote any proof code, the paper states [S2, p. 26].

The blog post speaks of over six million lines of Lean; the technical paper counts about 6.5 million for the proofs alone [S2, p. 25]. What has to be read and accepted is much shorter: about 18,000 lines of statements and definitions, plus about 8,000 lines describing the processor, how Linux runs the program and the symbol names of the compiled code, so about 26,000 lines [S2, p. 1, 3 and 5]. A team of five worked for four weeks [S2, p. 25]; each agent team typically had 40 to 80 agents, on a single machine, for 24 to 72 hours per campaign, meaning one team launch on one part of the system [S2, p. 6 and 25].

And the "1%"? According to the blog post, the agents audited the proof and flagged the areas that needed a second look by a human, "just one percent of the codebase", with Lean automatically checking the rest. The post doesn't say which codebase; the technical paper doesn't give that figure.

Ehren Kret, Signal's chief technology officer, quoted in the post: "Using AI agents to translate live code into valid Lean theorems is a major breakthrough." The blog post claims, for Google DeepMind, the first formal verification, with or without AI, of the implementation of such a widely deployed protocol. The technical paper claims something else: the first proofs of protocol-level security properties for the unmodified code of such an implementation, without qualification in its abstract, "to our knowledge" on p. 29 [S2, p. 1, 2 and 29].

The test of libsignal's two old bugs, put back in

To test their specifications, the authors put two old bugs, fixed since, back into libsignal [S2, p. 24].

The first: Bob didn't check that a key sent by Alice was well formed. The attacker flips one bit: the key is written differently but gives the same calculations, like an address written two ways. The buggy program accepts the replayed message and opens a second session with the same secret [S2, p. 24 and 25]. The second: a session-opening message that fails to decrypt in its new session is retried against older ones, and if that works, the program stores the new session anyway, with a copy of a secret key [S2, p. 24].

In both cases, Lean validated a proof that the buggy program violates the symbolic security theorem [S2, p. 24]. The computational theorem was not refuted: that would be much harder, the paper explains [S2, p. 25].

What the Signal proofs don't cover

The results concern libsignal-cli, launched as a fresh process with 1 GiB (about a billion bytes) of memory, not Signal's apps [S2, p. 12 and 23]. The verified program runs on Linux; the Android and iOS (the iPhone's operating system) apps run the same Rust code, but the result only carries over if you accept that they preserve its behavior [S2, p. 11]. Group chats and server-side protocols are left for later [S2, p. 6 and 30]. The properties are established against classical attackers; the post-quantum protection the SPQR ratchet adds after a key theft is not proved [S2, p. 3, 8 and 19].

You also have to accept the trusted computing base. 39 routines (small pieces of program that do a single task) are replaced by contracts, descriptions assumed without proof, including the low-level cryptographic building blocks [S2, p. 11]. Their strength is an assumption, not a result. Same for Lean's kernel and the description of the processor and of Linux, which cannot be proved faithful to the real hardware and is only tested [S2, p. 4, 5 and 24].

On the attacker side, side channels are out of scope [S2, p. 19]. The computational proof gives no guarantee against a quantum attacker, leaves out multi-device accounts and bars the attacker from injecting its own first message [S2, p. 8 and 23]. The symbolic proof does not rule out a loss of forward secrecy through replay, already described by other researchers [S2, p. 19]. And the computational proof's numerical guarantee says nothing anymore for a single session of about 25,000 messages, in an unfavorable scenario described by the paper [S2, p. 23].

My opinion, labeled as such: four properties of the one-to-one session code are proven, provided the assumed building blocks hold; the house around it is not.

What we don't know yet

• The price: neither the post nor the paper gives a cost, in dollars or in computing; a clean build of the proofs could take several hours [S2, p. 26].
• Third-party verification: specifications and proofs are published [S2, p. 1]; our sources mention neither journal review nor a conference.
• Signal's position beyond its chief technology officer's quote.

Key terms

• Formal verification: mathematically proving that a program meets written properties, in every case, instead of testing it on examples [S2, p. 1].
• Specification: the exact statement of what must be proved, with its assumptions; it has to be right, because the machine cannot check that it says what was meant [S2, p. 3].
• Lean: a programming and proof language whose kernel, a small program, checks every proof [S2, p. 24].
• Machine code, AArch64: the instructions the processor runs; AArch64 is the processor architecture of nearly all Android phones and all iPhones [S2, p. 11].
• libsignal: the reference library of the Signal protocol, written in Rust [S2, p. 1 and 11].
• PQXDH: Signal's handshake, which mixes classical key exchanges with a post-quantum mechanism [S2, p. 7].
• Post-quantum: designed to resist a future quantum computer.
• Triple Ratchet: Signal's ratchet, which derives a fresh key per message; it combines the classical Double Ratchet and the post-quantum SPQR module [S2, p. 7].
• Forward secrecy: stealing a device's current state doesn't reveal past messages [S2, p. 7].
• Post-compromise security: after a key theft, security comes back at the next key exchange, if the attacker stays passive [S2, p. 7].
• Symbolic model: a proof framework where cryptography is a perfect black box (no collisions, nothing can be guessed without the key) [S2, p. 8 and 13].
• Computational model: a proof framework that bounds the chances of any classical attacker with limited means, by tying them to the difficulty of breaking the cryptographic building blocks [S2, p. 8 and 12].
• Trusted computing base: everything that has to be read and trusted for the theorems to guarantee what they claim [S2, p. 24].
• Side channel: information leaking through a physical effect of computation, such as its timing or power consumption.

Source sheet

• Google DeepMind: blog post "Introducing AlphaProof Code: a breakthrough in verifying complex software at depth", by Pushmeet Kohli and Swarat Chaudhuri, dated 10/11/2026.
• Google DeepMind and Google: technical paper "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level", 57 pages, dated 10/11/2026 (Chaudhuri, Ferraiuolo, Kovsharov, Chajed, Schlesinger, Seth, Katz, Sutton, Kohli).
• Google DeepMind: page of the published artifacts (Lean specifications and proofs).
• Related articles: Claude Fable 5.2 and Mythos 5.2, Fermat formalized in Lean according to Anthropic · Gemini 4 Carbon, Google's model.
• Links: Google DeepMind's blog post (10/11/2026) · technical paper (PDF) · artifacts

Source passages

Pages read on 10/11/2026 around 12:13 UTC (dated copies in the article's folder).

Show the 3 sources

Ref.	Quote (original language)	URL
S1↑1↑2↑3↑4↑5↑6	"November 10, 2026" ; "Because Lean automatically checks the rest" ; "From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean" ; "Next, the agents audited the proof and highlighted areas that needed a second look by a human – just one percent of the codebase, a massive time savings." ; "Our work marks the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth. It's also the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI." ; "our verification process took just four weeks" ; "While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion,” said Ehren Kret, Chief Technology Officer of Signal. “Using AI agents to translate live code into valid Lean theorems is a major breakthrough." ; "We thank Signal's Rolfe Schmidt, Michael Rosenberg, and Ehren Kret for their feedback on our methodology."	https://deepmind.google/blog/introducing-alphaproof-code/
S2↑	p. 1 : "2026-11-10" ; "our agents generated about 6.5 million lines of machine-checked Lean proof code, resting on about 26,000 lines of trusted specifications and AArch64 semantics. The proofs cover Signal's post-quantum PQXDH handshake and Triple Ratchet, establishing forward secrecy, authentication, post-compromise security, and handshake secrecy." ; "The formally verified seL4 microkernel [...] took twenty person-years to verify" ; p. 3 : "about 18,000 lines of code in our repository, plus about 8,000 lines of the AArch64 semantics" ; p. 5 : "This cannot be proved, since the hardware and kernel are not formal objects" ; "It does not model threads, signals, the vDSO, dynamic linking" ; p. 6 : "a team typically had 40 to 80 agents and ran on a single machine for 24 to 72 hours" ; "(We leave group messaging as future work.)" ; p. 7 : "stealing a party's current state therefore exposes no earlier encrypted messages (forward secrecy). Every reply also mixes in a fresh DH value, which locks out an adversary who stole the state, as long as it stays passive during that fresh DH exchange (post-compromise security)." ; p. 9 : "We verify the one-to-one session code of libsignal-protocol (v0.105.4, with spqr v1.6.0)" ; "keygen is not verified" ; p. 11 : "The remaining 39 hooked routines are replaced by contracts at the binary boundary" ; "Nearly all Android phones and all iPhones use AArch64" ; "as long as we trust that they preserve the behavior of the protocol code" ; p. 12 : "1 GiB of memory beyond its loaded segments" ; p. 19 : "side channels and other secrets in memory are out of scope" ; "not the post-quantum healing that SPQR adds" ; p. 23 : "Our bounds give no guarantee against a quantum adversary." ; "vacuous for single sessions of about 25,000 messages, or for 2^20 sessions of 2^10 messages" ; p. 23 : "not Signal's own applications" ; p. 24 : "Notably, however, the Rust compiler is not trusted." ; "we reintroduced two bugs that Cheval et al. [40] found in libsignal and that are now fixed" ; "For both bugs we have complete Lean proofs that the symbolic security theorem (§5.1.4) does not hold of the bug-injected binary" ; p. 25 : "refuting the computational theorem is much harder" ; "The proof work was done by a team of five over four weeks" ; "About 6.5 million of them are proofs" ; "Another 140,000 lines prove the reintroduced bugs" ; "about 560 KB, about 140,000 AArch64 instructions" ; "agents powered by Gemini 4 Carbon and Claude Opus 5.5" ; p. 26 : "The proofs were produced entirely by agent teams powered by Gemini 4 Carbon (§2.3), and none of the authors wrote any proof code." ; "Fifteen are gaps or bugs in the computational analysis of the Double Ratchet" ; "A clean build of our proofs could take several hours" ; p. 29 : "To our knowledge, ours are the first proofs of protocol-level security properties for the unmodified code of a widely deployed implementation of a cryptographic protocol." ; p. 30 : "beyond one-to-one sessions, for example, to Signal's group messaging, sealed sender and server-side protocols" ; p. 2 : "we give the first proofs of protocol-level security properties for a widely deployed, unmodified implementation" ; p. 3 : "against classical attackers, and, in the symbolic model, handshake secrecy against a future quantum attacker" ; p. 8 (tableau 1) : "Not covered Computational secrecy, more than two parties, and SPQR's post-quantum healing" ; "Quantum attackers, multi-device state, adversarial first messages to sessions that are later promoted" ; p. 12 : "the two proofs give different assurances about the protocol" ; p. 19 : "our forward secrecy and post-compromise security theorems do not rule out the replay-based loss of forward secrecy described by Cheval et al." ; p. 23 : "The most significant restriction is that the adversary cannot inject its own PQXDH initial message to the responder of a session that is later promoted."	https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf
S3↑1↑2	"Code: https://github.com/google-deepmind/code-verification" ; "Our Lean development is available at https://google-deepmind.github.io/code-verification"	https://google-deepmind.github.io/code-verification