Google DeepMind's AI Agents Machine-Verified Signal's Core Crypto Code

Google DeepMind used teams of AI agents to produce roughly 6.5 million lines of machine-checked Lean proof code verifying security properties of Signal's compiled libsignal implementation, according to work introduced as AlphaProof Code on November 10, 2026. A five-person research team completed the proof effort in four weeks and released its specifications and verification artifacts for outside review. The technical paper describes the result as the first protocol-level security proofs for the unmodified code of a widely deployed cryptographic protocol implementation.

The stakes are significant. Formal verification (mathematical proof that code satisfies specified properties, checked by a proof tool's kernel rather than by testing) has historically been too labor-intensive to apply to production cryptographic code. If agent-generated proofs can compress that timeline, the security guarantees available to widely used messaging infrastructure could change materially.

What exactly was verified?

The work moved beyond an abstract model of Signal's protocol design to its compiled implementation. The researchers wrapped the unmodified libsignal v0.105.4 and SPQR v1.6.0 crates in a small command-line harness, then used stock rustc to build a statically linked AArch64 Linux executable. That binary — not a paper model — is the target of the proofs.

The verified scope covered one-to-one session code, including the PQXDH handshake and Triple Ratchet messaging. The team reports two independent arguments:

• Ten symbolic theorems under idealized cryptographic assumptions
• One computational proof bounding an attacker's advantage through cryptographic assumptions and statistical terms

The properties verified include forward secrecy, which protects earlier messages after current state is stolen; authentication; post-compromise security, which concerns recovery after a compromise; and handshake secrecy. The symbolic argument additionally covers handshake secrecy after a later Diffie–Hellman break.

How did the agents divide the labor?

Humans selected the properties to verify, resolved ambiguities and security trade-offs, reviewed specifications and retained final approval. Agents powered by Gemini 4 Carbon and Claude Opus 5.5 drafted and reviewed those specifications, with review performed by a model from a different family than the drafter. Gemini 4 Carbon agent teams then generated all the proof code. According to the paper, none of the human authors wrote any proof code.

Typical campaigns used 40 to 80 agents running on a single machine for 24 to 72 hours. An orchestrator and team leads coordinated proof workers, while architect and integrator roles maintained the shared proof base. The agents ran continuously on the researchers' workstations while symbolic and computational proofs proceeded in parallel.

The proof generation rested on roughly 26,000 lines of trusted specifications and AArch64 (Arm's 64-bit processor architecture) semantics.

How did the team prevent agents from gaming the proofs?

A gatekeeper accepted a proof only after Lean's kernel (the small trusted core that checks proof validity) verified it and a comparator confirmed that it matched the held-out, human-approved specification — including every transitive definition — using only Lean's standard axioms.

The control matters. The paper identifies a documented risk in agent-generated proofs: a specification can be weakened indirectly through one of its definitions, silently hollowing out the guarantee. Agents could propose small amendments when proofs exposed genuine specification problems, but changes to trusted assumptions required human approval or a user-set policy, and every change was logged with justifications.

Did the specifications catch real bugs?

Yes. To test whether the specifications could detect actual errors, the team reverse-applied the fixes for two previously repaired libsignal bugs — known as the weak state and small subgroup bugs — and recompiled the altered binaries. In both cases, the system produced Lean proofs showing that the symbolic security theorem failed. The public verification repository separates the computational, symbolic, shared binary and AArch64-semantics material, and documents how to rebuild and independently check the proofs.

Signal chief technology officer Ehren Kret said the work "gives us even greater confidence in our code's privacy guarantees."

What are the limits of the guarantees?

The guarantees stop well short of certifying Signal's complete applications, and the paper is explicit about the boundaries:

• The results concern the researchers' libsignal-cli build running as a fresh process
• Key generation was not verified
• Group messaging was left for future work
• Side channels and multi-device state fall outside the scenario
• Low-level cryptographic primitives and selected output and library routines are represented by trusted contracts, so the result depends on those contracts, the approved specifications, Lean's kernel, the AArch64 semantics and assumptions about the primitives

The post-quantum question remains open. The paper states that neither argument proves the post-quantum healing that SPQR is designed to add: the computational theorem covers classical attackers only, while the symbolic ratchet theorems let the attacker choose SPQR keys. The computational model also restricts several attacker actions and becomes vacuous at sufficiently large message and session scales. These boundaries define exactly what an outside reviewer must trust before treating the machine-checked proofs as a security guarantee for a particular deployment.

What comes next?

The researchers' stated next steps are threefold: strengthen the theorems, reduce the trusted base by verifying more hooked routines and connecting cryptographic contracts to verified implementations, and expand coverage to group messaging, sealed sender and server-side protocols. Their objective of verifying new libsignal releases before shipment is a research goal, not an announced deployment.

The result's immediate significance lies in the division of labor it demonstrates. Agents handled the proof construction entirely; assurance still rests on human-reviewed specifications and explicit, logged assumptions. By releasing the proofs and the checking procedures, the team has given outside reviewers a way to test that foundation as the researchers work to carry the workflow into continuing libsignal development.