Google DeepMind Uses AI Tool to Formally Verify Key Guarantees of the Signal Protocol

The work, a proof-of-concept that took four weeks, did not turn up any new vulnerabilities in the parts of the protocol it examined. As a check on the method, the team ran AlphaProof Code against older versions of Signal that contained known, long-since-fixed flaws. The tool found those flaws and showed that those versions could not be formally verified, Wired reported.

The result matters beyond messaging apps. Formal verification uses mathematics to prove that software behaves as specified, and security engineers have long seen it as the strongest assurance available. It has rarely been used at scale because people had to describe the properties they wanted to prove, translate them into formulas and then write the proofs by hand. DeepMind's project shows AI agents taking on much of that work, though the researchers stress it covered only part of the system. It did not verify the whole Signal mobile app, for example.

"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," Swarat Chaudhuri, a DeepMind research scientist, told Wired.

The researchers said they got a head start from formal verification work the Signal Foundation had already done on smaller parts of its code. They are releasing the specification and proof from the Signal analysis so that others can build on it.

Ehren Kret, Signal's chief technology officer, said in a statement that earlier verification efforts "focused on smaller portions of the code" and that DeepMind's approach "enables significant expansion." He added: "As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees."

Pushmeet Kohli, DeepMind's vice president of research and chief scientist at Google Cloud, pointed to regulated industries as likely users. "You can imagine banks, imagine all those other companies who rely on assurances and who worry about bugs who could now say, 'I can prove these properties,'" he told Wired.

The researchers described their main advance as a process for humans and AI to work together, in which agents propose and correct work at most stages while people review it at key points. Chaudhuri said the team wanted to avoid a setup where AI writes both the goals and the proofs, comparing that to "taking tests that are self-written."

Cost is the main unanswered question. DeepMind did the Signal analysis free of charge as a research project, and Google declined to say what it cost or whether it plans to sell formal verification as a product or service. Whether AI-automated verification can cover large codebases and whole software supply chains at a price companies will pay is still unproven. The Signal specification and proof are the first public material outside researchers can use to test DeepMind's claims.