Google DeepMind's AlphaProof Code formally verifies Signal's protocol down to machine code

AlphaProof Code splits the job the way a research team would. A specification-writer agent works with a human to turn security models and properties into a Lean specification, reviewer agents critique each draft, and the human approves the result[2]. The unmodified Rust code is compiled with the standard compiler and loaded into Lean alongside a formal semantics of AArch64 machine code. A team of prover agents then proves the specification, and a gatekeeper agent accepts a proof only if Lean's kernel checks it against a held-out copy of the specification[2].

DeepMind says agents powered by Gemini Carbon generated the proofs, then audited them and flagged about one per cent of the codebase for a second human look[1].

Applied to libsignal, the agents produced about 6.5 million lines of machine-checked Lean proof code, resting on about 26,000 lines of trusted specifications and AArch64 semantics[2]. The proofs cover Signal's post-quantum PQXDH handshake and Triple Ratchet, establishing forward secrecy, authentication, post-compromise security and handshake secrecy, in both the symbolic and computational models of protocol security[2].

Most protocol verification stops at the design. Here the proofs reach the compiled code that runs on devices, where real vulnerabilities often hide. DeepMind says the verification took four weeks, against years for expert teams with earlier tools[1]. As a check, the team reintroduced two real, previously 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[1].

The results trust Lean's kernel, the approved specifications, the security of the underlying cryptographic primitives and the contracts of some routines the executable calls[2]. The target is libsignal linked into a small command-line harness and compiled for AArch64 Linux[2]. The full Lean development is on GitHub, and rebuilding and kernel-checking every proof takes several hours and about 15 to 34 GiB of RAM[3].

Formal verification has been the gold standard for security assurance but too costly for most software. If agents can write millions of lines of proof that a small, trusted checker accepts, the expensive part shifts to writing and reviewing the specification. That could make machine-checked guarantees practical for far more of the code that critical systems depend on.