Google DeepMind has used AI agents to mathematically prove key security properties of the code behind the Signal protocol, the encryption that protects billions of private conversations in apps including Signal and Google Messages. The work, done with a new framework called AlphaProof Code, took four weeks, a task DeepMind says historically takes expert teams years.
The lab announced the result on November 10, calling it the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time the actual implementation of such a protocol has been formally verified by any method, with or without AI.
How AlphaProof Code verified Signal
AlphaProof Code is a multi-model agentic framework that splits formal verification the way a research team would. Human experts work with AI to decide what must be proved, translating Signal’s security goals into formal mathematical specifications, with experts reviewing every one. Then a group of proof-writing agents, powered by Gemini Carbon, does the proving, generating over 6 million lines of Lean, a computer language that mathematically proves the accuracy of code.
What makes the result unusual is its depth. Most protocol verification stops at the design level, checking that the protocol is sound on paper. DeepMind’s agents went further, proving that the compiled code fulfills the key security properties down to the exact code running on devices. The target was libsignal, Signal’s reference implementation, compiled with the standard Rust compiler into AArch64 machine code. The verified properties include message confidentiality and authenticity, forward secrecy, post-compromise security and handshake secrecy for Signal’s post-quantum PQXDH handshake and Triple Ratchet.
Because real vulnerabilities often hide in the gap between a design and its implementation, closing that gap is what makes the proofs far more complex, and far more valuable, than a design-level check.
A machine-checked result, with humans on 1%
Every proof the agents wrote was checked by Lean’s kernel, which verifies the work automatically. The agents then audited their own proofs and highlighted the areas that needed a second look by a human: just 1% of the codebase. DeepMind says that focus is a massive time saving, because experts could spend their review where human judgment matters most.
To confirm the system can tell correct code from buggy code, the researchers reintroduced two real, previously fixed bugs into an isolated version of Signal’s code. In both cases, the system produced a machine-checked proof that the buggy version was insecure. The verification also found no new vulnerabilities in the parts of Signal it examined.
“Our work marks the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth,” DeepMind wrote in the announcement.
What the proof does not cover
The result is a milestone, not a certificate that Signal is unhackable. The proof covers the core cryptographic protocol code for one-to-one sessions, not the full Signal mobile app, and it does not cover group chats, multi-device behavior or every device architecture. The low-level cryptographic primitives were treated as assumed-secure contracts rather than proven from scratch, and the proofs target one compiled platform, AArch64 Linux. For Signal users, there is no emergency patch or account change tied to the announcement.
DeepMind is open-sourcing its formal verification artifacts for community use, and has published a technical paper with the full details. The lab says the same techniques could secure other vital systems, from medical device firmware to power grid software, and that paired with automated defense agents such as CodeMender, formal verification can help counter the speed and scale of modern cyber threats.
Why it matters
Cryptographic protocols underpin nearly all digital communication, from online banking to web browsing, and a single flaw can expose millions of people at once. Formal verification is the highest standard of security assurance, but it has been so labor-intensive that it was reserved for a handful of critical systems.
If AI agents can compress years of expert proof work into four weeks, that standard becomes affordable for far more software. The Signal result is the proof of concept: a widely deployed protocol, verified at the machine-code level, with the artifacts published so others can check the work. The next question is which critical system gets verified next, and how quickly the technique spreads beyond the lab that built it.
