Google DeepMind's AI agents proved Signal's code secure. What that does and doesn't mean

On 10 November Google DeepMind said its AI agents had mathematically proved key security properties of the code behind the Signal protocol, the encryption that protects messages in Signal and Google Messages. Most AI security news is about finding bugs. This is about the opposite: showing that a whole class of bugs is not there. Here is what was proved, how, and the limits the researchers set out in their own paper.

What was announced

The work uses a new system called AlphaProof Code. DeepMind applied it to libsignal, the official implementation of the Signal protocol, written in Rust. The proofs cover two core parts of the protocol: the PQXDH handshake, which sets up a conversation and is designed to resist future quantum computers, and the Triple Ratchet, which keeps changing the keys as a conversation goes on.

The properties proved include:

• Forward secrecy: if a device is compromised today, past messages stay protected.
• Post-compromise security: after a temporary compromise ends, later messages become protected again.
• Authentication: you are talking to the person you think you are.
• Handshake secrecy: including, in one of the two proofs, against a future quantum attacker.

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 verified by any method.

Why "machine code" matters

Formal verification means writing a precise mathematical statement of what software must do, then proving that it does it. A program called a proof checker, here the Lean language, checks every step, so a mistake in the proof is rejected automatically.

Signal's design has been analysed formally before. What is new is the level. The proofs are about the compiled machine code that actually runs on a 64-bit Arm processor, not about a description of the design. DeepMind points out that real vulnerabilities often hide in the gap between a design and the code that implements it, and closing that gap is what makes the proofs so large.

How the work was split

AlphaProof Code divides the job the way a research team would:

• Humans decide what to prove. Researchers worked with AI models to turn Signal's security goals into formal specifications, and human experts reviewed every one. SecurityWeek reports that the agents helping with this step ran on Gemini 4 Carbon and Claude Opus 5.5.
• Agents write the proofs. Agents powered by Gemini Carbon produced about 6.5 million lines of Lean proof.
• Agents flag what needs a human. The agents audited their own work and marked about 1% of it for human review. Lean checks the rest.

The key design choice is that the agents are not trusted. Only about 26,000 lines need to be trusted: some 18,000 lines of specifications plus about 8,000 lines describing how the processor executes instructions. If the agents make a logical error, Lean refuses the proof.

The scale is large. The verified code is about 560 KB, roughly 140,000 machine instructions. DeepMind says the work took four weeks, and SecurityWeek reports that five researchers did it. For comparison, the paper notes that the verified seL4 operating-system kernel, one of the field's best-known successes, took twenty person-years.

A test with real bugs

A proof is only as good as the statement it proves. To check that the specifications would catch genuine mistakes, the team put two real, previously fixed libsignal bugs back into an isolated copy of the code. In both cases the system produced a machine-checked proof that the buggy version was insecure.

The limits, in the researchers' own words

The paper is careful about what is not covered, and these limits matter:

• It is not the Signal app. The proofs cover Google's own build of libsignal, wrapped in a small command-line program. SecurityWeek quotes the work as covering "not Signal's own applications."
• Cryptography is assumed to be perfect in the symbolic proof. It treats building blocks such as hashes and encryption as ideal and says nothing about how well the real algorithms resist attack. A separate computational proof covers more, but with its own assumptions.
• Side channels are out of scope, such as leaks through timing or other secrets in memory.
• The scenario is narrow. Two honest parties with fixed roles, identity keys already trusted, limits on message sizes and counts, and no multi-device state. Group chats and some kinds of one-time keys are not covered.
• One known weakness is not ruled out. The forward-secrecy theorems do not exclude a previously published replay attack, although the real code runs a check intended to stop it.

None of this makes the result small. It does mean the right headline is "the core protocol code meets these specific guarantees under these assumptions", not "Signal is proven unhackable".

Why it matters

Last week I wrote about OpenAI's pipeline that built 948 Linux exploits. AI is making it cheaper to find and exploit flaws. Formal verification is the defender's answer: rather than racing to find bugs first, prove that whole categories of them cannot exist. Until now that has been too expensive for most software. If AI agents can write the proofs while humans focus on the specifications, that could change.

Signal's chief technology officer, Ehren Kret, said in DeepMind's announcement that the work gives the company "even greater confidence in our code's privacy guarantees." DeepMind has published the specifications and proofs on GitHub so others can check them. In October I covered Claude's machine-checked proofs that software cannot crash; this is a much larger example of the same idea.

The same day, Google made Gemini 4 Carbon, the model behind the proof agents, available to all paying developers and businesses. SecurityWeek reports that the introductory price of $2 / $10 per million tokens runs until 30 November and then doubles. I covered Carbon's limited release in an earlier post.

What to watch

• Outside experts working through the published Lean proofs and specifications.
• Whether the approach extends to the Signal apps themselves, group messaging and side channels.
• DeepMind's next targets. It mentions medical device firmware and power grid software as possibilities.
• The cost. DeepMind has not said how much computing the four weeks of agent work used.