Google DeepMind has used AI agents to produce a mathematical proof that the code behind the Signal protocol delivers the security it promises, in a project the company calls a milestone for software security.
The work, announced on 10 November, used a new system called AlphaProof Code to verify the actual compiled code of libsignal, the open-source library that implements the Signal protocol. The same protocol protects conversations in Signal itself, as well as in WhatsApp and Google Messages.
AlphaProof Code is a multi-agent framework that divides the work the way a research team would. Human experts worked with AI models to turn Signal’s security goals into formal mathematical specifications, reviewing every one. Agents powered by Gemini Carbon then did the proving, generating more than six million lines of Lean, a language whose checker verifies each step automatically. The agents then audited their own output, flagging only about one per cent of the codebase for a second human look.
The proof covers the post-quantum PQXDH handshake that sets up a conversation and the Triple Ratchet that rotates the key for every message, in libsignal version 0.105.4 with SPQR version 1.6.0. It establishes four properties for one-to-one sessions: forward secrecy, authentication, post-compromise security and handshake secrecy. Crucially, the verification reaches down to the compiled AArch64 machine instructions, rather than stopping at the protocol’s design on paper.
DeepMind says the whole effort took four weeks with a team of five researchers, a task that has historically taken expert teams years. 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 buggy version was insecure.
The limits matter as much as the achievement. The proof covers one-to-one sessions only; group messaging is left for future work. It applies to a single compiled build running in a test harness, not to the full Signal app on a phone, and it does not cover key generation, sealed sender, server-side code or side-channel attacks. The underlying cryptographic building blocks are assumed sound rather than proved. Even so, Signal’s chief technology officer, Ehren Kret, said the work gives the company even greater confidence in its code’s privacy guarantees.
DeepMind has open-sourced the verification artefacts and published a technical paper alongside the announcement. The company says the same techniques could eventually be applied to other critical systems, from medical device firmware to power grid software, and paired with automated defence agents to counter the speed and scale of modern cyber threats.
Sources: Google DeepMind, “Formal Verification of Signal’s Protocol with Gemini” (10 November 2026), https://deepmind.google/blog/introducing-alphaproof-code/; The Register, “Google DeepMind melds humans and AI agents to vet Signal’s secure messaging techniques” (10 November 2026).
