Google DeepMind researchers have used an agentic AI to mathematically demonstrate several key cryptographic guarantees of the Signal protocol. Conducted over four weeks as a proof-of-concept project, this work relies on a new AI framework called AlphaProof Code.
The Signal protocol provides the encryption for the Signal application, and also, according to the source, for Google Messages and WhatsApp. For the article, this demonstration constitutes a new independent validation of this cryptography, which protects a vast quantity of messages worldwide. It also illustrates Google DeepMind’s formal verification capabilities.
Formal verification involves using mathematics to check that software functions as intended, meaning it contains no critical flaws. Its proponents have long considered it the holy grail of software security. But its large-scale use remains uncertain, as does its effectiveness against large volumes of code.
A Targeted Analysis
Before the AI era, it took considerable time to describe a software’s characteristics, transform these descriptions into formulas, and then develop the proof. According to the source, agentic AI can significantly reduce the duration of this last step. However, the scope of the analysis remains limited: it did not, for example, formally verify the entire Signal mobile application.
In the parts of the protocol examined, the researchers found no new vulnerabilities. Conversely, when they applied AlphaProof Code to older versions of Signal containing long-known and fixed flaws, the tool correctly identified them and showed that the protocol could not be formally verified in those versions. The researchers are publishing the specification and proof developed for the Signal protocol analysis to facilitate other formal verification work.
The speed of the project is partly due to prior work by the Signal Foundation in this area, as the DeepMind researchers note. ‘While previous formal verification focused on smaller portions of the code, the Google DeepMind approach allows for significant extension,’ says Ehren Kret, Signal’s CTO, in a statement. ‘As AI-related security threats multiply, rigorously verifying the Signal protocol implementation gives us even greater confidence in the privacy guarantees of our code.’
A Question of Cost and Scale
For critical services used in high-stakes contexts, being able to formally verify every codebase and all software supply chains would be, according to Pushmeet Kohli, Chief Scientist at Google Cloud and VP of Research at DeepMind, a major breakthrough. ‘If we can now verify the correctness of these implementations, we can be at ease. Imagine banks, and all the other companies that rely on guarantees and worry about bugs, now being able to say: “I can prove these properties,”‘ he says.
The question remains, open for the entire tech sector, of whether AI-automated formal verification can truly scale at a reasonable cost. DeepMind conducted the Signal analysis for free, as a research project, and Google did not wish to disclose its cost. The company also did not specify whether it plans to commercialize a formal verification product or service.
The researchers believe some of their crucial advances lie in a ‘human-AI collaboration process,’ in the words of Swarat Chaudhuri, a research scientist at DeepMind. This process allows the agents to contribute and self-correct at almost every step, while seeking human input and validation at key moments. ‘We don’t want that world of vibe, where the AI sets the goals, the AI produces the proofs, and you pass tests it wrote itself. There is a middle ground.’
