1. Home
2. News
3. Google

Google DeepMind says its AI agents formally verified Signal's encryption code in four weeks

The proofs run down to the machine code on the phone, and nobody has to read the 6.5 million lines the agents wrote.

By Think Facility · November 10, 2026 · Google DeepMind Cybersecurity Save

On November 10, 2026, Google DeepMind said a team of its AI agents had mathematically proved key security properties of the code behind the Signal protocol, the encryption that protects chats in Signal and Google Messages. The system is called AlphaProof Code, and the work took four weeks.

The proofs aren't about a design on paper. They cover the compiled program itself, the machine code that runs on a phone's processor, and DeepMind says no widely deployed protocol's implementation had been verified like this before, by any method.

Announced

November 10, 2026

Verified

libsignal, the Signal protocol's reference implementation, at the machine-code level

Proof size

about 6.5 million lines of machine-checked Lean

Trusted specification

about 26,000 lines

Time taken

four weeks

How the agents did it

The work splits the way a research team would. People decided what to prove. A writer agent helped them turn security definitions from the research literature into a formal specification in Lean, a language for writing proofs a computer can check, and reviewer agents critiqued each draft before a human approved it.

Then prover agents, running on Gemini Carbon, did the heavy lifting. They wrote the proofs against the executable built from the unmodified Rust code with the standard compiler. Agents also flagged about one percent of the codebase for a person to look at again.

That's the reason the size of the proof doesn't matter much. Nobody has to read 6.5 million lines. What a reader has to trust is the specification, about 18,000 lines in DeepMind's repository plus about 8,000 lines describing how the chip executes code.

What got proved, and what didn't

The proofs cover Signal's post-quantum PQXDH handshake and its Triple Ratchet, the parts that set up a conversation and keep changing its keys. They establish that messages stay protected before and after a device is temporarily compromised, among other properties.

To check the system could tell good code from bad, the team put two real libsignal bugs back in, both fixed long ago, in an isolated copy. In both cases it produced a machine-checked proof that the buggy version was insecure.

The researchers are plain about the limits. The results also trust Lean's kernel and the security of the underlying cryptographic primitives, plus contracts for some routines the program calls. And a flaw in the specification itself could weaken the guarantee, which is why people review every piece of it.

Ehren Kret, Signal's chief technology officer, said in DeepMind's post that the work gives Signal "even greater confidence in our code's privacy guarantees."

What it means for the rest of us

The paper notes that variants of the protocol run in WhatsApp, Meta's Messenger app and Google Messages, as well as Signal. The proofs are about libsignal, not those apps' own code, but the protocol design they check is the one people rely on across all four. DeepMind's post puts the reach at "billions of private conversations."

The bigger shift is cost. Formal proofs have been too slow and expensive for most software, so security has leaned on testing and bug hunting instead. If agents can write the proofs and people only have to get the specification right, the paper's authors say, the main human effort moves to the specification. DeepMind says the Signal work lays groundwork for medical device firmware and power grid software. It didn't give dates for any of that.

It's the second big AI verification claim in a few weeks. On October 23, 2026, we covered Anthropic's report that Claude proved 239 test entry points never crash. DeepMind is open-sourcing its Signal proofs and specifications on a project page, with the technical paper beside them.