Google DeepMind unveils AlphaProof Code, an agentic verification framework that produced machine-checked proofs for key security properties in Signal’s deployed cryptographic code. The project connected formal guarantees to compiled AArch64 instructions instead of stopping at an abstract protocol model.

 

The four-week research effort covered Signal’s post-quantum PQXDH handshake and Triple Ratchet. It did not verify the entire Signal app, every protocol component or the surrounding software supply chain, so the result is a focused assurance claim rather than a declaration that Signal is immune to every flaw.

 

The published work establishes four central points:

  • About 6.5 million lines of Lean proof code were generated.
  • The proofs target unmodified compiled code in a controlled harness.
  • Lean’s kernel checked every accepted proof.
  • Historical bugs caused verification to fail as expected.

 

DeepMind Unveils AlphaProof Code for Compiled Signal Code

Google DeepMind’s November 10 announcement describes AlphaProof Code as a multi-agent system for formal software specification and verification. Human experts decide which properties matter and approve the mathematical specifications; AI agents then attempt to prove that the executable satisfies them.

 

The team compiled an unmodified Rust implementation of libsignal for AArch64, loaded the resulting machine code into Lean and modeled the processor behavior needed to reason about its execution. That closes part of the gap between a secure protocol design and the code a device actually runs after compilation.

 

The technical paper says the result rests on roughly 26,000 lines of trusted specifications and AArch64 semantics. The much larger AI-generated proof body is accepted only when Lean’s small kernel checks it against those approved foundations.

 

The Signal Proofs Cover PQXDH and Triple Ratchet

The work covers Signal’s PQXDH handshake and Triple Ratchet, including properties tied to authentication, handshake secrecy, forward secrecy and post-compromise security. Those guarantees address whether a conversation remains protected under specified attacker capabilities and key-compromise scenarios.

 

That scope reaches farther than earlier work centered on abstract descriptions, verification-friendly replacements or narrower implementation properties. DeepMind claims these are the first proofs linking protocol-level guarantees to the unmodified code of a widely deployed cryptographic protocol implementation.

 

The agents generated about 6.5 million lines of Lean, while an automated audit marked about one percent of the development for closer human review. DeepMind says the verification took four weeks, compared with the years of specialist labor such a project could previously require.

 

Background Reading

 

Historical Bugs Test AlphaProof Code’s Gatekeeping

A proof system must reject broken programs rather than produce convincing-looking paperwork. The researchers reintroduced two real, previously fixed bugs into isolated versions of Signal’s code. AlphaProof Code could not establish the desired guarantees and instead produced machine-checked demonstrations that the altered versions were insecure.

 

The team published the Lean artifacts on GitHub, including symbolic and computational developments, binary specifications and mappings from the paper to individual theorems. That gives outside specialists material to inspect rather than asking them to rely only on a provider summary.

 

The method still contains trusted assumptions. Researchers wrote and reviewed the specifications that define what must be proven, while the machine-code model covers a selected execution environment. The paper says its semantics excludes threads, signals, dynamic linking, the virtual dynamic shared object and files outside the current directory.

 

The Verification Does Not Cover the Entire Signal App

WIRED’s independent report says DeepMind found no new vulnerabilities in the portions examined. It also stresses that the project did not formally verify the complete Signal mobile application or every part of the protocol implementation.

 

The proofs therefore do not rule out defects in user interfaces, operating-system integrations, networking layers, update systems or code outside the modeled harness. Formal verification proves specified properties under stated assumptions; an incomplete or mistaken specification can leave relevant behavior beyond the theorem.

 

The research matters because it demonstrates a plausible way to reduce the cost of assurance for mature production code. Similar methods could eventually support cryptographic libraries, medical devices, financial infrastructure and industrial controllers, but DeepMind has not announced a commercial product or disclosed the project’s cost.

 

Signal users gain an unusually deep, independently inspectable argument for core cryptographic behavior, while software teams gain a test of AI agents as theorem-producing tools. The next test is whether the workflow remains practical across larger systems, changing codebases and specifications maintained by people outside DeepMind.

 

Illustrative feature photograph: a smartphone displaying a security-lock graphic, photographed by Dan Nelson and published on Unsplash under the Unsplash License. The image does not depict Signal or the AlphaProof Code project; it was cropped and resized.