# Google DeepMind Uses AI to Formally Verify the Signal Protocol, Producing 6.5 Million Lines of Proofs in Four Weeks

*2026-11-12 15:01 UTC · AI · 1 min read*

> DeepMind's AlphaProof Code produced machine-checked proofs of Signal's core security properties, though only for one-to-one chats.

Google DeepMind has used a new system called AlphaProof Code to produce machine-checked mathematical proofs of security properties in the Signal messaging protocol. Announced on November 10, the work covered message confidentiality, authentication, forward secrecy and post-compromise security, and the proofs are checked by the Lean proof system, including about 140,000 instructions of compiled machine code.

Five researchers generated roughly 6.5 million lines of proofs in four weeks, work that has historically taken specialist teams years. To test the method, DeepMind reinserted two previously fixed Signal vulnerabilities into test versions, and the system produced proofs showing both modified versions violated their security requirements.

The scope is limited: only one-to-one conversations were covered, not group messaging, multi-device use or the whole mobile app, and a proof only checks the requirements it is given. Google has published the proofs and specifications on GitHub, and says there is no commercial service yet.

## Sources

- [theneuron.ai](https://www.theneuron.ai/news/google-ai-math-signal-security-verification/)
- [github.com](https://github.com/google-deepmind/code-verification)

---
TechTools News · https://techtools.cz/tools/news/article/2678-google-deepmind-uses-ai-to-formally-verify-the-signal-protocol-producing-6-5
Česká verze: https://techtools.cz/tools/news/clanek/2752-google-deepmind-formalne-overil-protokol-signal-pomoci-ai-6-5-milionu-radku