TL;DR
A Google DeepMind team has used AI agents to produce mathematical proofs that several core cryptographic guarantees of the Signal protocol hold, WIRED reported on 10 November. The proof-of-concept took four weeks and used a new framework called AlphaProof Code. It found no new flaws in the parts it examined, but correctly caught known, long-fixed vulnerabilities when run against older versions of the protocol.
What was done
Formal verification uses mathematics to show that software behaves as intended. Security specialists have long prized it, but it is slow: people have to describe the properties they want proved, turn them into formulas and then build the proof. DeepMind’s work uses AI agents to shorten that last step.
The scope was limited. The team did not verify the whole Signal mobile app, and the researchers describe the result as one milestone among many. The team is publishing its formal specification and the proof itself so others can build on them, and they say earlier verification work by the Signal Foundation gave them a head start. The Signal protocol also protects messages in WhatsApp and Google Messages, which is why the result matters beyond one app.
Signal’s CTO, Ehren Kret, said in a statement that DeepMind’s approach “enables significant expansion” beyond earlier, narrower verification efforts.
The open questions
The big unknown is cost and scale. DeepMind ran the Signal work at no charge, as research. Google would not give its cost, nor say whether it plans to sell verification as a product or service.
Swarat Chaudhuri, one of DeepMind’s research scientists, said the team’s progress rests on a “human-AI collaboration process” in which agents work and self-correct through most stages while humans review key points. “We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs,” he said. Pushmeet Kohli, who runs research at DeepMind as a vice president, suggested banks and other firms that “worry about bugs” could one day prove properties of their own code.
What it means
This is the defensive counterpart to stories we have covered on the attack side, such as OpenAI’s automated exploit pipeline.
In our view, the human-in-the-loop design is the most transferable part. For UK banks, insurers and critical infrastructure operators, AI-assisted proof could eventually support assurance on the most sensitive code, such as payment and authentication systems. Until the cost is public, though, it is a research signal rather than a tool to budget for.