DeepMind's AlphaProof Code formally verifies the Signal protocol

Google DeepMind researchers used an agentic AI framework called AlphaProof Code to mathematically prove several key cryptographic guarantees of the Signal protocol, according to Wired. The work, a proof of concept completed in four weeks, is an exercise in formal verification: a method that uses mathematics to check that software behaves as intended, instead of testing a sample of cases.

The Signal protocol is the encryption scheme behind the Signal app and, as Wired points out, it also protects communications on Google Messages and WhatsApp. The analysis is therefore presented as further independent validation of cryptography that secures a very large volume of messages. Wired calls it a landmark for cryptography and for AI itself, while stressing that its scope is limited.

What exactly did DeepMind prove?

The team proved “a number of” the protocol’s key guarantees, not all of them. Wired is explicit that the analysis did not formally verify the entire Signal mobile app, and the researchers describe their result as one milestone in a larger process. “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,” Swarat Chaudhuri, a DeepMind research scientist, told Wired.

According to the same article, the analysis found no new vulnerability in the portions of the protocol that were examined. The researchers also ran AlphaProof Code on older versions of Signal that contain known, long-fixed vulnerabilities: the tool correctly identified them and showed that those versions could not be formally verified. That test matters because it shows the method can fail when a flaw exists, not only succeed when none does.

• Tool: AlphaProof Code, a new agentic AI framework from Google DeepMind.
• Duration: four weeks, as a proof-of-concept project.
• Result: key cryptographic guarantees proved; no new vulnerability found in the portions analysed.
• Older versions: known, long-fixed flaws detected, and the protocol shown to be unverifiable.
• Release: the specification and the proof are being published to help other formal verification work.
• Cost: not disclosed; the analysis was done free of charge as a research project.

How did AI and humans share the work?

Before the AI era, people had to describe the properties they wanted to prove, turn those descriptions into formulas, and then develop the proof. Wired explains that agentic AI can sharply reduce the time spent on the last step, which is what made the four-week Signal evaluation possible. The DeepMind researchers add that they had a head start because the Signal Foundation had already done formal verification work on smaller portions of the code.

Ehren Kret, Signal’s chief technology officer, said in a statement quoted by Wired: “While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach enables significant expansion.” He added that rigorously verifying the implementation gives Signal even greater confidence in the privacy guarantees of its code as AI-driven security threats grow.

DeepMind says its main advance is a “human-AI collaboration process”: agents contribute and self-correct at almost every phase, while humans review at key junctures. “We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs,” Chaudhuri said. A formal proof only guarantees the properties that were written down, which is why human review of the specification remains central.

A parallel effort around Signal

DeepMind’s work is not the only attempt to prove Signal’s cryptography. The Beneficial AI Foundation, working with Signal’s Rolfe Schmidt and the Lean FRO, has launched “Signal Shot”, a public project to verify the protocol and its Rust implementation with the Lean proof assistant. It plans to translate Signal’s Rust code into Lean using a tool called Aeneas, and lists components to verify such as the PQXDH post-quantum key exchange, the Double Ratchet and the SPQR/Triple Ratchet. Wired does not link this initiative to DeepMind’s, and the two should be treated as separate efforts.

What remains uncertain?

The open question, Wired notes, is whether AI-automated formal verification can scale at a workable cost. Google declined to share the cost of the Signal analysis and declined to say whether it plans a commercial formal verification product or service. Pushmeet Kohli, chief scientist at Google Cloud and DeepMind’s vice president of research, imagines banks and other companies worried about bugs being able to say they can prove certain properties of their software. That is a vision, not an announced offer.

What this changes for companies

For a company that chooses a messaging tool or builds on the Signal protocol, the result is a reassuring signal about the protocol’s design, not a certificate for every app that uses it: the full Signal app was not verified, and a product’s deployment, servers and settings remain outside the proof. The published specification and proof give security teams material to study and reuse. Since the cost and any commercial offer are unknown, firms should not yet count on formally verifying their own code with this approach, but they can start asking suppliers of critical software which properties are specified and proved.