DeepMind's AI Wrote a Math Proof That Signal's Encryption Holds Up

Google DeepMind researchers have mathematically proven, or formally verified, several core cryptographic guarantees of the Signal protocol, according to WIRED. The proof-of-concept took just four weeks and leaned on a new agentic AI framework called AlphaProof Code. The analysis turned up no new vulnerabilities in the portions of the protocol it examined, and the team is publishing the specification and proof to help other formal verification efforts.

The result matters on two fronts. It offers independent validation of cryptography guarding huge volumes of communications across the Signal app, Google Messages and WhatsApp, and it showcases DeepMind's formal verification capabilities. When researchers pointed AlphaProof Code at older Signal versions containing known, long-fixed bugs, it caught them and showed the protocol could not be formally verified.

DeepMind research scientist Swarat Chaudhuri was blunt about the limits. “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,” he told WIRED. Signal CTO Ehren Kret said in a statement that the approach enables significant expansion over prior verification work on smaller code portions, adding that rigorously verifying the protocol implementation gives greater confidence in the code's privacy guarantees as AI-driven threats grow.

The researchers had a head start thanks to past formal verification work by the Signal Foundation. Even so, the project was narrow — it did not formally verify the entire Signal mobile app. Formal verification has long been treated as a software security holy grail, since it uses math to confirm code behaves as intended, but it was painfully slow before AI arrived to automate the proof-building step.

Pushmeet Kohli, chief scientist at Google Cloud and DeepMind's vice president of research, pitched the upside for high-stakes settings. “If you can now verify the correctness of these implementations, then you can rest easy,” he said, imagining banks and other companies that could say, “I can prove these properties.” Whether AI-automated verification can scale at a workable cost remains open: DeepMind ran the Signal analysis free as research, Google declined to share its cost, and it wouldn't say whether a commercial verification product is coming.

The team says a key advance is a human-AI collaboration process that lets agents contribute and self-correct at nearly every stage while still pulling in human review at critical points. “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 said. “There's a middle ground.”