Google DeepMind researchers used agentic artificial intelligence to mathematically prove a number of the Signal protocol's key cryptographic guarantees, marking a development for both the widely used encryption standard and AI-assisted formal verification. The researchers completed the project in four weeks using a new AI framework called AlphaProof Code, according to a report published Tuesday.
The analysis serves as independent validation of the cryptography that protects communications on platforms including the Signal app, Google Messages, and WhatsApp. The DeepMind analysis did not find any new vulnerabilities in the portions of the Signal protocol it examined. When researchers tested AlphaProof Code on older versions of Signal containing known and previously fixed vulnerabilities, the system correctly identified them and showed that those versions could not be formally verified. The researchers are releasing the specification and proof they developed to aid other formal verification work.
Formal verification uses mathematics to validate that software functions as intended without critical vulnerabilities. Before AI assistance, the process was time-consuming, requiring people to describe software characteristics, convert them into formulas, and develop proofs. Agentic AI can significantly reduce the time required for this work. The DeepMind analysis was limited in scope and did not formally verify the entire Signal mobile app. The researchers were able to accelerate their work partly because the Signal Foundation has conducted some past formal verification work on smaller portions of the code.
"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, said in a statement. DeepMind researchers say they developed a human-AI collaboration process that allows AI agents to contribute and self-correct at almost every phase while seeking human input and review at key points. The researchers emphasized their findings represent one milestone in a larger process, and questions remain about whether AI-automated formal verification can scale across the technology sector at a workable cost. Google declined to share the cost of the analysis or comment on plans for a commercial formal verification product.