Key facts
- DeepMind said the four-week project used a new AI framework called AlphaProof Code to prove Signal protocol guarantees.
- The analysis found no new vulnerabilities in the portions of the Signal protocol it examined.
- Run on older Signal versions with known, long-fixed flaws, AlphaProof Code identified them and showed the protocol could not be formally verified.
- DeepMind research scientist Swarat Chaudhuri said there is a long distance to go before scaling this to all software.
- The analysis did not formally verify the entire Signal mobile app, DeepMind said.
- DeepMind released the specification and proof it developed for the Signal analysis.
Google DeepMind researchers used agentic AI to mathematically prove, or formally verify, a number of the Signal protocol's key cryptographic guarantees, the lab said in work dated November 11, 2026. The project ran as a proof-of-concept over four weeks and used a new AI framework called AlphaProof Code, according to DeepMind.
DeepMind said the work serves as further independent validation of the cryptography protecting communications on platforms including the Signal app, Google Messages and WhatsApp. It also demonstrates the lab's formal verification capabilities using AlphaProof Code.
Formal verification uses math to check that software functions as intended, meaning it has no critical vulnerabilities. Before the AI era, describing the properties to be proven, turning them into formulas and developing the proof was time-consuming for people; agentic AI can cut down the time needed for the proof stage, the report said.
The analysis was limited in scope and did not formally verify the entire Signal mobile app. DeepMind said it found no new vulnerabilities in the portions of the protocol it examined. When the researchers ran AlphaProof Code on older versions of Signal containing known and long-fixed vulnerabilities, it correctly identified them and showed the protocol could not be formally verified.
"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," DeepMind research scientist Swarat Chaudhuri told WIRED.
The researchers are releasing the specification and proof they developed for the Signal protocol analysis to aid other formal verification work. The report said it is unclear how practical AI-aided formal verification will be for widespread use and how effective it can be at securing large amounts of code.