DeepMind's AI proved Signal's code secure in four weeks. The proof trusts 37 crypto routines it didn't check.

Google DeepMind published a result on November 10 that sounds like a finished job: AI agents mathematically proved that the code behind the Signal protocol keeps messages secret. The claim is real, and it’s also narrower than “Signal is proven safe.” The paper behind the blog post spells out the edges, so it’s worth reading them before the headline gets repeated.

What DeepMind says it did

The tool is called AlphaProof Code. According to DeepMind’s announcement, human experts and AI models first turned Signal’s security goals into formal specifications, and humans reviewed every one. Then agents running on Gemini Carbon wrote the proofs in Lean, a language whose checker accepts a proof only if every step holds. DeepMind puts the output at over six million lines of Lean; the technical paper says about 6.5 million.

DeepMind says the proofs cover the protocol’s post-quantum PQXDH handshake and its Triple Ratchet. The properties are forward secrecy, authentication, post-compromise security and handshake secrecy. DeepMind says the whole thing took four weeks, and that its agents flagged about one percent of the work for a human second look.

Signal’s chief technology officer, Ehren Kret, is quoted in the announcement calling the use of AI agents to translate live code into valid Lean theorems “a major breakthrough.”

What’s new here, and what isn’t

Cryptographers have analyzed Signal’s design for years. What’s new is that the proof goes down to the compiled program. The paper says the team built the unmodified libsignal crates with the stock Rust compiler into one AArch64 executable and proved things about whole runs of it, instruction by instruction. DeepMind says real-world vulnerabilities often hide in the gap between design and implementation, and this proof closes that gap for the covered part.

The Register adds some useful scale. It notes that verifying the seL4 microkernel took 20 person-years and the CompCert C compiler took six years. By the paper’s own account, the Signal work took four weeks for a team of five and “quite a few tokens.” DeepMind doesn’t give a dollar figure for those tokens, so the cost comparison stays open.

Where the proof stops

This is the part the headline skips. From the paper:

Item	What the paper says
Code covered	One-to-one sessions in libsignal-protocol v0.105.4: session setup and message encrypt and decrypt
How it’s run	A small command-line tool built around the unmodified library, not the Signal app
Trusted, not proven	37 routines replaced by contracts, including SHA-256, AES-256-CBC, X25519, Kyber1024 and ML-KEM-768
Trusted specifications	About 26,000 lines of specifications and machine-code semantics

So the proof says that if those 37 low-level routines behave as their contracts promise, the protocol code around them delivers the stated security properties. Group chats, the app’s interface and the servers are outside it. My read: that’s normal for formal verification, which always proves a specific statement under stated assumptions. It just matters when the summary becomes “Signal verified.”

Wired reports that the analysis found no new vulnerabilities in the portions it examined. DeepMind says it also reintroduced two real, previously fixed bugs into an isolated copy of the code, and in both cases the system produced a machine-checked proof that the buggy version was insecure. My read: that’s a sanity check on the tool, and it’s the only bug-finding evidence in the announcement.

My read

My read: this is a strong result and a modest security upgrade. Signal users aren’t safer today than they were last week, because nothing was found or fixed. What changed is how cheaply someone can now demonstrate that a piece of security code does what it claims, if a human writes the right specification first.

That last condition is the one I’d watch. The paper itself says most human effort in verification now goes into the specification, and the proof is only as good as that statement. DeepMind notes that humans reviewed every specification. A wrong specification would produce a flawless proof of the wrong thing, and Lean can’t catch that.

I’d also keep the source in mind. DeepMind built the tool, ran the test and wrote the announcement, and the only outside voices I found so far are Signal’s own CTO and press coverage built on the same materials. The Lean files are open-sourced, so anyone can check them, which is the right way to settle it. Cryptographers’ reactions over the next few weeks will tell us more than the blog post does.

For other formal-math work on this site, see our posts on Axiom’s Lean formalization of the Stacks Project and OpenAI’s 722 math papers and what Lean checks in them. On the offensive side of the same coin, there’s Claude finding Xen VM-escape flaws. The Beneficial AI Foundation, according to The Register, set the Signal verification challenge in April. The Signal app itself is outside what DeepMind’s paper covers.

Sources

1. Google DeepMind: Introducing AlphaProof Code
2. DeepMind paper: AlphaProof Code, Verifying Signal’s Security at the Machine-Code Level
3. Wired: A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure
4. The Register: Google DeepMind melds humans and AI agents to vet Signal’s secure messaging techniques