Agentic WeeklyGet The Weekly Verdict, freeSubscribe free

Reported News

DeepMind's AlphaProof Code proves Signal's libsignal secure at machine-code level with 6.5M lines of Lean

Google DeepMind said on November 10, 2026 that AlphaProof Code, a multi-agent framework, proved key security properties of Signal's libsignal v0.105.4 at the AArch64 machine-code level, calling it "the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI." The paper counts about 6.5 million lines of Lean proof.

By Agentic Weekly · Evidence: Reported · Editorial standards

Share on X
Changes reported
6
listed below, each from a source we read
We tested
Not tested yet
reported from sources; we did not run it ourselves
Gaps we flag
5
things we could not verify
Sources
6
3 primary, linked below

What changed

Changes the sources report, with the evidence status of each
#What the source saysStatus
01AlphaProof Code is a multi-LLM agentic framework: humans and a specification-writer agent turn security goals into Lean specifications that human experts review, then a team of prover agents (the blog says they ran on Gemini Carbon) writes the proofs, and a gatekeeper accepts a proof only if Lean's kernel checks it.Reported
02The target is unmodified libsignal v0.105.4 with spqr v1.6.0, compiled by stock rustc 1.98.1 to an AArch64 Linux binary inside a small CLI harness. The paper says the proofs cover the PQXDH handshake and Triple Ratchet: forward secrecy, authentication, post-compromise security and handshake secrecy.Reported
03Scale, per the paper: about 6.5 million lines of Lean proof, resting on about 18,000 trusted specification lines plus about 8,000 lines of AArch64 semantics, for about 140,000 AArch64 instructions of verified code. The blog says agents flagged just one percent of the codebase for human review.Reported
04The work took four weeks; the paper says a team of five ran agent teams of typically 40 to 80 agents on a single machine for 24 to 72 hours per proof campaign. It compares this with 20 person-years to verify the seL4 microkernel.Reported
05As a check, the team reverse-applied two upstream libsignal fixes (commits cd36118 and 5293caa, a weak-state bug and a small-subgroup bug) and produced machine-checked Lean proofs that both bug-injected binaries violate the symbolic security theorem.Reported
06The Lean specifications and proofs are open-sourced under Apache 2.0 at github.com/google-deepmind/code-verification, with a reviewers' site. The blog pairs the work with Google's CodeMender defense agent.Reported

reported by the sourcemeasured or run by usnot verified

Primary source: Google DeepMind: Introducing AlphaProof Code (blog). We are the fast, independent index; the vendor’s own page is the source of record for this release.

Who this matters for

Security and formal-methods teams, and anyone who ships Rust crypto or protocol code, should read the paper and the repository now: it is a worked, reproducible template for proving properties of a compiled binary rather than a model of it, with a clear split between trusted specification and untrusted AI-written proof. Signal and Google Messages users get no new feature or setting; the result is assurance about one build of the library, not a product change.

Developers looking for a tool to run on their own code can wait. Neither the blog nor the repository offers AlphaProof Code itself as a product, and the model the blog names is in limited release (see below).

What the proofs do not cover, in the paper's own words

  • Group messaging is left as future work; only one-to-one sessions between two honest parties are verified.
  • The computational proof gives no guarantee against a quantum adversary and does not cover multi-device state; its bound becomes vacuous at large scale, for example single sessions of about 25,000 messages if nearly every message starts a new epoch.
  • 37 hooked routines, including the low-level cryptographic primitives (SHA-256/512, AES-256-CBC, X25519, Kyber1024, ML-KEM-768), are replaced by trusted contracts rather than verified; keygen is not verified; one-time Kyber prekeys and side channels are out of scope.
  • The results concern the team's own libsignal-cli build run as a fresh process, not Signal's Android or iOS apps; the paper argues the theorems carry over only if those builds preserve the same protocol behaviour.

Hard questions the announcement leaves open

  • Line counts do not agree across Google's own materials: the blog says over six million lines of Lean and the paper about 6.5 million lines of proof (nearly 7 million lines in the repository), while the summary in DeepMind's own blog feed says three million lines of proofs. Which figure counts what?
  • Gemini Carbon: Google's October 28 post says Gemini 4 Carbon is available only to a subset of cyber defenders through its Fairwind Program, not to developers yet. Could anyone outside Google reproduce the proof campaign today, and at what token cost? Wired reports Google declined to share the cost.
  • Is the AlphaProof Code framework (agent skills, orchestrator, gatekeeper) going to be released, or only the Signal artifacts? The repository holds the specifications, proofs, AArch64 semantics and comparator scripts; Wired reports Google declined to comment on whether it plans a commercial formal verification product or service.
  • Independent replication: the README says re-checking all proofs takes several hours and about 15 to 34 GiB of peak RAM. No third party has yet reported a full kernel re-check, and the trusted specifications still need expert review.
  • The 'first time' claims are DeepMind's. The paper frames them as the first proofs connecting protocol-level guarantees to unmodified code of a widely used implementation, and as a milestone toward the Signal Shot grand challenge launched in April 2026, which targets the Signal protocol and Signal app; the app itself is not verified here.

In the source’s words

“the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI.”

“Using AI agents to translate live code into valid Lean theorems is a major breakthrough.”

“once proofs become cheap, the hard question is what to prove.”

What we have not verified

  • We did not build libsignal-cli or re-run the Lean kernel check on the published proofs.
  • We did not review the roughly 18,000 trusted specification lines or the AArch64 semantics for soundness.
  • The four-week timeline, team size, agent counts and the one percent human-review figure are Google DeepMind's statements; we could not check them.
  • We could not confirm which exact Gemini model version ran the prover agents beyond the blog's 'Gemini Carbon' wording, or the compute and token cost.
  • Whether the results transfer to Signal's shipping Android and iOS builds is argued in the paper, not proved, and we did not check it.

This brief is Reported: written from the sources below, not from running the release ourselves.

Sources

Spotted an error? See our corrections policy or email the address on the contact page. Markdown version for agents: /news/alphaproof-code-signal-libsignal-formal-verification.md

Want these briefs in your Google Top Stories? Add Agentic Weekly as a preferred source on Google.

Newsletter

The Weekly Verdict. Free, every Monday.

A free email every Monday: the week's few big AI releases, then 5 short use cases for the new models, each with a prompt you can paste.

Free. Double opt-in. One click to unsubscribe.