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

Google DeepMind researchers used an agentic AI framework called AlphaProof Code to formally verify several core cryptographic guarantees of the Signal protocol. The proof-of-concept project took about four weeks and is being presented as a landmark both for the encryption that protects large volumes of communications across Signal, WhatsApp and Google Messages, and for AI's role in formal verification.

Formal verification uses mathematics to confirm that software behaves as intended, a practice long described as a holy grail of software security because it can establish correctness rather than merely test for bugs. Before the AI era, defining the desired properties, translating them into formulas and constructing the proofs was extremely time-consuming for people; agentic AI can substantially cut the proof-building stage, which is what made DeepMind's evaluation feasible on that timeline.

The analysis turned up no new vulnerabilities in the portions of the Signal protocol it examined, though it did not formally verify the entire Signal mobile app. When the researchers applied AlphaProof Code to older Signal versions carrying known, long-fixed vulnerabilities, it correctly identified them and showed the protocol could not be verified at those points. DeepMind is releasing the specification and proof it produced to help other formal verification efforts.

The team got some of a head start from formal verification the Signal Foundation had already done, and Signal chief technology officer Ehren Kret said that prior work covered smaller portions of the code while DeepMind's approach enables significant expansion. Kret added that verifying the protocol implementation gives the organization greater confidence in its privacy guarantees as AI-driven security threats grow. Google Cloud chief scientist and DeepMind vice president of research Pushmeet Kohli pointed to banks and other organizations that rely on assurances as potential users of provable correctness.

DeepMind research scientist Swarat Chaudhuri described a human-AI collaboration process in which agents contribute and self-correct at almost every phase while humans are still consulted at key junctures, framing it as a middle ground against a "vibe world" where AI writes both the goals and the proofs. What remains open is whether AI-automated formal verification can scale to large code bases at a workable cost: the Signal analysis was done free of charge, Google declined to share what it cost, and the company would not say whether a commercial verification product is planned. Chaudhuri said a long distance remains before the method can scale to "all the software of the world."