Google DeepMind's AI agents formally verify Signal's encryption code: what it proves
Google DeepMind says AI agents built on its AlphaProof Code framework have mathematically proved key security properties of the compiled code behind the Signal protocol, generating about 6.5 million lines of machine-checked proofs in four weeks. The result covers Signal's core one-to-one encryption library under stated assumptions, not the whole Signal app or every messaging service that uses the protocol.
Google DeepMind says a team of researchers working with AI agents has mathematically proved that the compiled code at the heart of the Signal protocol delivers its core security guarantees. The work, announced on 10 November 2026, used a new framework called AlphaProof Code and produced about 6.5 million lines of machine-checked proof in roughly four weeks, a job the researchers say would have taken expert teams years with earlier tools.
The proofs cover libsignal, the official implementation of the encryption protocol used by the Signal app and, according to Google, Google Messages. They show that the code's post-quantum handshake and message-encryption scheme provide forward secrecy, authentication, post-compromise security and handshake secrecy, under assumptions the researchers spell out. The analysis did not find new vulnerabilities, and it does not amount to a security guarantee for the entire Signal app.
What did DeepMind actually announce?
In a blog post by Pushmeet Kohli, DeepMind's vice president of research, and research scientist Swarat Chaudhuri, the company described AlphaProof Code as a "multi-LLM agentic framework" for formal verification. Formal verification means writing down precisely what a program is supposed to guarantee and then proving, with mathematical rigour, that the program always does so. Unlike testing, which checks particular cases, a valid proof rules out every bug or attack that would violate the stated properties.
DeepMind says this is 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 such a protocol has been formally verified by any method. Those are DeepMind's own claims; the published paper and proof files allow outside researchers to check them.
The company has published a technical paper and released its proof files publicly through a GitHub repository so that others can inspect and build on them.
How does AlphaProof Code work?
The framework splits the work in two. First, human experts work with AI models to turn Signal's security goals into formal specifications written in Lean, a programming language and proof assistant used to state and check mathematical proofs. DeepMind says human experts reviewed every specification.
Second, a team of AI agents powered by Gemini Carbon, Google's newest model, tries to prove that the code satisfies those specifications. A proof is accepted only if Lean's kernel, a small trusted checker, confirms it. DeepMind says the agents then audited their own work and flagged about 1% of the material for human review.
According to the paper, the repository holds nearly 7 million lines of Lean. About 6.5 million lines are proofs, resting on roughly 26,000 lines of trusted specifications and a formal model of AArch64, the 64-bit Arm instruction set used by nearly all Android phones and all iPhones. The verified libsignal code is about 560 KB, or roughly 140,000 machine instructions.
Chaudhuri told The Register that the project took a team of five people four weeks. For comparison, the paper notes that verifying the seL4 microkernel, often cited as the field's biggest success, took about 20 person-years, and the CompCert verified C compiler took six.
Why does proving the compiled code matter?
Most formal analysis of cryptographic protocols stops at the design: it proves the protocol is sound on paper. Real attacks, however, often exploit the gap between a design and the code that implements it.
DeepMind's proofs go down to the compiled machine code, the instructions a processor actually runs. The researchers wrapped the unmodified libsignal Rust code (version 0.105.4) in a small command-line tool, compiled it for AArch64 Linux, and proved theorems about complete runs of that executable, instruction by instruction. The paper says the results should carry over to the Signal apps on Android and iOS, which run the same Rust code, with differences in compiler settings, linking and operating system.
To check that the system could tell good code from bad, the team reintroduced two real, previously fixed bugs into an isolated copy of the code. In both cases AlphaProof Code produced a machine-checked proof that the buggy version was insecure.
What are the limits of the result?
The guarantees are conditional, and the paper is explicit about where they stop:
- Scope: the proofs cover one-to-one sessions: the PQXDH handshake that sets up a conversation and the Triple Ratchet that encrypts messages. Anything outside that one-to-one session code, including the rest of the Signal mobile app, is not covered, a point Wired also highlighted.
- Cryptography assumptions: one of the two proofs is "symbolic", meaning it assumes the underlying cryptographic building blocks are perfect. A second, "computational" proof gives probability-based bounds but, the paper says, offers no guarantee against a quantum adversary and restricts the attacker in some ways the academic literature does not.
- Trusted pieces: readers must still trust the formal model of the processor and of how Linux runs a process, the stated behaviour of certain "hooked" routines such as low-level cryptographic functions, and the specifications themselves.
- Environment: the guarantees describe a specific, controlled execution setup, not every device configuration.
Other apps such as WhatsApp use the Signal protocol design but their own code, so these proofs do not directly verify those implementations.
What has Signal said?
Signal's chief technology officer, Ehren Kret, said in a statement provided by DeepMind that prior formal verification had focused on smaller portions of the code and that DeepMind's approach "enables significant expansion". He added that "rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees."
Wired reported that DeepMind's team benefited from earlier formal verification work carried out for the Signal Foundation, and that the project was done free of charge as research. Google declined to share its cost or say whether it plans a commercial verification product.
Why does this matter beyond Signal?
AI tools are making it faster to find software vulnerabilities, and defenders are under pressure to keep up. Formal verification is often described as the strongest form of assurance, but its cost has confined it to a few critical systems. If AI can cut that cost sharply, it could be applied to banking software, medical-device firmware or power-grid systems, examples DeepMind itself cites.
The researchers say the bottleneck has shifted. "Once proofs become cheap, the hard question is what to prove," the paper says, noting that most of the team's effort went into writing specifications rather than proofs. Chaudhuri told Wired the team wanted to avoid a world where "AI is generating the goals and AI is generating the proofs" without human judgment.
What happens next?
The Register reported that the work is a step towards a challenge set in April 2026 by the Beneficial AI Foundation to formally verify both the Signal protocol and the Signal app in Lean. DeepMind says scaling the technique will require further research and could be paired with automated defence tools such as its CodeMender project.
For ordinary Signal users, nothing changes in how the app works. The result adds independent, machine-checked evidence that the core encryption code does what it is designed to do, within clearly stated limits.
Image: Photo: Photographer.JuliaMustard, CC BY-SA 4.0 (https://creativecommons.org/licenses/by-sa/4.0/), via Wikimedia Commons (https://commons.wikimedia.org/wiki/File:Pushmeet_Kohli_at_SXSW_London_2026.jpg) — June 2026 file photo of Pushmeet Kohli at SXSW London, resized; not taken at the announcement
About this article: prepared by The Daily Context editorial desk using automated, source-based reporting from the publications linked below. No reporter was on the ground.
Sources
- Google DeepMind, Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (10 Nov 2026): https://deepmind.google/blog/introducing-alphaproof-code/
- Google DeepMind, AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (technical paper, 10 Nov 2026): https://google-deepmind.github.io/code-verification/
- Google DeepMind, code-verification repository on GitHub: https://github.com/google-deepmind/code-verification
- Wired, A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure (10 Nov 2026): https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/
- The Register, Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques (10 Nov 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
Kabeer Ahmad
Kabeer Ahmad is the founder and editor of The Daily Context. He oversees the site's source-based coverage of world affairs, technology, business, entertainment, lifestyle and sports, and is responsible for its editorial standards, sourcing and corrections.
