Google DeepMind announced the result on 10 November in a blog post and a technical paper. Wired and ZDNet reported it the same day, drawing on the company’s announcement and interviews, so their reports do not independently confirm the results.

The Signal protocol encrypts messages in the Signal app and Google Messages and, according to Wired and ZDNet, also in WhatsApp. DeepMind said the agents proved the properties not just for the protocol’s design but for the implementation itself. The company argues that real vulnerabilities often hide in the gaps between design and implementation.

Humans specified, agents proved

Formal verification does more than test a program: it proves mathematically that the program behaves according to its specification in every situation. A proof therefore covers only what the specification contains.

In AlphaProof Code, researchers first used several language models to turn Signal’s security goals into mathematical specifications. Experts checked each one. AI agents powered by DeepMind’s Gemini Carbon model then wrote the proofs, totalling more than six million lines of Lean. Lean is a programming language in which a computer checks every step of a proof.

The agents also reviewed the proofs and flagged one per cent of the code for human review. Lean checks the rest automatically.

‘We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written,’ DeepMind researcher Swarat Chaudhuri told Wired.

What was proved and what was left out

DeepMind said the properties were proved for the compiled code that devices run. One is that messages stay protected both before and after a temporary compromise of a device. The check did not cover, for example, the whole Signal mobile app, Wired reported.

The work took four weeks. The company said comparable work has taken expert teams years. DeepMind’s researchers told Wired that the Signal Foundation’s earlier formal verification gave them something of a head start. DeepMind said no implementation of such a widely deployed protocol had previously been formally verified by any method. In a statement, Signal’s chief technology officer Ehren Kret said the earlier verification focused on smaller parts of the code.

No new vulnerabilities were found in the parts of the protocol examined, Wired reported. In a test, the researchers reintroduced two real, previously fixed bugs into an isolated version of the code. In both cases, the system produced a machine-checked proof that the version was insecure.

Chaudhuri said there is still a long way to go before the method can be extended to all the world’s software. Google did not tell Wired what the analysis cost.

What DeepMind is opening up

DeepMind is making the verification materials available to others: the specification and the proof, according to Wired. ZDNet’s subheading says the company also plans to open up AlphaProof Code itself, but DeepMind’s announcement mentions only the verification materials. Google did not comment on whether a commercial product is coming, Wired reported.