Google DeepMind's AlphaProof Code formally verifies key Signal protocol guarantees in four weeks

Google DeepMind used agentic AI to formally verify a number of the Signal protocol's key cryptographic guarantees, completing the proof-of-concept project in four weeks, WIRED reports. The work relies on a new AI framework called AlphaProof Code.

What was verified

Formal verification uses math to check that software functions as intended, meaning it has no critical vulnerabilities. The DeepMind analysis found no new vulnerabilities in the portions of the Signal protocol it examined.

The researchers also ran AlphaProof Code on older versions of Signal that contain known, long-fixed vulnerabilities. The framework correctly identified them and showed that those versions could not be formally verified.

DeepMind is releasing the specification and proof it developed for the Signal protocol analysis to support other formal verification work.

Scope and limits

The analysis was limited in scope. It did not formally verify the entire Signal mobile app. DeepMind researchers describe the findings as one milestone in a larger process.

The team also had a head start from earlier formal verification work by the Signal Foundation. Ehren Kret, Signal's chief technology officer, said in a statement: "While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion." He added that verifying the protocol implementation gives Signal "even greater confidence in our code's privacy guarantees."

Swarat Chaudhuri, a DeepMind research scientist, told WIRED: "We are very excited by this result, but 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."

Human-AI collaboration process

Chaudhuri says a key advance is a "human-AI collaboration process" in which agents contribute and self-correct at almost every phase while still seeking human input and review at key junctures. He rejected a fully automated approach: "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. There's a middle ground."

According to WIRED, describing the desired software properties, turning them into formulas and developing the proof were all time-consuming for people before AI. Agentic AI can significantly cut the time of the last step, the proof development.

Cost and commercial plans

DeepMind conducted the Signal analysis free of charge as a research project. Google declined to share the cost of the analysis and declined to comment on whether it plans a commercial formal verification product or service. No pricing, benchmark scores or model specifications for AlphaProof Code have been disclosed.

Pushmeet Kohli, chief scientist at Google Cloud and DeepMind's vice president of research, said: "If you can now verify the correctness of these implementations, then you can rest easy." He pointed to banks and other companies that rely on assurances and worry about bugs.

What this means

The result is independent validation of cryptography that, per WIRED, protects large volumes of communications on Signal, Google Messages and WhatsApp. It also shows AlphaProof Code can both confirm a protocol's guarantees and flag versions with known flaws as unverifiable.

The open question, as WIRED frames it, is whether AI-automated formal verification can scale at a workable cost. With the cost undisclosed and no commercial plans commented on, the four-week timeline is the only effort metric available. The released specification and proof give other researchers material to build on. The human review checkpoints in DeepMind's process show how the team intends to keep proofs and goals from being both AI-generated and self-validated.