AlphaProof Code: DeepMind agents verify Signal's compiled code in Lean

01What happened

Google DeepMind introduced AlphaProof Code on 10 November 2026, in a post by Pushmeet Kohli and Swarat Chaudhuri that comes with a technical paper and open-sourced proof artifacts. The team applied it to libsignal-cli, a command-line harness wrapping unmodified libsignal v0.105.4 and SPQR v1.6.0, and reports the work took four weeks where expert teams have historically needed years. DeepMind states this is the first time the implementation of a widely deployed protocol has been formally verified by any method.

02How it works

Human experts choose the properties to prove, specifications are drafted with a mix of models and reviewed by people, and agents running on Gemini Carbon write the proofs in Lean, whose kernel checks each one. The proofs reason about the AArch64 executable rather than the protocol design, using modelled semantics for 467 instructions and 31 system calls. DeepMind reports over six million lines of generated Lean standing on about 26,000 lines of specification and semantics that humans have to trust, alongside cryptographic primitives the proofs assume secure.

03Who is affected

Coverage is narrow and stated in the paper: the init handshake, send and recv for one-to-one sessions, with ten symbolic theorems for forward secrecy, authentication, post-compromise security and handshake secrecy. Signal and Google Messages users have nothing to install. The exclusions are listed below and include key generation and group messaging.

04What to do

Read the published specifications before treating the result as a guarantee, because each theorem holds only for the operations and assumptions the paper lists. Teams that want to try the same approach can take the Lean development and the proofs from the project page, which DeepMind has open-sourced.

Questions people ask

Does AlphaProof Code prove that Signal is secure?

AlphaProof Code proves named properties of named operations, not blanket security. The Lean theorems cover the handshake, send and recv in one-to-one sessions of libsignal-cli, and they assume Lean's kernel, the modelled AArch64 semantics and idealized cryptographic primitives are sound. Group messaging, multi-device state, key generation and quantum attackers in the computational proof sit outside what DeepMind proved.

Which Signal code did Google DeepMind actually verify?

The target is libsignal-cli, a command-line harness that wraps unmodified libsignal v0.105.4 and SPQR v1.6.0 and is compiled with stock rustc into an AArch64 Linux executable. DeepMind says the proofs therefore reach the compiled code that runs on devices, which is where implementation flaws usually appear, rather than covering the protocol design alone.

How did DeepMind test that the proofs catch real bugs?

DeepMind reintroduced two previously fixed libsignal bugs into an isolated copy of the code, and in both cases the system produced a machine-checked proof that the buggy build violated the symbolic security theorems. Signal's CTO, Ehren Kret, calls the translation of live code into valid Lean theorems a major breakthrough, which is Signal's own assessment rather than an independent review.

Sources 3 links, all fetched

1. 1deepmind.googleDeepMind Announcement
2. 2deepmind.googleTechnical Paper
3. 3google-deepmind.github.ioProof Artifacts