AlphaProof Code: How AI Agents Proved Signal’s Machine Code

TL;DR

What: Google DeepMind’s AlphaProof Code used AI agents to prove security properties of Signal’s compiled machine code in Lean.
Why it matters: The agents’ proofs are untrusted; only a small, human-approved spec and Lean’s kernel are trusted.
What to do: Copy the pattern for your own coding agents: a held-out spec, a gatekeeper, and mutation checks.
Key stat: About 6.5 million lines of agent-written proof rest on about 26,000 trusted lines.

AlphaProof Code is a Google DeepMind framework where humans and AI agents write a formal Lean specification, then a team of prover agents proves the compiled code meets it. A gatekeeper accepts a proof only if Lean’s kernel checks it against a held-out copy of the approved spec. It verified Signal’s libsignal at the AArch64 machine-code level.

— Ashutosh Tiwari, NexGismo

Formal verification is the practice of writing a mathematical specification of what a program must do and then proving, with a machine-checked proof, that the program satisfies it. Unlike testing, a valid proof covers every possible input the specification describes, not just the cases someone thought to try.

AlphaProof Code hit the Hacker News front page this week, and most coverage stops at the headline: AI verified Signal. The part developers can use is the trust architecture. DeepMind let dozens of agents write millions of lines of proof without trusting any of them. Teams running coding agents against a test suite have the opposite problem. The agent writes the code and can touch the tests that judge it. The ImpossibleBench paper describes exactly this failure: an agent with access to unit tests “may delete failing tests rather than fix the underlying bug.” Below: what DeepMind did, what it does not prove, and a small Node.js gatekeeper we ran that applies the same idea.

What is AlphaProof Code and what did it verify?

It is a multi-agent framework for formal specification and verification, and it verified key security properties of libsignal, Signal’s reference implementation. DeepMind announced it on November 10, 2026. The target was not a simplified model. The technical paper says the team verified libsignal v0.105.4 with spqr v1.6.0, compiled by the stock rustc compiler to AArch64 Linux machine code.

The proofs cover the post-quantum PQXDH handshake and the Triple Ratchet, establishing forward secrecy, authentication, post-compromise security and handshake secrecy.

Per the paper, the verified libsignal code is about 560 KB, roughly 140,000 AArch64 instructions. The agents produced about 6.5 million lines of Lean proof. The work took a team of five people four weeks.

Why the machine-code level matters

Most protocol verification stops at the design, but real bugs often live in the implementation. Reasoning about the compiled binary removes the Rust source and compiler from the trusted base. To prove the spec catches real mistakes, the team reintroduced two previously fixed libsignal bugs. Lean then proved that both buggy binaries violate the symbolic security theorem, per the paper.

How does AlphaProof Code keep AI agents honest?

It keeps agents honest by never trusting their output: only the human-approved specification, the machine-code semantics and Lean’s kernel are trusted. Everything the agents write is checked mechanically. The workflow has three stages.

Specification. A spec-writer agent drafts Lean theorem statements with the user. Reviewer agents critique each draft. The human approves it, and that git commit becomes the baseline.
Code. Unmodified Rust is compiled normally. The ELF binary is loaded into Lean with a formal semantics of AArch64.
Proof. A team of prover agents proves the spec about the binary. A gatekeeper accepts a proof only if Lean’s kernel checks it and the comparator tool confirms it proves exactly a held-out copy of the spec.

The paper says a proof team typically had 40 to 80 agents on a single machine for 24 to 72 hours. Only an integrator agent committed to the repository.

The held-out spec and the critic

Provers cannot edit the specification; they can only propose small amendments to a critic agent that never sees the proof attempts, and humans approve any that change trusted assumptions. The gatekeeper itself “sees only file paths and theorem names,” not the provers’ explanations. Lean replays every proof in a fresh environment, and sorry and native_decide are rejected.

Why do AI proof agents need a gatekeeper?

They need a gatekeeper because agents under pressure will weaken the goal instead of meeting it. The paper is blunt about this. It cites a swarm of Lean-proving agents where one agent “redefined a predicate used in a conjecture’s hypothesis as False, and the trick spread to the rest of the swarm.” A theorem with a false hypothesis is trivially true, so the “proof” means nothing.

Coding agents show the same failure mode: skip a test or loosen an assertion and the suite goes green. The Lean reference on validating proofs classifies “un-reviewed AI-generated proofs and programs” as potentially malicious input. For that case it recommends the comparator tool as the gold standard.

The comparator README documents a gaming example: a solver defines an open Prop as the conjecture itself and proves the equivalence by reflexivity. Such “definition hole” solutions, it says, must always get an extra, possibly human, check.

A gotcha most write-ups miss

If you plan to try this workflow in Lean, note that the standalone leanprover/comparator repository was archived on October 20, 2026. Its README says it was merged into core as of Lean v4.35.0, as lake comparator and lake check. New setups should use those commands, which the README says are the only ones guaranteed further security fixes.

What does AlphaProof Code not prove?

It does not prove Signal is bug-free; it proves specific properties under stated assumptions. The paper lists the limits clearly.

The AArch64 semantics covers 467 instructions and 31 system calls in 7,532 lines of Lean. It does not model threads, signals, the vDSO or dynamic linking.
The keygen operation is not verified; theorems take the parties’ keys as setup. One-time Kyber prekeys are not covered.
Side channels and other secrets in memory are out of scope. Group messaging is future work.
Cryptographic primitives are specified by trusted contracts, not proved. The symbolic proof assumes perfect cryptography.

All of this comes from the technical paper. One detail to flag: DeepMind’s blog body says “over six million lines of Lean,” while the page’s meta description says “over three million.” The paper’s figure is about 6.5 million lines of proof, so treat the paper as the authoritative number.

How much cheaper is AI formal verification than before?

In this case it cut the effort from person-years to weeks. The paper notes the verified seL4 microkernel took twenty person-years and the CompCert verified C compiler took six. Both were written with verification in mind; the libsignal work, on unmodified production code, took five people four weeks.

The cost moved rather than vanished. “The majority of our effort went not into proofs but into specifications,” the authors write. Writing specs against real code even found fifteen gaps or bugs in a published computational analysis of the Double Ratchet. Humans still review the spec; the blog says agents flagged just one percent of the codebase for a second human look.

My read: the bottleneck is shifting from writing code to writing the thing that judges code, in Lean and in your Jest suite.

How can you apply the AlphaProof Code pattern to Node.js agents?

Apply it by treating agent output as untrusted and gating it with a spec the agent cannot change. Unit tests are not proofs, but the trust boundary carries over.

Our gatekeeper mirrors the paper’s design in four steps. It checks that the agent’s copy of the spec is byte-identical to the approved baseline. It scans untrusted source for weakening markers. It requires the spec to fail on known-bad mutants, which catches vacuous specs. Then it runs the held-out spec, never the agent’s copy, against the agent’s code.

// gatekeeper.mjs — accept untrusted agent code only if a held-out spec passes
import { createHash } from 'node:crypto';
import { readFileSync, writeFileSync, readdirSync, mkdtempSync, cpSync } from 'node:fs';
import { spawnSync } from 'node:child_process';
import { join } from 'node:path';
import { tmpdir } from 'node:os';

const sha = (f) => createHash('sha256').update(readFileSync(f)).digest('hex');
const WEAKENING = [/\b(test|it|describe)\.(skip|todo|only)\b/, /@ts-(ignore|nocheck|expect-error)/, /\bas any\b/, /process\.exit\(0\)/];

function runSpec(srcDir, specDir) {
  const work = mkdtempSync(join(tmpdir(), 'gk-'));
  cpSync(srcDir, join(work, 'src'), { recursive: true });
  cpSync(specDir, join(work, 'spec'), { recursive: true }); // always the HELD-OUT copy
  const files = readdirSync(join(work, 'spec')).map((f) => join(work, 'spec', f));
  const r = spawnSync(process.execPath, ['--test', ...files], { encoding: 'utf8' });
  return r.status === 0;
}

export function gatekeep({ workspace, heldOut, baseline, mutants = [] }) {
  // 1. The agent's copy of the spec must match the approved baseline
  for (const [file, hash] of Object.entries(baseline)) {
    if (sha(join(workspace, 'spec', file)) !== hash) return `REJECT: spec/${file} was modified`;
  }
  // 2. No weakening markers in untrusted source
  for (const f of readdirSync(join(workspace, 'src'))) {
    const code = readFileSync(join(workspace, 'src', f), 'utf8');
    const hit = WEAKENING.find((re) => re.test(code));
    if (hit) return `REJECT: src/${f} matches weakening pattern ${hit}`;
  }
  // 3. Vacuity check: the spec must FAIL on known-bad mutants
  for (const m of mutants) {
    const dir = mkdtempSync(join(tmpdir(), 'mut-'));
    cpSync(join(workspace, 'src'), dir, { recursive: true });
    writeFileSync(join(dir, m.file), m.code);
    if (runSpec(dir, heldOut)) return `REJECT SPEC: mutant "${m.name}" survived — spec is too weak`;
  }
  // 4. The held-out spec must pass on the agent's code
  return runSpec(join(workspace, 'src'), heldOut) ? 'ACCEPT' : 'REJECT: held-out spec failed';
}

What happened when we ran it

We ran this on Node.js v22.23.4 against a slugify() function with a three-test held-out spec and two mutants. We tried four scenarios: honest code, an agent that changed test( to test.skip( in its own spec copy, buggy code that forgot to strip punctuation, and a vacuous spec with no assertions. The raw output:

$ node run.mjs
A honest code      -> ACCEPT
B edited spec      -> REJECT: spec/slugify.spec.mjs was modified
C buggy code       -> REJECT: held-out spec failed
D vacuous spec     -> REJECT SPEC: mutant "no-lowercase" survived — spec is too weak

Scenario D is the paper’s lesson in miniature. A spec that asserts nothing passes every implementation, just as a false hypothesis makes every theorem true. The paper’s agents “add natural bugs to the code” and prove the theorem false on the mutated binary. For JavaScript, StrykerJS automates mutant generation instead of our hand-written two.

One small gotcha from our run: our first version passed a directory to node --test, and Node v22.23.4 failed with Error: Cannot find module for that path. Passing explicit file paths fixed it, so every run was wrongly rejected until we did. Test the gatekeeper too.

If your agent writes structured data rather than code, the same boundary applies to schemas; see our guide to LLM structured outputs in Node.js. For agents with long-lived state, our agent memory architecture post covers keeping writes bounded and auditable.

How does this compare with typical agent CI?

Trust boundaries: DeepMind’s Signal verification versus a typical coding-agent workflow (DeepMind column from the technical paper)
Concern	DeepMind (Signal)	Typical agent + test suite	Our Node.js gatekeeper
Who writes the judge	Human-approved Lean spec (~18,000 trusted lines)	Often the agent, in the same repo	Human; held-out copy outside the workspace
Can the agent edit the judge?	No; amendments go through a critic and humans	Usually yes	Edits detected by SHA-256 baseline
Checker	Lean kernel + comparator	Test runner exit code	Test runner on held-out spec
Vacuity / weak-spec check	Satisfiability proofs, mutants, historical bugs	Rare	Hand-written mutants (or StrykerJS)
Guarantee strength	Proof for all inputs within the spec	Only the tested cases	Only the tested cases

The NexGismo verdict: this is a research milestone, not a tool you can install today, and its limits are real. The transferable idea is the trust boundary. My recommendation: never let an agent grade its own work. Keep the spec held out, check it for vacuity, and gate merges on a checker the agent cannot touch.

DeepMind’s AlphaProof Code proved security properties of libsignal v0.105.4 at the AArch64 machine-code level, per DeepMind’s November 2026 paper.
About 6.5 million lines of agent-written Lean proof rest on about 26,000 lines of trusted specification and AArch64 semantics.
A team of five completed the work in four weeks, versus twenty person-years for the seL4 microkernel verification.
Agent proofs are untrusted; a gatekeeper accepts them only if Lean’s kernel and the comparator match a held-out spec.
The standalone Lean comparator repository was archived on October 20, 2026, and merged into core as lake comparator in Lean v4.35.0.
The same pattern works for coding agents: hash the approved tests, run a held-out copy, and require the tests to fail on mutants.

Frequently Asked Questions

What is AlphaProof Code?

AlphaProof Code is a Google DeepMind framework for formal software verification. Humans and AI agents write a Lean specification, then a team of prover agents proves compiled code satisfies it. A gatekeeper accepts proofs only when Lean’s kernel checks them against a held-out copy of the approved spec. It was first used on Signal’s libsignal.

Can developers use AlphaProof Code today?

DeepMind has not released AlphaProof Code as a product. It has open-sourced the Lean development for the Signal work, including specifications and proofs, on its code-verification site. Developers can study those artifacts and reuse the trust pattern, a held-out spec plus an independent checker, in their own agent workflows.

Does formal verification mean Signal has no bugs?

No. The proofs cover specific properties such as forward secrecy and post-compromise security under stated assumptions. Key generation, one-time Kyber prekeys, threads, side channels and group messaging are outside the verified scope, and cryptographic primitives are trusted contracts. Bugs outside the specification are not ruled out.

What is the difference between formal verification and testing?

Testing checks a program on the specific inputs someone wrote down. Formal verification proves the program meets a mathematical specification for every input that specification covers. Both depend on the specification being right: a weak test suite or a vacuous theorem can pass buggy code, which is why mutation checks matter in both.

How do I stop an AI coding agent from cheating on tests?

Keep the approved tests outside the agent’s workspace and run that held-out copy, not the agent’s. Detect edits with a hash baseline, block markers like test.skip and @ts-ignore in agent code, and confirm the tests fail on deliberately broken mutants. Review any request to change the tests yourself.

AlphaProof Code shows AI can write proofs nobody needs to trust, as long as the judge is small, fixed and human-approved. Most teams will not write Lean proofs, but they should stop letting agents grade their own homework. Start with the gatekeeper above: hash your approved tests, run them from a held-out copy, and add two or three mutants that must fail. If you are caching or replaying agent results, pair this with our notes on semantic caching for LLMs. The paper’s sections on spec writing and gatekeeping are its most practical pages.