Google DeepMind uses AI agents to formally verify core parts of Signal's protocol code

Google DeepMind says it has used AI agents to formally verify key security guarantees of the Signal protocol. The proofs were checked against the compiled code that runs on devices, not only against the protocol's design. The work took about four weeks. DeepMind announced it on 10 November together with a new framework called AlphaProof Code.

The Signal protocol protects messages in the Signal app, and Ars Technica notes it is also used in Google Messages and WhatsApp. The result adds independent mathematical assurance for one of the most widely used pieces of cryptography. It also tests a broader question: can AI make formal verification, a slow and specialised discipline, practical at larger scale?

What was verified

Formal verification uses mathematics to prove that software behaves as specified. Most earlier work on Signal stopped at the design level, according to DeepMind. This project went further and proved properties of the compiled machine code. One example DeepMind gives is that messages stay protected before and after a device is temporarily compromised. The announcement does not list every property that was proved.

DeepMind describes the work as the first AI-assisted formal verification of a widely deployed cryptographic protocol at this depth. It also calls it the first formal verification of such a protocol's implementation by any method. Both are DeepMind's own claims.

The scope was limited. Ars Technica reports that the Signal mobile app as a whole was not verified. DeepMind says that scaling the techniques "requires continued research." The verification found no new vulnerabilities in the parts it examined.

To check that the system can tell correct code from flawed code, the team put two real bugs back into an isolated copy of Signal's code. Both bugs had been fixed long ago. In both cases the system produced a machine-checked proof that the buggy version was insecure. DeepMind is releasing the specifications and proofs as open-source artifacts for other verification work.

How the agents and humans split the work

AlphaProof Code is a multi-agent framework. DeepMind sums up the division of labour this way: human experts decide what to prove, and AI agents do the proving. Researchers used a mix of models to translate Signal's security goals into formal specifications in Lean, a proof language. Human experts reviewed every specification. Agents running on Gemini Carbon then wrote the proofs.

DeepMind's diagram shows three stages. First, a specification is drafted and approved. Second, the compiled machine code runs on a processor model built in Lean. Third, a team of prover agents generates proofs, and a trusted gatekeeper checks them. The provers themselves are treated as untrusted. Lean checks every proof mechanically, so a proof's correctness does not depend on trusting the model that wrote it. The agents also audited their own output and flagged sections for people to look at.

The numbers are large. DeepMind says the agents generated more than six million lines of Lean, and roughly one percent of the codebase needed a second look from a human. DeepMind says comparable work has historically taken expert teams years.

"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," Swarat Chaudhuri, a DeepMind research scientist, told WIRED, as reported by Ars Technica. "There's a middle ground."

Caveats and open questions

The project did not start from zero. DeepMind researchers told Ars Technica they had a head start because the Signal Foundation had done formal verification work before. Ehren Kret, Signal's chief technology officer, said in a statement that prior verification "focused on smaller portions of the code," and that DeepMind's approach "enables significant expansion."

Cost is the main unknown. DeepMind ran the analysis free of charge as a research project. Google declined to share what it cost. The company also declined to say whether it plans a commercial verification product or service. Pushmeet Kohli, DeepMind's vice president of research, said banks and other companies that depend on assurances could one day say, "I can prove these properties." DeepMind presents uses in areas like medical device firmware and power grid software as future possibilities, not results. A technical paper has the details.

"There is a long distance to go before we are able to scale this to all the software of the world, and we want to do that," Chaudhuri said.

What it means for work

Until now, formal verification depended on a small number of specialists. The slowest part of their work was writing the proofs, often over years. In this project, agents wrote nearly all of the proofs, and people reviewed specifications and about one percent of flagged output. If that division holds, the job for security engineers and assurance teams moves away from writing proofs. The skill that matters becomes deciding what should be proved and judging whether a specification captures what matters. That work stays human, and errors at that step are not caught by Lean. What remains open is whether the method transfers to codebases without years of prior groundwork, and at what price, because Google has not disclosed the cost.