Overview
- DeepMind announced on Nov. 10, 2026 that its new agentic framework AlphaProof Code used Gemini Carbon models to generate over six million lines of Lean proofs that verify key security properties of portions of the Signal protocol implementation.
- The company open‑sourced the formal specifications and proofs so other researchers can inspect the work and build on the results.
- The verification covered selected implementation code rather than the entire Signal mobile app and found no new vulnerabilities in the reviewed sections.
- To test the system, DeepMind reintroduced two real, long‑fixed bugs into older Signal code and showed the AI produced machine‑checked proofs that those buggy versions failed the security specifications.
- Researchers say the project shows how human experts and AI agents can split the heavy theorem‑proving work, but they caution that questions remain about the computational cost, how to scale the method to full apps and large codebases, and whether this will become a paid service.