Google DeepMind says its new AlphaProof Code framework used AI agents to mathematically prove key security properties of the actual code behind the Signal protocol — the encryption that protects private conversations in Signal and Google Messages — in just four weeks. Why it matters: formal verification is the strongest form of security assurance there is, and DeepMind says this is the first time a widely deployed cryptographic protocol’s implementation has been verified at this depth, by AI or by any other method.
November 10, 2026
What happened
DeepMind introduced AlphaProof Code on November 10, describing it as a multi-agent framework for formal verification — proving mathematically that code does what it is supposed to do, rather than testing it and hoping no bug was missed. Human researchers worked with models to turn Signal’s security goals into formal specifications, reviewing every one. Agents powered by Gemini Carbon then did the proving, generating more than six million lines of Lean, the language used to write machine-checked proofs. The agents also audited their own work and flagged about one percent of the code for a closer human look.
Why verifying the code, not the design, is the hard part
Most protocol verification stops at the design. AlphaProof Code went further, proving that Signal’s compiled code — down to the machine instructions that actually run — delivers properties such as keeping earlier messages protected if a device is later compromised, and recovering security after a compromise. That design-to-implementation gap is exactly where real-world vulnerabilities tend to hide, which is why work of this kind has historically taken expert teams years. The verified target was Signal’s one-to-one session code, covering its post-quantum handshake and its message ratcheting.
To check the system could tell good code from bad, the team reintroduced two real, previously fixed bugs into an isolated copy of the code. In both cases AlphaProof Code produced a machine-checked proof that the altered version was insecure.
What it does not prove
The result is not a blanket guarantee that the Signal app can never be broken. Key generation was not verified, group messaging was left for future work, and the proof covers the core cryptographic code in the researchers’ build rather than every part of the apps people install. DeepMind has open-sourced its verification artifacts so outside reviewers can check the work, and Signal’s chief technology officer said the project gives the company even greater confidence in its code’s privacy guarantees.
Why it matters
For subscribers, the practical takeaway is twofold. First, the encryption underneath billions of conversations just passed an unusually rigorous, independently checkable examination — and passed it. Second, the method matters as much as the result: if AI agents can compress years of verification work into weeks, the same approach could bring proof-grade assurance to other critical software, from medical devices to power-grid systems, at a moment when AI is also making attacks faster. That is the “everything AI, tested” angle in its purest form — here, the test is a mathematical proof, and anyone can re-run the checker.
Frequently asked questions
What is AlphaProof Code?
It is Google DeepMind’s agentic framework for formal verification. Humans and AI together define what a piece of code must guarantee; teams of AI agents then construct machine-checked proofs in Lean that the code meets those guarantees.
What exactly was verified in Signal?
Key security properties of Signal’s core one-to-one cryptographic code — its post-quantum handshake and message ratcheting — at the level of the compiled implementation, not just the protocol design.
Does this mean Signal is unhackable?
No. Key generation and group messaging were not covered, and the proof applies to the specified properties of the core code. It raises confidence substantially; it does not certify the whole app against every possible attack.
How long did the verification take?
Four weeks, according to DeepMind — work the company says has historically taken expert teams years. The agents produced more than six million lines of Lean proof in the process.
Sources: Google DeepMind, Unite.AI