---
title: Google DeepMind's AlphaProof Code uses AI agents to formally verify Signal's libsignal down to AArch64 machine code | ctxsec
url: https://ctxsec.com/items/google-deepmind-alphaproof-code-formally-verifies-libsignal-machine-code
description: "DeepMind says human experts and Gemini-powered agents wrote Lean specifications for Signal's PQXDH handshake and Triple Ratchet, then prover agents generated about 6.5 million lines of machine-checked proof that unmodified libsignal v0.105.4, compiled to AArch64 Linux code, delivers forward secrecy, authentication, post-compromise security and handshake secrecy. It rests on about 26,000 lines of trusted specifications and machine semantics, took four weeks, and when two old, already-fixed bugs were reintroduced, the system showed the altered code was insecure. DeepMind calls it the first verification of a widely deployed protocol's implementation at this depth by any method."
status: "official (Google DeepMind blog and paper, Nov 10, 2026)"
published: 2026-11-10
---

> DeepMind says human experts and Gemini-powered agents wrote Lean specifications for Signal's PQXDH handshake and Triple Ratchet, then prover agents generated about 6.5 million lines of machine-checked proof that unmodified libsignal v0.105.4, compiled to AArch64 Linux code, delivers forward secrecy, authentication, post-compromise security and handshake secrecy. It rests on about 26,000 lines of trusted specifications and machine semantics, took four weeks, and when two old, already-fixed bugs were reintroduced, the system showed the altered code was insecure. DeepMind calls it the first verification of a widely deployed protocol's implementation at this depth by any method.

[← AI](/ai) · [markdown](/items/google-deepmind-alphaproof-code-formally-verifies-libsignal-machine-code.md)

official (Google DeepMind blog and paper, Nov 10, 2026)

2026-11-10

### Google DeepMind's AlphaProof Code uses AI agents to formally verify Signal's libsignal down to AArch64 machine code

- **What it does and doesn't cover:** the proofs assume the cryptographic primitives are secure and trust contracts for some low-level routines; no new Signal vulnerabilities were reported.
- **Why it matters:** if agents can make formal verification cheap, it becomes a defensive counterweight to AI-driven bug hunting. The Lean development is published for others to reuse.

Sources: [Google DeepMind: Introducing AlphaProof Code (Nov 10, 2026)](https://deepmind.google/blog/introducing-alphaproof-code/) · [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (paper, Nov 10, 2026)](https://google-deepmind.github.io/code-verification/)