DeepMind’s AlphaProof Code Proves Signal’s Crypto Core in Four Weeks, Not Years

Google DeepMind has achieved a milestone in software security: its new AI system, AlphaProof Code, formally verified critical cryptographic guarantees of the Signal protocol in roughly four weeks—work that has traditionally consumed years of expert effort. The verification targeted libsignal, the open-source library at the heart of Signal, and extended down to the compiled 64-bit Arm machine code, closing a gap that source-level proofs often leave open.

• AI-driven verification: A five-person team, paired with agents powered by Gemini Carbon, generated approximately 6.5 million lines of Lean proof code, with only about 1% flagged for human review.
• Machine-code level assurance: The proofs cover PQXDH session establishment and the Triple Ratchet protocol, establishing forward secrecy, authentication, post-compromise security, and handshake secrecy against the actual binary, not just the design.
• Built-in validation: When researchers reintroduced two previously fixed libsignal bugs, AlphaProof Code correctly identified that the modified builds violated security properties, demonstrating the framework’s rigor.

What Was Actually Verified

The scope of the verification is both impressive and carefully bounded. DeepMind’s team used libsignal version 0.105.4 with the Sparse Post-Quantum Ratchet library, compiling an AArch64 Linux command-line executable from unmodified Rust crates. The theorems address runs of that compiled executable, covering the PQXDH handshake for one-to-one communication and the Triple Ratchet messaging protocol. The properties proven include authentication, confidentiality, forward secrecy, and post-compromise security.

Critically, the proofs assume the underlying cryptographic primitives are perfect. Side-channel attacks such as timing and power analysis are out of scope, as is the rest of the Signal application—from the user interface to backup code. No new vulnerabilities were discovered, which is good news for Signal users but also underscores that this is a demonstration of capability, not a bug hunt.

“While previous formal verification focused on smaller portions of code, Google DeepMind’s approach allows for significant expansion,” said Ehren Kret, Signal’s chief technology officer, adding that rigorously verifying the protocol implementation gives “greater confidence in privacy guarantees.”

The technical foundation rests on Lean, a theorem prover whose small trusted kernel checks every proof step. While the AI agents wrote the bulk of the proof code, human experts defined the formal security requirements and reviewed proposed specification changes—a division of labor that DeepMind research scientist Swarat Chaudhuri described as “a system that is fundamentally built for human AI collaboration.”

The Economics of Trust

The significance of this work lies less in what it says about Signal—whose cryptography was already among the most audited in the world—and more in what it says about the economics of formal verification. Historically, writing mathematical proofs for software has been prohibitively expensive: the seL4 microkernel took around 20 person-years, and the CompCert verified C compiler took six years. If AlphaProof Code can compress that timeline to weeks for a small team, verification could become viable for a much broader class of critical software.

Google has open-sourced the verification artifacts and published a technical paper alongside the announcement. The team claims two firsts: the first AI-assisted formal verification of a widely deployed cryptographic protocol at this depth, and the first time any method has verified a protocol’s actual running implementation rather than just its design blueprint.

Yet the path to broader adoption is not without obstacles. Google told Wired that “it’s unclear as yet how practical it will be to use it more broadly,” given the compute demands of agentic formal verification. The company declined to disclose the cost of this project and would not comment on whether a commercial product is planned. DeepMind has signaled intentions to extend the method to power grids and medical devices through systems like CodeMender, but those applications remain speculative.

A New Frontier, With Caveats

The achievement also highlights a persistent challenge: a proof only establishes what its statement says. Human experts must define confidentiality, specify which executions count, describe the attacker model, and determine how the program is modeled. These choices create the proof boundary, and a strong proof of a narrow claim remains a narrow proof. The published paper lists the trusted base, including contracts for selected cryptographic primitives, making the boundary explicit—a practice that every verification effort should follow.

For now, DeepMind’s work stands as a proof of concept with real teeth. It demonstrates that AI agents can shoulder the heavy lifting of formal verification while humans retain control over specifications and review. If the approach scales and costs become manageable, the implications stretch far beyond messaging: banks, infrastructure, and software supply chains could move from “we believe it’s correct” to “it’s proven correct.” That would be one of the most powerful tools yet for trusting the code that underpins modern life.