DeepMind AlphaProof Code Explained: How AI Verified Signal’s Encryption Code

Google DeepMind has shown AlphaProof Code, an AI agent system that wrote machine-checked proofs about Signal’s encryption code. The proofs cover the compiled machine code that runs on devices, not just the protocol on paper.

The whole effort took about four weeks with a small human team. Everything is open source, so you can read the specs and even re-check the proofs yourself.

In this guide I explain what was proved, what was not, and how to explore the proofs step by step.

What DeepMind Announced on November 10, 2026

On November 10, 2026, Google DeepMind published a blog post by Pushmeet Kohli and Swarat Chaudhuri introducing AlphaProof Code. They call it “a novel agentic framework for formal verification” that combines human expertise with AI agents.

The first big target was the core cryptography behind the Signal protocol. This protocol protects private chats in apps like Signal and Google Messages.

Here are the headline claims from the blog and paper:

• Depth: the proofs reach the compiled machine instructions, not only the Rust source or a protocol model.
• Speed: about four weeks of work. The paper says the Signal proof team was five people.
• Size: over six million lines of Lean. The paper puts it at about 6.5 million lines of untrusted proof code.
• Human load: agents audited their own proofs and flagged about one percent of the codebase for a human look.
• Bug test: the team put two real, already fixed libsignal bugs back in. In both cases the system proved the buggy binary was insecure.

Signal’s CTO, Ehren Kret, is quoted in the blog: “Using AI agents to translate live code into valid Lean theorems is a major breakthrough.”

Note: The blog body says “over six million lines of Lean” while one page summary mentions three million lines. The paper and project site both give about 6.5 million lines, so I use that figure.

Formal Verification in Plain English

Normal testing runs code on some inputs and checks the output. It can find bugs, but it can never show that no bug exists for every possible input.

Formal verification is different. You write a precise math statement of what the code must do (the specification). Then you build a proof that the code meets it in every case.

Why Lean matters here

Lean is a proof assistant and programming language. Its small “kernel” checks every step of a proof. If one step is wrong, the proof does not compile.

This is why AI can safely write the proofs. A model can make things up, but Lean will reject a fake proof. You only need to trust the spec and the kernel, not the AI.

Why this used to be so slow

Writing proofs by hand is very hard work. The DeepMind paper compares it with the seL4 microkernel, which took “twenty person-years to verify.” AlphaProof Code moves most of that proof work to agents.

How AlphaProof Code Works

The key idea is a split of jobs. Humans decide what to prove. Agents do the proving. Lean decides whether the proof is real.

The agent roles

The paper describes several kinds of agents working together:

• Specification writer: drafts the trusted theorems from papers and standards, under close human guidance.
• Reviewer agents: act as skeptics and look for specs that are too weak or not faithful.
• Prover agents: an orchestrator schedules work, team leads manage workers, and an architect and integrator keep the proof structure tidy.
• Critic agent: reviews any proposed change to the spec. It never sees proof attempts.
• Gatekeeper: accepts a proof only if Lean checks it and a tool called comparator confirms it matches a held-out copy of the approved spec.

That gatekeeper rule is important. Agents cannot quietly weaken the goal and then claim success, because the approved spec lives where they cannot write to it.

Which models were used

The blog says proofs came from agents “powered by Gemini Carbon”, linked to the Gemini 4 Carbon launch. The paper also names Claude Opus 5.5 for specification review. You can read more about the model in my Gemini 4 Carbon guide.

A typical proof campaign used 40 to 80 agents on one machine for 24 to 72 hours. If you have used sub-agents in coding tools, the pattern will feel familiar. See my Claude Code subagents guide for a small-scale version of the same idea.

Where humans stay in the loop

• Before proving: a human reviews and approves each specification. That git commit becomes the baseline.
• During proving: humans approve any change to trusted assumptions.
• At the end: humans re-run the comparator by hand and look at the ~1% the agents flagged.

What Was Proved (and What Was Not)

The verified program is libsignal-cli, a small command-line harness around unmodified libsignal v0.105.4 and SPQR v1.6.0. It was built with stock rustc 1.98.1 for AArch64 Linux.

Protocol parts covered

• PQXDH handshake: uses X25519 plus Kyber1024 (the round-3 predecessor of ML-KEM-1024).
• Triple Ratchet: the Double Ratchet combined with SPQR, the Sparse Post-Quantum Ratchet using ML-KEM-768.
• Building blocks: XEdDSA signatures, HKDF, HMAC-SHA256, AES-256-CBC with HMAC, SHA-256/512 and Protobuf parsing.

The security results

The project proves results in two models. The symbolic model (built on a framework called DyLean) has ten theorems. They cover forward secrecy, post-compromise security, authentication, KCI resistance, handshake secrecy and “harvest now, decrypt later” resistance.

The computational model gives a concrete bound on how much advantage an attacker can get. It rests on standard crypto assumptions such as Gap-DH and XEdDSA unforgeability.

What is out of scope

This is where honest reading matters. The paper lists these limits:

• Side channels: timing and memory leaks outside the model are not covered.
• Key generation: the keygen command is not verified. Keys are taken as given.
• Crypto primitives: 37 routines (such as AES, SHA compression and X25519 operations) are replaced by trusted contracts. They are assumed correct, not proved.
• Quantum attackers: the computational proof covers classical attackers only.
• Platform: only static, single-threaded AArch64 Linux binaries. Android and iOS builds were not directly tested.
• Features: group chats and multi-device state are not covered.

Warning: “Formally verified” does not mean “unhackable”. It means the code meets a specific written spec under listed assumptions. Always read the assumptions before quoting the result.

Key Numbers at a Glance

How to Explore the Proofs Yourself

You have two options. Browse the proofs on the web in minutes, or rebuild and re-check them on a strong Linux machine over several hours.

Option 1: Browse online (no install)

1. Open the project site. Go to google-deepmind.github.io/code-verification. It hosts the paper text and the Lean development.
2. Start with Tier-1 statements. These are the headline theorem files. They are the part a human really needs to read.
3. Read Tier-2 definitions next. These hold the symbolic specs that the theorems use.
4. Skip Tier-3 at first. This is the trusted AArch64 semantics and loader. It matters, but it is long and low-level.
5. Use the paper map. In the GitHub repo, open docs/PAPER_MAP.md to jump from a paper claim to the Lean file that proves it.

Option 2: Rebuild and re-check locally

The README says a full build takes several hours and uses roughly 15 to 34 GiB of peak RAM. Plan for a big workstation or a cloud VM.

1. Install Lean via elan. The repo’s lean-toolchain file pins leanprover/lean4:v4.34.0, and elan picks it up automatically.
2. Install the pinned Rust toolchain. Use version 1.98.1 with the AArch64 targets (command below). Do not override it, because generated Lean files depend on the exact compiler output.
3. Add the other tools. Put protoc, LLVM ld.lld 22.1.8 and Zig 0.16.0 on your PATH.
4. Clone the repo. Run git clone https://github.com/google-deepmind/code-verification and change into the folder.
5. Fetch the cache and build. Run the build commands below. Set about one Lean thread per 4 GiB of free RAM.
6. Run the comparator (Linux only). This checks that each headline theorem matches its trusted statement and uses only standard Lean axioms.

Rust toolchain install:

rustup toolchain install 1.98.1 \
  --target aarch64-unknown-linux-gnu,aarch64-unknown-linux-musl \
  --component rust-src,llvm-tools-preview

Build and kernel-check the proofs:

lake exe cache get
ulimit -S -s 524288
export LAKE_RESTORE_ARTIFACTS=true
export LEAN_NUM_THREADS=8
lake build

Independent comparator check:

comparator/install-tools.sh /tmp/comparator-tools
set -a; source /tmp/comparator-tools/env; set +a
lake build ComparatorChallenge ComparatorSolution
comparator/run.sh

Tip: If you only want to confirm the headline claims, the comparator step is the most useful part. It replays the main theorems in a fresh Lean kernel and checks them against the held-out spec.

Try the verified CLI

The project site shows a small demo where “alice” sends “Hi Bob!” to “bob” with libsignal-cli. Replaying the same message makes recv exit with code 1 and write no files, which is the replay protection in action.

Exit codes are simple: 0 means accepted, 1 means rejected, and 2 means a bad command line or unreadable file.

Who Should Care About This

• Security engineers: this shows proof work at binary level can now take weeks, not years.
• Developers using AI coding agents: the “held-out spec plus checker” pattern is a smart way to stop agents from gaming their own goals.
• Signal users: nothing changes in the app today, but it is extra evidence the core crypto code matches its design.
• Researchers and students: the repo is a huge, real Lean codebase to learn from.

If you are interested in related ideas, I also covered Anthropic FlashProve and provable inference, which applies proof ideas to model outputs.

My Take

The most impressive part is not the size of the proof. It is that the result is checkable by anyone. You do not have to trust Gemini, DeepMind or me, only the spec and the Lean kernel.

I also like how open the paper is about limits. Hooked crypto routines, no keygen proof and classical-only bounds are real gaps, and they are listed clearly.

The bigger lesson for everyday devs is the workflow. Humans write and approve the goal, agents grind, and a strict checker decides. That pattern will spread far beyond crypto.

Troubleshooting: Common Problems and Fixes

• Build runs out of memory: lower LEAN_NUM_THREADS. The README suggests about one thread per 4 GiB of free RAM.
• Stack overflow during build: make sure you ran ulimit -S -s 524288 in the same shell before lake build.
• Looking for a -j flag: Lake has no -j option. Control parallel work with LEAN_NUM_THREADS instead.
• Comparator fails on macOS or Windows: it needs Linux, because it uses landrun and the Linux Landlock security module. Use a Linux VM.
• Binary pin check fails: you probably used a different rustc. Reinstall 1.98.1 and do not override rust-toolchain.toml.
• Build takes hours: that is expected. Run lake exe cache get first to download prebuilt pieces.

Frequently Asked Questions

What is AlphaProof Code?

It is a Google DeepMind framework where human experts write and approve specifications, and AI agents write Lean proofs that code meets them. It was announced on November 10, 2026.

Did AI prove that Signal is unhackable?

No. It proved specific security properties of the compiled libsignal code under listed assumptions. Side channels, key generation and the internals of some crypto primitives are out of scope.

Which AI model wrote the proofs?

The proof agents were powered by Gemini 4 Carbon. The paper also says Claude Opus 5.5 was used for specification review.

What does the 1% flagged for humans mean?

The agents audited their own work and marked about one percent of the codebase for a human second look. The rest is checked automatically by the Lean kernel.

Can I use AlphaProof Code on my own project?

DeepMind has not released it as a product. What is public is the Signal verification work: the specs, proofs and tooling in the open-source repo.

Do I need special hardware to check the proofs?

Browsing online needs nothing. A full local rebuild needs a Linux machine with roughly 15 to 34 GiB of free RAM and several hours.

What licence is the code under?

The repository is Apache 2.0. The included libsignal code keeps its AGPL-3.0-only licence.

Sources

• Google DeepMind: Formal Verification of Signal’s Protocol with Gemini
• AlphaProof Code project site
• google-deepmind/code-verification on GitHub
• Technical paper (PDF)
• Qodo: where should human review go?