DeepMind Formally Verifies Signal in 4 Weeks

Google DeepMind has formally verified key elements of the Signal protocol using an agentic AI and a new framework, AlphaProof Code. The team publishes its proofs without having discovered any new vulnerabilities, while acknowledging scalability limits and unknowns regarding economic viability.

Costs, commercial product, and scaling remain uncertain

The ability of automated formal verification by AI to scale effectively and at a viable cost remains an open question in the tech sector. DeepMind conducted a free analysis of the Signal protocol as part of a research project. Google declined to disclose the cost of this analysis and did not specify whether it is considering a commercial formal verification product or service.

A human-in-the-loop approach claimed by DeepMind

Researchers describe a collaborative process between humans and AI, where agents contribute and self-correct at nearly every phase while seeking human intervention at key moments. Swarat Chaudhuri, a researcher at DeepMind, rejects the idea of a system where AI sets its own goals and generates proofs without human oversight, preferring a balance between AI autonomy and human supervision. Before AI, specifying and formally proving software properties was very time-consuming for humans, and agentic AI helps reduce this time. However, DeepMind clarifies that the analysis does not cover the Signal mobile application in its entirety and presents these results as a step in a broader process, emphasizing that generalizing this approach to all software will take time.

What DeepMind verified, with AlphaProof Code in 4 weeks

DeepMind used agentic AI to formally verify several cryptographic guarantees of the Signal protocol. Conducted over four weeks and based on the AlphaProof Code framework, the evaluation revealed no new vulnerabilities in the examined parts. In older versions of Signal containing known and fixed vulnerabilities, the tool correctly identified the issues, demonstrating that these versions could not be formally verified. The researchers are publishing the specification and proof developed to support further verification work.

Why this matters for messaging and beyond

This step provides additional independent validation for the cryptography used by services like Signal, Google Messages, and WhatsApp. DeepMind indicates that it benefited from prior formal verification work conducted by the Signal Foundation. Ehren Kret, Chief Technology Officer of Signal, emphasizes that previous verifications focused on smaller portions of the code, while DeepMind's approach allows for significant expansion and enhances trust in privacy guarantees as AI-related threats increase. Proponents of formal verification often refer to it as the "Holy Grail," as it relies on mathematical methods to demonstrate the absence of critical flaws. For high-stakes services, the optimal goal would be to apply formal verification to every source code as well as all software supply chains. According to Pushmeet Kohli, Chief Scientist at Google Cloud and Vice President of Research at DeepMind, having such technology could provide additional assurance to sectors like banking, which seek to demonstrate certain essential properties of their systems. However, the industrialization and large-scale efficiency of these methods remain to be established.