Google DeepMind uses AI to prove key security guarantees of the Signal protocol

Key cryptographic promises behind the Signal protocol now have another mathematical check behind them. Google DeepMind researchers used an AI framework called AlphaProof Code to verify those guarantees in a four-week research project, WIRED reported. The result adds assurance about the portions examined, but it is not proof that the entire Signal app is secure.

A mathematical check, with a defined scope

Formal verification uses mathematics to establish that software meets specified requirements. Engineers describe the properties they want to check, translate those descriptions into formulas, and develop a proof. That makes defining the requirements a separate task from proving that the software satisfies them.

The stakes extend beyond one messaging app. The Signal protocol underpins encrypted communications in Signal, Google Messages and WhatsApp. DeepMind’s project focused on a number of its key cryptographic guarantees, adding independent validation of protections used across those services.

The researchers checked both the protocol portions they wanted to validate and older versions with already-known weaknesses. According to WIRED, the two exercises produced different results:

• In the portions examined for the main analysis, the team found no new vulnerabilities and formally verified the selected guarantees.
• In older versions containing known, long-fixed vulnerabilities, AlphaProof Code identified the flaws and showed that the protocol could not be formally verified.

The team is releasing its specification and proof to support other verification work. Those are the descriptions and mathematical evidence developed for this analysis, rather than a claim to have checked every part of the messaging service.

We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written,

Swarat Chaudhuri, Google DeepMind research scientist, speaking to WIRED

People still decide what gets proved

DeepMind describes the workflow as human-AI collaboration, not an autonomous replacement for security researchers. Agents contribute and correct their work at almost every phase, while people provide input and review at key points. Chaudhuri presented that division of work as a middle ground between manual verification and AI setting and passing its own tests.

The four-week schedule also had a foundation in earlier research. DeepMind’s team said prior formal-verification work by the Signal Foundation gave it a head start. Signal chief technology officer Ehren Kret said that earlier work covered smaller portions of the code, while DeepMind’s approach allowed a significant expansion.

Four weeks is not a price tag

The project’s duration offers a concrete example of a short verification effort, but its economics remain undisclosed. DeepMind conducted the Signal analysis free of charge as research. Google declined to tell WIRED what the work cost or whether it intends to offer a commercial formal-verification product or service.

That leaves a practical question beyond whether AI can help construct proofs: can the process cover much larger amounts of software at a workable cost? Formal verification has historically required substantial human effort, from describing the intended behavior to building the proof. AI can shorten the proof-building work, but widespread use remains uncertain.

DeepMind’s ambition reaches well beyond messaging. Chaudhuri told WIRED the team wants to scale verification to all software, while emphasizing that it remains a long way from that goal. For now, the concrete result is a bounded research demonstration, with a specification and proof for others to build on.