Google DeepMind checks Signal protocol’s cryptographic guarantees

What the researchers checked

Formal verification uses mathematics to establish whether software works as intended and whether it contains critical vulnerabilities. Google DeepMind used AI agents and its new framework, AlphaProof Code, for the task.

The project was a proof of concept, significant in two ways. It provided an independent check of the cryptography protecting a huge volume of messages on Signal, Google Messages and WhatsApp. It also showed how Google DeepMind uses AlphaProof Code for formal verification.

The current interest in AI-assisted formal verification has not settled questions about how practical the approach will be or whether it can reliably check large volumes of code. Supporters of formal verification have long considered it one of the main goals of software security: mathematics can establish whether a program behaves according to specified requirements.

Before AI, specialists had to describe by hand the properties of a program they wanted to prove, translate those descriptions into formulas, and then construct a proof. AI agents can significantly speed up the final part of this work.

The Signal verification was limited, however: the researchers did not prove the security of the entire mobile app. They stressed that the project is just one stage in a much larger effort. DeepMind research scientist Svarat Chaudhuri said there is still a long way to go before all software in the world can be verified, though that is what the company is working toward.

Checking older versions

The team found no new vulnerabilities in the parts of the current protocol it examined. The researchers also tested older versions of Signal that contained known vulnerabilities, fixed long ago. AlphaProof Code correctly flagged them and showed that the protocol in those versions could not be formally verified.

The team is publishing the specification and proof created for the Signal analysis so other formal verification researchers can use them.

Previous work by the Signal Foundation also helped the team complete the project quickly: the foundation had already formally verified parts of the code. Signal CTO Ehren Kret said Google DeepMind’s approach makes it possible to extend that verification substantially. He said rigorous checks of the protocol’s implementation strengthen confidence in Signal’s privacy guarantees amid rising security threats associated with AI.

The scale and cost of verification

For critical services, it would be useful to formally verify every codebase and the entire software supply chain. Pushmeet Kohli, Google Cloud’s chief scientist and DeepMind’s vice president of research, believes such verification would let companies, including banks, prove that their software meets specific requirements and rely on it with greater confidence.

The open question is whether automated AI formal verification can scale to an industry-wide level, and how much it would cost. DeepMind conducted the Signal analysis for free as a research project, but Google has not disclosed its cost. The company also declined to comment on whether it plans to release a commercial product or service for formal verification.

The role of people

The researchers cite human-AI collaboration as one of the process’s key outcomes. Agents can take part in nearly every stage and correct their own mistakes, while human judgment and review remain at important points in the process.

Chaudhuri stressed that DeepMind is not aiming for a situation in which AI sets its own goals, generates proofs and tests itself against tests it has created. He said an intermediate approach involving people is possible.

Dataist’s take: the work shows that AI agents can speed up formal verification of specific parts of a protocol and detect previously known errors. But the Signal check did not cover the entire app, and its cost and commercial viability remain unclear. That leaves open how far this approach can scale beyond a research project.