AlphaProof Code: What Google's Signal Proof Actually Verifies

Google DeepMind introduced AlphaProof Code on November 10, showing how AI agents can produce machine-checked security proofs for Signal's core protocol implementation. The result is substantial, but it does not certify the whole Signal app. For developers, the useful question is exactly which code, properties and assumptions the proof covers.

What AlphaProof Code does

DeepMind describes a workflow where people help define the security requirements, AI agents construct proofs, and Lean checks them. Gemini Carbon powered the proving agents. Google says the verification campaign took four weeks and generated more than six million lines of Lean proof code.

The distinction from an AI code review matters. A model saying that a function looks safe is still making a judgment that could be wrong. A formal proof makes a precise claim that a separate checker can accept or reject. The model can be unreliable at finding a proof without making a successfully checked proof unreliable for the same reason.

That moves the difficult question upstream: did the team ask the checker to prove the right thing? A proof that faithfully establishes a weak requirement is still a weak security guarantee.

Which Signal code was verified?

The technical paper identifies libsignal-protocol v0.105.4 with spqr v1.6.0. It covers one-to-one session setup and messaging, including PQXDH and the Triple Ratchet. The unmodified Rust crates run inside a small command-line harness, compiled to AArch64 Linux machine code.

The covered operations are initialization, sending and receiving. Key generation is outside the verified operations. The theorem concerns the specified compiled program under its modeled environment, rather than every version, platform and feature carrying the Signal name.

For a team evaluating a similar claim, the code revision and build target belong next to the result. Changing a dependency or compiler can change the executable. A proof attached to yesterday's binary should not quietly become a promise about tomorrow's release.

What remains outside the proof?

The paper lists a trusted computing base: the specifications, machine and process semantics, contracts for certain external routines, cryptographic assumptions, supporting tooling and Lean itself. These are the foundations on which the checked result rests. It also distinguishes symbolic security arguments from computational ones, rather than treating every guarantee as unconditional.

A verified protocol component does not certify the surrounding application. The desktop interface, account recovery, device security and organizational handling of messages introduce questions that this result does not settle. This is a scope boundary, not evidence of a flaw in those systems.

A useful review asks whether an assumption matches the deployment. If the theorem assumes an external routine behaves according to a contract, someone must justify that contract for the implementation being shipped. More generated proof lines cannot compensate for an assumption nobody checked.

Why the known-bug check matters

Google reports reinserting two previously fixed bugs into an isolated version of the code. In both cases, AlphaProof Code produced machine-checked evidence that the modified version was insecure. These were controlled tests involving historical bugs, not an announcement that two new vulnerabilities remain in current Signal.

This is a useful habit for teams adopting AI-assisted verification. Deliberately break a property you care about and check whether the verification process rejects it. If an obviously broken implementation still passes, investigate the specification before celebrating the passing proof. The check tests the usefulness of the question, rather than merely the system's ability to answer it.

How developers can inspect the released artifacts

The public repository includes the specifications, proofs, a paper-to-code map and reproduction instructions. Start with docs/PAPER_MAP.md to connect the claims you care about to the corresponding Lean files. The repository is a research artifact, not a hosted service that automatically certifies an arbitrary application.

Its build instructions pin Lean 4.34.0, Rust 1.98.1, LLVM ld.lld 22.1.8 and Zig 0.16.0. They estimate several hours and roughly 15–34 GiB peak RAM for the proof build. The separate comparator workflow is Linux-only and checks that the headline theorem matches its trusted statement and permitted axioms, replaying it in a fresh Lean kernel.

Those details make reproducibility a real engineering task. Follow the pinned toolchain, preserve the binary checks and record what actually completed. Reading a proof repository, building its dependencies and independently replaying its headline theorems are different levels of verification. The instructions here describe the published reproduction process, not a completed independent proof replay.

Where this helps an engineering team

The practical starting point is a narrow component with an expensive failure mode and requirements that can be stated precisely. Before allocating a large agent budget, write down the invariant, the deployment boundary and the assumptions a reviewer must accept. That work remains valuable even if the proof attempt fails, because it exposes ambiguities that ordinary test cases can miss.

The strongest implication of AlphaProof Code is a change in where expert effort goes. If agents can shoulder more proof construction, the scarce work becomes choosing meaningful guarantees and keeping them attached to the software people actually run. A verification process earns trust when its scope survives scrutiny, not when its proof directory becomes enormous.

I'm Paras. I work at the intersection of AI, engineering and distribution.

I help technical founders explain difficult engineering work clearly, without turning the limitations into fine print.

Book a 30-minute call