DeepMind's AlphaProof Code produces machine-checked proof of Signal's core encryption

What happened

On November 10, 2026, Google DeepMind published a formal verification of libsignal, the reference implementation of the Signal protocol, according to a dev.to analysis of the announcement. This is not a code review or a manual audit: it is a machine-checked mathematical proof, generated largely by AI, covering the compiled code that actually runs on devices.

The project, called AlphaProof Code, was carried out by five researchers over four weeks. During that time, AI agents working under human supervision generated more than six million lines of proof in the Lean language. The verification targets the two components at the heart of the protocol: the PQXDH handshake, which establishes a secure conversation between two parties, and the Triple Ratchet, which rotates keys for every message. libsignal is the library behind Signal's own app, and the same protocol design is used by WhatsApp and Google Messages.

Proving the code, not the paper

As the dev.to author notes, most security assurance in the industry stops at the design level. Cryptographers prove properties of a protocol described on paper, then engineers implement it, and the gap between the two is where implementation bugs live — a reused nonce, a skipped step on an error path, a state transition the paper never considered.

DeepMind's work reportedly goes further, verifying the compiled code down to the individual instructions that execute on ARM devices. Four properties were established: messages remain secret, the other party is authenticated, past messages stay confidential even if a later key leaks (forward secrecy), and a conversation regains its security after a compromise (post-compromise security). DeepMind describes this as the first time the implementation of a widely deployed protocol has been formally verified by any method, with or without AI.

A tool that can fail

A proof that finds no bugs invites an obvious question: would it have caught one if it existed? According to the dev.to post, DeepMind tested this directly by reintroducing two real bugs that had previously been found and fixed in older Signal versions into an isolated copy of the code. In both cases, AlphaProof Code produced a machine-checked demonstration that the buggy version was insecure.

Humans remained central to the process. Researchers and models wrote the formal specifications together, and human experts reviewed every one. The agents flagged roughly one percent of the codebase for a second human look, while Lean automatically checked the remainder.

What the proof does not cover

The dev.to article is careful about the limits. The proof covers one-to-one sessions only, with group messaging listed as future work. It applies to libsignal version 0.105.4 compiled for ARM Linux inside a test harness — not the full Signal app, its servers, or its user interface. Low-level cryptographic building blocks such as ML-KEM and the curve arithmetic are assumed secure rather than proven. And any proof rests on its specification: if the wrong security goal is written down, the prover will simply verify the wrong claim.

There is also a scope caveat. WhatsApp and Google Messages maintain their own implementations of the Signal protocol, so the result does not automatically carry over to every app that borrows its ideas.

Why it matters

If a five-person team can produce implementation-level verification of a deployed protocol in four weeks, formal verification becomes dramatically cheaper. Work of this kind has historically taken expert teams years, putting it within reach only of the largest organisations. DeepMind has released the verification artifacts as open source, published a technical paper titled "Formal Verification of Signal's Protocol with Gemini," and named medical device firmware and power grid software as future targets.

For messaging developers, the more immediate effect is that the next generation of protocols — including post-quantum designs — could be verified at implementation depth from the outset rather than audited years after shipping. As AI accelerates both code production and attacks on code, the dev.to author argues, defences that can be verified in weeks rather than years are the ones that can keep pace. DeepMind also points to pairing verification with automated patching through a tool called CodeMender, suggesting a loop from discovered flaw to proven fix measured in weeks rather than release cycles.

None of this makes the whole Signal app safe, and audits are not obsolete. But the strongest form of assurance available for software has now been applied to the part of a messenger that matters most, and no new flaws were found in the current code. By DeepMind's account, that level of verification has moved from a multi-year research effort to something a small team could plan for.