DeepMind’s AlphaProof Code formally verifies the Signal protocol’s code
Google DeepMind said a team of AI agents proved key security properties of the compiled code behind the Signal protocol in four weeks, with human experts writing and reviewing the specifications.
Source published · In the Daily Brief of 11 November 2026
Filed under Agents, Mathematics, AI safety
AlphaProof Code splits formal verification in two. Human experts work with language models to turn Signal’s security goals into formal specifications, each one reviewed by a person. Agents running on Gemini Carbon then write the proofs, which came to more than six million lines of Lean, and flag the parts that need a human look, about 1% of the code according to DeepMind.
The proofs cover the implementation rather than only the design, including protection of messages before and after a device is temporarily compromised. DeepMind said it is the first time the implementation of a widely deployed protocol of this kind has been formally verified by any method. As a check, the team reintroduced two real, long-fixed bugs into an isolated copy of the code, and in both cases the system produced a machine-checked proof that the buggy version was insecure.
The work did not cover the whole Signal app, and Google did not disclose its cost, Wired reported. The specification and proofs are being released.