Google DeepMind introduced AlphaProof Code on November 10, describing a human-guided framework that uses Gemini Carbon agents to produce machine-checked proofs about Signal’s cryptographic implementation.

What was verified

The technical paper studies a command-line harness built from libsignal and compiled to AArch64 machine code. It reports roughly 6.5 million lines of Lean proof code establishing specified secrecy and authentication properties, supported by trusted specifications, machine semantics and contracts for some called routines.

Humans determine and review the specifications. Lean checks whether a proof establishes those statements; that does not automatically establish that every assumption or security goal is correct.

A research result with a defined boundary

The paper distinguishes symbolic and computational guarantees. Its computational proof excludes quantum attackers, multi-device state and other scenarios; the result concerns the authors’ harness build, rather than certifying all Signal applications. It does not prove every possible implementation bug absent.

DeepMind published the paper and verification artifacts. The reported four-week campaign and successful tests using two reintroduced historical bugs are the researchers’ results; we have not rerun their proofs or independently audited the trusted code.