Google DeepMind researchers used agentic AI to mathematically prove several key cryptographic guarantees of the Signal protocol. The four-week proof-of-concept project utilized a new AI framework called AlphaProof Code to perform formal verification, a process that uses mathematics to validate that software functions as intended without critical vulnerabilities.
The analysis did not uncover new vulnerabilities in the specific portions of the Signal protocol examined. However, when researchers applied AlphaProof Code to older versions of Signal containing known, long-fixed vulnerabilities, the AI correctly identified the flaws and demonstrated that those versions could not be formally verified. The researchers are releasing the specification and proof developed during the analysis to assist further formal verification efforts.
While the project demonstrated the ability of AI to significantly reduce the time required to develop mathematical proofs, researchers noted the scope was limited and did not include the entire Signal mobile app. Swarat Chaudhuri, a DeepMind research scientist, said, “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.”
Signal's chief technology officer, Ehren Kret, stated that while prior formal verification efforts focused on smaller code segments, the DeepMind approach allows for significant expansion. Kret added that as AI-driven security threats increase, rigorous verification provides greater confidence in the protocol's privacy guarantees.
Google Cloud and DeepMind vice president of research and chief scientist Pushmeet Kohli suggested that the ability to verify implementations could provide essential assurances for high-stakes industries like banking. Despite the successful test, it remains unclear if AI-automated formal verification can scale to entire software supply chains at a workable cost. Google declined to comment on whether it plans to release a commercial formal verification product or service.
