Google DeepMind Says AI Agents Proved Signal's Actual Encryption Code Secure in Four Weeks, With Humans Writing What to Prove
Google DeepMind said on November 10 that AlphaProof Code, a multi-agent framework built on Gemini Carbon, produced machine-checked Lean proofs that the code implementing the Signal protocol meets key security properties that human experts specified. DeepMind says the work took four weeks, that agents flagged about 1% of the proof for human review, and that the system caught two reintroduced bugs. Signal's CTO welcomed it; no independent audit has been published.
The claim that matters is not that an AI wrote a lot of proofs. It is where the proofs reach: Google DeepMind says its agents verified the compiled code of the Signal protocol, not just its design, which is where real-world bugs tend to hide. The strength of the result rests on the specifications, and those were written and reviewed by people.
What DeepMind says it did#
Google DeepMind said on November 10 that researchers used AlphaProof Code, a new multi-LLM agentic framework, to mathematically prove key security properties of the code underlying the Signal protocol, which protects messages in apps including Signal and Google Messages.
The work split in two. 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 wrote the proofs in Lean, a language whose checker verifies each step. DeepMind says the agents generated more than six million lines of Lean, then audited the result and flagged about 1% for human review.
DeepMind says the proofs show that the compiled code delivers properties such as keeping messages protected before and after a device is temporarily compromised. The verification took four weeks, which DeepMind contrasts with the years such work has historically taken expert teams.
To check that the system could tell correct code from flawed code, the team reintroduced two real, previously fixed bugs into an isolated copy of Signal's code. In both cases, DeepMind says, it produced a machine-checked proof that the buggy version was insecure.
DeepMind calls this 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. It says it is open-sourcing the verification artifacts.
Signal's view and the caveats#
Signal CTO Ehren Kret said in DeepMind's post that "using AI agents to translate live code into valid Lean theorems is a major breakthrough" and that the verification gives Signal "even greater confidence" in its privacy guarantees.
Axios, which interviewed DeepMind research scientist Swarat Chaudhuri, reported that the work remains a research project, not a commercial product. DeepMind is looking at building the technique into AI coding agents and combining it with Google's Project Zero and CodeMender bug-hunting and patching tools, Axios reported.
The result fits a run of machine-checked security work from frontier labs. In October, Anthropic and Theorem said Claude produced Rocq-checked no-crash proofs for 239 entry points in 123 libraries, limited to RISC-V builds. Axios names the model as Gemini 4 Carbon, the system Google first released to vetted cyber defenders in October.
Limits#
- A formal proof shows the code meets its specification, nothing more. Properties that were not specified, and flaws outside the verified code, are not covered.
- The figures and "first" claims are DeepMind's own. We read DeepMind's post and Axios's report, not the technical paper, and found no independent review of the proofs.
- DeepMind's post says more than six million lines of Lean; Axios reported more than three million. We could not resolve the difference.
- DeepMind's post names the model as Gemini Carbon; Axios calls it Gemini 4 Carbon.