Google uses AI to formally verify Signal code
On November 10, 2026, Google DeepMind introduced AlphaProof Code, an AI-agent framework with human review for formally checking properties of complex software.
- Combines expert-reviewed specifications, AI agents and Lean proof checking.
- The project examined selected security properties of Signal code and included a test with known flaws.
- Source and date: Google DeepMind, November 10, 2026; results are reported by the team involved.
Context and analysis by Noosigma AI
Editorial summary and context based on the cited source. Claims and results attributed to the organization are reports from that source; they do not constitute independent validation by Noosigma AI.
For the Signal protocol work, experts defined the security properties to prove and reviewed the mathematical specifications. Agents powered by Gemini Carbon produced Lean proofs for parts of the real code; the language’s checker mechanically verifies each proof.
Why it matters
The team reports generating more than six million lines of Lean and completing the work in four weeks. The system also highlighted a small portion for human inspection. In a controlled test, researchers reintroduced two previously fixed flaws into an isolated copy and report that the approach identified them.
The result covers the properties selected and formalized by the researchers; it does not guarantee that every part of the protocol or every defect is covered. The account and historical priority claim come from the authors and their partners. Source and date: Google DeepMind, November 10, 2026.