Takeaway: On November 10, 2026, Google DeepMind introduced AlphaProof Code, an agentic framework for formally verifying real software, and said researchers had used it to prove key security properties of the compiled code behind the Signal protocol — the end-to-end encryption used in the Signal app and, in related forms, in other messengers. The technical paper reports about 6.5 million lines of machine-checked Lean proof about libsignal, the protocol’s reference implementation, at the AArch64 machine-code level. DeepMind calls this the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time an implementation of a protocol like this has been formally verified by any method. The work took four weeks. It is a proof about specified properties of a particular build, not a certificate that every Signal client, or every app that uses a Signal-like protocol, is free of bugs.
The blog says Gemini Carbon agents produced the proofs after human researchers, working with models, translated Signal’s security goals into formal specifications and reviewed those specifications. Carbon itself became generally available the same day on paid API and Google AI Ultra surfaces. This article is about the verification result, not about that product rollout.
What was proved, and at what level
Most formal work on messaging protocols stops at an abstract design, a cleaned-up reimplementation, or a narrower property such as crash-freedom. AlphaProof Code goes further: the paper says the proofs connect protocol-level guarantees to the unmodified code of a widely used cryptographic implementation, after that code is compiled with the ordinary Rust compiler to AArch64 Linux machine code. The target is libsignal version 0.105.4, with the Sparse Post-Quantum Ratchet crate, wrapped in a small command-line harness and linked into one executable. The theorems are about whole runs of that binary — starting a session from a prekey bundle, and encrypting or decrypting a message — not about a rewritten model of the Rust functions alone.
The paper’s headline properties cover Signal’s post-quantum PQXDH handshake and the Triple Ratchet. In the authors’ words, the proofs establish forward secrecy, authentication, post-compromise security, and handshake secrecy. In plainer terms: a later leak of keys should not expose earlier messages; parties should be talking to who they think they are talking to, under the stated conditions; stealing a device’s current state should not, after a later honest key update, leave an attacker permanently inside the conversation; and the handshake secret should stay hidden even in some cases where a future attacker can break ordinary Diffie–Hellman. Those are the properties written into the theorems. They are not a blanket claim that “Signal is unbreakable.”
The team proved those properties in two standard academic models. The symbolic, or Dolev–Yao, model treats cryptographic primitives as ideal black boxes and asks whether secrets leak on any execution. The computational model treats messages as bytes and bounds how well an efficient attacker can do, relative to the hardness of the underlying primitives. The paper uses both because they fail in different ways and give different assurances. The symbolic side, for example, can talk about a later quantum break of Diffie–Hellman; the computational theorems, as stated, cover classical attackers only.
How AlphaProof Code is supposed to work
The framework splits the job the way a research group would. Human authors decide what to prove, resolve ambiguities, and approve the specification — the formal statement of the properties and the assumptions about the machine. Agents draft and criticize that specification. Once it is approved, a team of prover agents writes the Lean proofs. A proof is accepted only if Lean’s kernel checks it and a comparator confirms it proves exactly the held-out, approved statement, not a quietly weakened copy. The blog says agents then flagged about one percent of the codebase for a second look by a human; Lean checks the rest.
That division of trust is the point of the system. The multi-million-line proofs are untrusted in the ordinary formal-methods sense: a wrong proof should not get past the kernel. The specification is trusted. If the theorem asks too little, assumes too much, or models the environment incorrectly, a checked proof can still be true and the security story can still be weaker than a reader expects. DeepMind is explicit that specification writing, not proof writing, was the hard part once agents could generate large proofs.
The paper also describes the scale of the agent team: typically 40 to 80 agents on a single machine for 24 to 72 hours at a stretch, with an orchestrator, team leads, an architect, and an integrator who alone commits to the repository. A five-person research team ran those campaigns over four weeks. That is a sharp contrast with earlier landmarks the authors cite, such as the seL4 microkernel, which they note took twenty person-years, on code written with verification in mind. Those historical comparisons are about labor, not a claim that libsignal is in the same class of system as a microkernel.
What you still have to trust — and what was left out
A machine-checked proof is only as broad as its trusted base and its scope. The paper is unusually direct about both, and those limits belong in any summary that repeats the “grand challenge” language.
- The proofs are about a specific AArch64 build of a command-line harness around
libsignalv0.105.4, not about Signal’s iOS or Android apps as shipped. The authors say the same Rust protocol code runs in those apps, and that the theorems carry over only insofar as those environments preserve the behavior of the protocol code as exercised by this binary. - Group messaging is future work. The campaign covers one-to-one sessions.
- Low-level cryptographic primitives — hash compression, AES, X25519, Kyber, ML-KEM, and related routines — are modeled with contracts rather than proved instruction by instruction. The results assume those primitives meet their specifications. The security of the math itself is not what was proved.
- The computational theorems do not claim security against a quantum attacker. Part of that gap is addressed on the symbolic side, and even there the authors say their ratchet theorems show the Triple Ratchet is no weaker than the Double Ratchet, not the extra post-quantum healing the newer ratchet is designed to add.
- The symbolic theorems excuse some byte-collision cases rather than bounding their probability, and they assume fresh randomness. The computational bound becomes vacuous at large scale if nearly every message starts a new epoch, and the game restricts the attacker in ways the literature does not, including limits on injected first messages.
- WhatsApp, Messenger, and Google Messages are mentioned as places where variants of the protocol are deployed. This paper does not claim to have verified those products.
Readers who want the exact theorem statements, the hooked routines, and the attacker models should use the paper and the open Lean development. The blog’s shorter version is the announcement; the paper is the result.
A check that the specifications can fail
To test whether the theorems were strong enough to notice real mistakes, the authors reintroduced two bugs that earlier researchers had found in libsignal and that have since been fixed. In both cases, they compiled a buggy binary and proved, in Lean, that the symbolic security theorem does not hold of that binary. One bug stored unconfirmed session state, including a copy of a signed prekey secret, after a prekey message was decrypted only against an older session. The other failed to reject a malformed X25519 key and allowed a replayed handshake to create a second session with the same shared secret.
That is a meaningful check: the specification is not so loose that those historical bugs would still “prove.” It is not the same as an audit of today’s Signal clients, and the authors note that refuting the computational theorem in the same way is much harder, because that theorem is a bound involving reductions to hardness assumptions.
Using AI agents to translate live code into valid Lean theorems is a major breakthrough. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees.
Ehren Kret, Chief Technology Officer of Signal, quoted in DeepMind’s November 10 post
Kret also said prior formal verification had focused on smaller portions of the code, and that DeepMind’s approach enables a significant expansion. That is Signal’s endorsement of the method and the scope. It is not an independent replication of the proofs.
Why this matters for software security — with the obvious caveat
Formal verification has always been the highest bar in software assurance, and it has always been too expensive for almost all production code. If agent teams can take an approved specification and produce millions of lines of kernel-checked proof about compiled code in weeks, that bar moves. DeepMind frames the Signal result as groundwork for other critical systems, from firmware to grid software, and mentions pairing this kind of proof with automated defense agents such as CodeMender. Those are research directions, not products announced in the same post.
The result also sits next to a different kind of “proof about models” already on this site. Anthropic’s FlashProve is a research prototype for proving that a published model commitment produced a given reply. AlphaProof Code is about proving properties of compiled protocol code. They share a taste for machine-checkable guarantees. They are not the same technique, and neither is a general-purpose “AI proved this app is safe” button.
We have not rerun the Lean development or audited the trusted specification. The claims in this article are from DeepMind’s blog and paper, and from the Signal quote published with the announcement.
Facts at a glance
| Item | What DeepMind published on November 10, 2026 |
|---|---|
| Framework | AlphaProof Code: humans approve a Lean specification; AI agents write proofs; Lean’s kernel and a comparator accept only proofs of that statement. |
| Target | Unmodified libsignal v0.105.4, compiled with stock rustc to an AArch64 Linux executable, for one-to-one sessions. |
| Properties claimed | Forward secrecy, authentication, post-compromise security, and handshake secrecy for PQXDH and the Triple Ratchet, in symbolic and computational models, with the limits described in the paper. |
| Proof size | About 6.5 million lines of machine-checked Lean, on about 26,000 lines of trusted specifications and AArch64 semantics in the paper’s abstract (the body gives a more detailed trusted-base breakdown). |
| Time | Four weeks of work by a five-person team directing agent campaigns, versus years of expert labor for comparable formal efforts historically. |
| Bug check | Two previously fixed libsignal bugs were reintroduced; the team proved the symbolic security theorem false on those binaries. |
| Agents | The blog says Gemini Carbon agents generated the proofs. The paper describes teams of typically 40 to 80 agents. |
| Release | The Lean development is open at DeepMind’s code-verification site. |
| What it is not | A verification of Signal’s mobile apps as shipped, of group messaging, of WhatsApp or other variants, or of the underlying cryptographic primitives themselves. |
FAQ: DeepMind’s AlphaProof Code and Signal
Did Google DeepMind prove that Signal is completely secure?
No. It proved specified security properties of a particular compiled build of libsignal for one-to-one sessions, under stated assumptions. The paper lists a trusted base, hooked cryptographic primitives, attacker models, and several things that are out of scope, including group messaging and Signal’s own mobile apps as shipped.
What is AlphaProof Code?
It is DeepMind’s multi-agent framework for formal verification. People decide what to prove and approve the Lean specification. Agents write the proofs. A result counts only if Lean’s kernel accepts it and a comparator shows it matches the approved statement.
What does “machine-code level” mean here?
The theorems are about the compiled AArch64 executable, not only about a model of the Rust source. The code was compiled with the ordinary Rust compiler. That is meant to close the usual gap between a protocol design and the binary that actually runs.
How large were the proofs?
The paper says the agents generated about 6.5 million lines of machine-checked Lean, resting on about 26,000 lines of trusted specifications and AArch64 semantics, as described in the abstract. The proofs are untrusted in the formal-methods sense; the specification is what a reader has to believe.
Did this use Gemini 4 Carbon?
DeepMind’s blog says agents powered by Gemini Carbon did the proofs. Carbon’s general availability, announced the same day, is a separate product story. The paper focuses on the verification framework and the Signal result, not on API pricing or consumer access.
Is WhatsApp or Google Messages covered?
The paper notes that variants of the Signal protocol are used in those apps. It does not claim to have verified those products. The proofs are about this libsignal build.
How do we know the theorems are strong enough?
The authors reintroduced two historical, now-fixed bugs and proved that the symbolic security theorem does not hold of the buggy binaries. That is evidence the specification can fail when the code is wrong. It is not a substitute for reviewing the trusted definitions.
Can other teams inspect the work?
Yes. DeepMind says it is open-sourcing the formal verification artifacts, and the paper points to the Lean development on the project site. Open artifacts are not the same as an independent audit, but they make one possible.