A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure

Google DeepMind researchers used agentic AI to mathematically prove, or formally verify, a number of the Signal protocol's key cryptographic guarantees. Wired's report describes the result as a landmark development for the widely used cryptography and for AI itself. The team conducted the work as a proof-of-concept project and completed it in four weeks.

This piece covers the guarantees DeepMind checked, the limit that left the entire Signal mobile app unverified, the tests on older Signal versions, and what DeepMind and Signal said about scale and cost. It is for people who rely on the Signal protocol in the Signal app, Google Messages, and WhatsApp, and for banks and other companies that rely on assurances and worry about bugs.

01Three messengers under one proof

Conducted as a sort of proof-of-concept project in just four weeks, the work is significant in two ways. It serves as further independent validation of the cryptography that protects massive quantities of the world's communications on platforms like the Signal app, Google Messages, and WhatsApp.

The project also demonstrates Google DeepMind's formal verification capabilities using a new AI framework called AlphaProof Code. Researchers used that agentic system to mathematically prove, or formally verify, a number of the Signal protocol's key cryptographic guarantees during the four-week proof-of-concept.

02Math checks and a holy grail

AI-aided formal verification is having a moment. It is unclear how practical it will be for widespread use, and how effective it can be at securing large amounts of code. Proponents of formal verification have long referred to it as a sort of holy grail in software security.

Formal verification uses math to check and validate that software is functioning as intended. In other words, it shows that the software does not have critical vulnerabilities. DeepMind's Signal evaluation uses that check on a number of the protocol's key cryptographic guarantees.

Before the AI era, it was incredibly time-consuming for people to describe the characteristics of software they wanted to prove, turn these summaries into formulas, and then develop the proof. Agentic AI can significantly cut down the time of the latter project, developing the proof. That cut is what enabled analyses like DeepMind's Signal evaluation.

03Signal mobile app outside the proof

Even after agentic AI cut down the time to develop the proof, the Signal evaluation was limited in scope. It did not, for example, formally verify the entire Signal mobile app. DeepMind researchers emphasize that their findings are just one milestone in a larger process.

Swarat Chaudhuri, a DeepMind research scientist, tells 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."

04Older versions and a released proof

The DeepMind analysis did not find any new vulnerabilities in the portions of the Signal protocol it looked at. When the researchers used AlphaProof Code on older versions of Signal that contain known and long-fixed vulnerabilities, it correctly identified them and showed that the protocol could not be formally verified.

The researchers are releasing the specification and proof they developed for the Signal protocol analysis to aid other formal verification work. While the speed of the project was notable, they point out that they were able to get a head start to a degree because of past formal verification work that the Signal Foundation has conducted.

Ehren Kret, Signal's chief technology officer, says in a statement, "While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion." He also says, "As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees."

05Banks, cost, and a middle ground

For critical services used in high-stakes settings, formally verifying every code base and entire software supply chains would be a dream. Pushmeet Kohli, chief scientist at Google Cloud and DeepMind's vice president of research, says, "If you can now verify the correctness of these implementations, then you can rest easy." He adds, "You can imagine banks, imagine all those other companies who rely on assurances and who worry about bugs who could now say, 'I can prove these properties.'"

The open question across the tech sector is whether AI-automated formal verification can truly scale, and whether it can do so at a workable cost. 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 has plans to release a commercial formal verification product or service.

The researchers say that some of their crucial advancements are in developing a "human-AI collaboration process," as Chaudhuri puts it, that allows agents to contribute and self-correct at almost every phase of the process while still seeking human input and 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 and basically taking tests that are self-written," he says. "There's a middle ground."