AI Formally Verifies Signal Protocol in Four-Week Project

Google DeepMind researchers used agentic AI to mathematically prove key cryptographic guarantees of the Signal protocol in a four-week project. The proof-of-concept, using a new AI framework called AlphaProof Code, provided independent validation of the cryptography protecting communications on Signal, Google Messages, and WhatsApp.

Researchers found no new vulnerabilities in the sections they examined. The work demonstrates formal verification capabilities using AlphaProof Code. The analysis validated cryptographic guarantees in the protocol. DeepMind released the specification and proof from the analysis to support other formal verification work.

Human-AI collaboration model

Researchers employed a human-AI collaboration process where AI agents contribute and self-correct through most stages, while seeking human review at key junctures. Swarat Chaudhuri, a DeepMind research scientist, said they did not want AI to generate both goals and proofs and test itself, emphasizing a middle ground. This agentic AI approach can reduce the time needed for formal verification tasks, which before AI was extremely time-consuming due to manual formula translation and proof development.

Limitations and scaling challenges

The project was limited in scope, not formally verifying the entire Signal mobile app. The DeepMind analysis did not find new vulnerabilities in the portions of Signal it examined. AlphaProof Code identified known, long-fixed vulnerabilities in older Signal versions and showed the protocol could not be formally verified in those cases.

DeepMind researchers emphasized their findings are a milestone in a larger process, not a complete verification. Chaudhuri stated the result was encouraging but scaling remains a long way off. Whether AI-automated formal verification can scale at a workable cost for large codebases remains an open question.

Industry implications and cost model

The project was conducted free of charge as a research project, with Google declining to share costs or comment on commercial plans. Ehren Kret, Signal's chief technology officer, said the approach enables significant expansion beyond prior formal verification focused on smaller code portions. He added that rigorously verifying the Signal protocol implementation gave Signal greater confidence in its code’s privacy guarantees as AI-driven security threats grow.

Pushmeet Kohli, Google Cloud chief scientist and DeepMind vice president of research, said verifying implementations allows companies to 'rest easy' about security and could give organizations like banks confidence in correctness. The project benefited from earlier formal verification work by the Signal Foundation. The four-week duration and free research model highlight the current practical constraints of AI formal verification.