Google DeepMind has built an artificial intelligence system that mathematically verified key security properties of the Signal protocol, the encryption technology that protects billions of private conversations in apps such as Signal, WhatsApp, and Google Messages. The system, called AlphaProof Code, was described in a company announcement and a technical paper, and reported by Ars Technica.
The work concerns formal verification, a method to prove that software behaves exactly as intended. Such proofs give the highest standard of security assurance, but they are slow and expensive. AlphaProof Code is a multi-agent framework: teams of AI agents, guided by human experts, write formal specifications of what the code must do, then prove that the code meets them. Every proof is checked by Lean, a widely used proof-checking program.
What the verification covered
The team verified libsignal, Signal's reference implementation, down to the compiled machine code that actually runs on devices. The agents produced about 6.5 million lines of machine-checked proof, resting on roughly 26,000 lines of trusted specifications. The whole process took four weeks, a task the researchers say would historically take expert teams years. To test the system, the researchers reintroduced two real, previously fixed bugs; in both cases AlphaProof Code proved the buggy versions insecure. The work did not verify the entire Signal app, and the researchers stress it is one milestone in a longer process.
This matters because most cryptographic verification stops at the design level, while real-world flaws often hide in the gap between design and running code. These are the first proofs connecting protocol-level security guarantees to the unmodified, widely deployed code of a major cryptographic protocol. If AI can make formal verification fast and cheap enough, the same approach could bring mathematical assurance to banks, medical devices, and power grid software. DeepMind is releasing its specifications and proofs to support further work.