Google DeepMind Says AI Agents Proved Key Security Properties of Signal's Compiled Code
AlphaProof Code produced about 6.5 million lines of Lean proofs covering libsignal's handshake and ratchet at the machine-code level, under stated assumptions and with clear limits.
Published
Last updated / Fact-checked on
Illustrative photo of a classroom chalkboard with equations, graphs, and simple doodled faces; it is not Signal, DeepMind, AlphaProof Code, or a formal proof.
Google DeepMind said Tuesday its researchers used a new multi-agent framework, AlphaProof Code, to mathematically prove key security properties of libsignal, the Signal protocol's reference implementation, at the level of compiled machine code.
According to DeepMind's technical paper, the proofs cover Signal's PQXDH handshake and Triple Ratchet and establish forward secrecy, authentication, post-compromise security and handshake secrecy. The target was unmodified libsignal v0.105.4, compiled by the standard Rust compiler into an AArch64 executable inside a small command-line harness, for one-to-one sessions only. It is not a proof that Signal or its apps are secure in every respect.
At a glance
| Item | Detail | Source/status |
|---|---|---|
| Tool | AlphaProof Code, multi-agent framework with human-approved specs | DeepMind blog, paper |
| Target | Unmodified libsignal v0.105.4, compiled to AArch64 CLI harness | Paper |
| Proved | Forward secrecy, authentication, post-compromise security, handshake secrecy (PQXDH + Triple Ratchet) | Paper |
| Proof size | About 6.5M lines of Lean proof (not lines of verified code) | Paper; blog says "over six million" |
| Time | Four weeks, team of five | Paper; The Register |
| Assumed, not proved | Low-level crypto primitives; Lean kernel; AArch64 model | Paper |
| Not covered | Group messaging, multi-device, full app | Paper; WIRED |
What DeepMind claims
DeepMind's post calls the work "the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth," and "the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI." The paper describes "the first proofs connecting protocol-level security guarantees to the unmodified code" of a widely used cryptographic implementation. Earlier Signal efforts, it says, targeted abstract models, verification-friendly reimplementations, modified code or narrower properties.
The paper says the agents generated about 6.5 million lines of machine-checked Lean proof, resting on about 26,000 lines of trusted specifications and AArch64 semantics; the blog says "over six million." The code being verified is far smaller: about 140,000 AArch64 instructions, roughly 560 KB, per the paper.
How humans and agents split the work
DeepMind says researchers worked with a mix of models to turn Signal's security goals into formal specifications, with human experts reviewing every one; agents "powered by Gemini Carbon" then did the proofs, according to the blog. The paper says a proof counts only if Lean's kernel checks it against the approved specification, and that a team of five did the work over four weeks. The Register reported the same timeline, plus "quite a few tokens."
As a test, the team reintroduced two real, previously fixed libsignal bugs into an isolated version of the code. In both cases the system produced a machine-checked proof that the buggy build violated the symbolic security theorem, DeepMind and the paper report. DeepMind says it is open-sourcing its formal verification artifacts.
Signal CTO Ehren Kret, in a statement carried by DeepMind's post and by WIRED, said "Google DeepMind's approach enables significant expansion" over prior verification of "smaller portions of the code," and called using AI agents to translate live code into Lean theorems "a major breakthrough." Swarat Chaudhuri of DeepMind told The Register that "the next frontier is not going to be proof but specification."
The assumptions and the gaps
Low-level cryptographic primitives, including AES, X25519, Kyber and SHA routines, were assumed through contracts rather than verified; the paper counts 37 such hooked routines. Its symbolic proofs assume perfect cryptography. Its computational bound covers classical attackers only and, the paper says, becomes vacuous for very long sessions with many epochs.
Group messaging, multi-device state, side channels and key generation are outside the results. The paper says they concern DeepMind's own build of the harness, not Signal's applications, and carry over to phone builds only if those preserve the protocol code's behavior. WIRED reported the analysis did not cover the full Signal app and found no new vulnerabilities in the portions examined. Chaudhuri told WIRED there is "a long distance to go" before this scales to all software.
What to watch
Independent review of the open-sourced Lean development; extension to group messaging and to the cryptographic primitives; whether DeepMind applies the framework to other systems; and any Signal-hosted response, since Kret's comment so far appears only via DeepMind and WIRED.
How we reported this
DailyMech read DeepMind's Nov. 10 blog post in full and the technical paper from its abstract through the start of Section 7; the rest was truncated in our fetch and was not read. We read The Register and WIRED in full. No Signal-hosted statement was found. DailyMech did not run or inspect the Lean proofs and contacted no one.
Published and fact-checked November 10, 2026.
Sources
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Pushmeet Kohli and Swarat Chaudhuri, Google DeepMind, November 10, 2026, https://deepmind.google/blog/introducing-alphaproof-code/, fully read
- AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level, Chaudhuri, Ferraiuolo, Kovsharov, Chajed, Schlesinger, Seth, Katz, Sutton, Kohli, Google DeepMind and Google, 2026-11-10, https://google-deepmind.github.io/code-verification/, partially read (abstract through start of Section 7; remainder truncated)
- Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques, Thomas Claburn, The Register, November 10, 2026, https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/5308625, fully read
- A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure, Lily Hay Newman, WIRED, November 10, 2026, https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/, fully read (headline is broader than DeepMind's claims and is not adopted)
DailyMech used AI tools to help research and draft this article; it was fact-checked by our editors.