Google DeepMind researchers have used agentic AI to mathematically prove several key cryptographic guarantees of the Signal protocol.
This work, completed in four weeks as a proof-of-concept, validates the cryptography protecting communications on Signal, Google Messages, and WhatsApp. It also demonstrates the capabilities of a new AI framework called AlphaProof Code.
AI-aided formal verification is currently generating interest, though its practicality for widespread use remains unclear. Proponents view formal verification as the holy grail of software security. The method uses mathematics to check that software functions as intended and lacks critical vulnerabilities.
Before the AI era, describing software characteristics, converting them into formulas, and developing proofs took immense time. Agentic AI reduces the time required for these later stages, enabling analyses like DeepMind’s Signal evaluation. The analysis was limited in scope; it did not formally verify the entire Signal mobile app. Researchers emphasise these findings are 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, tells WIRED.
The DeepMind analysis found no new vulnerabilities in the portions of the Signal protocol it examined. When researchers applied AlphaProof Code to older versions of Signal containing known, long-fixed vulnerabilities, the tool correctly identified them and showed the protocol could not be formally verified. The team is releasing the specification and proof to aid other formal verification work.
Researchers note they gained a head start because the Signal Foundation has conducted past formal verification work.
“While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach enables significant expansion,” Ehren Kret, Signal’s chief technology officer, says in a statement. “As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees.”
For critical services in high-stakes settings, formally verifying every codebase and software supply chain would be ideal. “If you can now verify the correctness of these implementations, then you can rest easy,” says Pushmeet Kohli, chief scientist at Google Cloud and DeepMind’s vice president of research. “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 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 or comment on plans to release a commercial formal verification product or service.
Researchers say crucial advancements include a “human-AI collaboration process,” as Chaudhuri puts it. This allows agents to contribute and self-correct at almost every phase while 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,” Chaudhuri says. “There’s a middle ground.”
What it means
Developers of secure messaging apps can now rely on independent mathematical proof for specific parts of their code rather than just trusting internal audits. The project shows that AI can accelerate the creation of these proofs, but it does not mean every piece of software is currently being checked this way. The technology is still in the research phase.
