Signal’s encryption passed a 6.5-million-line math proof written by AI

Signal’s encryption code now has something almost no widely used software can claim: a mathematical proof that it does what it promises. A team of AI agents worked through libsignal, the library that runs the Signal protocol, and proved that its one-to-one chats stay secret, confirm who is on the other end and shut out an attacker again after a key is stolen. They found no new flaws.

That matters well beyond Signal’s own users. The protocol is the global standard for end-to-end encrypted messaging, and variants of it protect chats in WhatsApp, Messenger and Google Messages. Checking real, shipped code to this depth used to be so slow that almost nobody tried: one of the field’s biggest successes, a verified operating-system kernel, took twenty person-years. This job took four weeks.

The tool, built by Google DeepMind, is called AlphaProof Code. Human experts and AI models first turned Signal’s security goals into formal statements in Lean, a programming language built for mathematical proofs, and a person reviewed every one. Then teams of 40 to 80 agents, powered by Gemini Carbon, wrote the proofs, running for 24 to 72 hours at a time on a single machine. The result is about 6.5 million lines of Lean.

Nobody has to trust those millions of lines. Lean’s kernel checks every step and throws out any proof that does not hold, so it makes no difference which model wrote it or how often it got things wrong along the way. What people do have to trust is much smaller: about 26,000 lines of specifications and a model of how an ARM processor runs code.

The proofs cover the parts of Signal that guard a conversation: the PQXDH handshake that sets up a chat and the Triple Ratchet that changes the key for every message, including the post-quantum layer meant to resist future quantum computers. In practice that means stealing a phone’s current keys does not unlock older messages, and the thief loses access again once the two sides exchange fresh keys.

To show the system can tell good code from bad, the researchers put two old, already-fixed libsignal bugs back in. One made the library keep a copy of a secret key it should have discarded. In both cases AlphaProof Code produced a machine-checked proof that the buggy build was insecure.

The limits are real. The proof covers one-to-one sessions only, and DeepMind lists group messaging as future work. It applies to libsignal version 0.105.4, compiled with the standard Rust compiler for ARM Linux inside a small test program, not to the full Signal apps for iPhone, Android or desktop. The low-level cryptographic building blocks are assumed to be secure, not proven. A mistake in the human-approved specifications would weaken the guarantee, and WhatsApp and the other apps run their own versions of the protocol, so the result does not carry over to them automatically. Google also declined to tell Wired what the analysis cost or whether it plans to sell it as a service.

Signal welcomed the result. “As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees,” Ehren Kret, Signal’s chief technology officer, said in a statement. DeepMind research scientist Swarat Chaudhuri was more cautious, telling Wired there is “a long distance to go” before the method can scale “to all the software of the world.”

For anyone who uses Signal there is nothing to install and no setting to change. The proof is about code already in the app.

DeepMind published the work on November 10, alongside a technical paper, and has released the specifications and proofs as open source on GitHub. It describes the Signal project as a milestone toward a formal-verification grand challenge set in April, and names medical-device firmware and power-grid software as the kind of systems it wants to check next.

Chaudhuri also drew a line on how much of the job the machines should get. “We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs,” he told Wired. Humans still decide what counts as secure, and the AI only proves it.

Tags: Cybersecurity, Google DeepMind, AlphaProof Code, end-to-end encryption, formal verification, libsignal