# Google DeepMind Says AI Agents Proved Signal's Actual Encryption Code Secure in Four Weeks, With Humans Writing What to Prove

Times of AI Desk · 2026-11-11 · Research

[https://timesof.ai/2026/11/deepmind-alphaproof-code-formally-verifies-signal-protocol-lean](https://timesof.ai/2026/11/deepmind-alphaproof-code-formally-verifies-signal-protocol-lean)

> Google DeepMind said on November 10 that AlphaProof Code, a multi-agent framework built on Gemini Carbon, produced machine-checked Lean proofs that the code implementing the Signal protocol meets key security properties that human experts specified. DeepMind says the work took four weeks, that agents flagged about 1% of the proof for human review, and that the system caught two reintroduced bugs. Signal's CTO welcomed it; no independent audit has been published.

The claim that matters is not that an AI wrote a lot of proofs. It is where the proofs reach: Google DeepMind says its agents verified the compiled code of the Signal protocol, not just its design, which is where real-world bugs tend to hide. The strength of the result rests on the specifications, and those were written and reviewed by people.

## What DeepMind says it did

Google DeepMind said on **November 10** that researchers used **AlphaProof Code**, a new multi-LLM agentic framework, to mathematically prove key security properties of the code underlying the **Signal protocol**, which protects messages in apps including Signal and Google Messages.

The work split in two. Researchers worked with a mix of models to turn Signal's security goals into formal specifications, with human experts reviewing every one. Agents powered by **Gemini Carbon** then wrote the proofs in **Lean**, a language whose checker verifies each step. DeepMind says the agents generated more than **six million lines** of Lean, then audited the result and flagged about **1%** for human review.

DeepMind says the proofs show that the compiled code delivers properties such as keeping messages protected before and after a device is temporarily compromised. The verification took **four weeks**, which DeepMind contrasts with the years such work has historically taken expert teams.

To check that the system could tell correct code from flawed code, the team reintroduced **two real, previously fixed bugs** into an isolated copy of Signal's code. In both cases, DeepMind says, it produced a machine-checked proof that the buggy version was insecure.

DeepMind calls this the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a protocol has been formally verified by any method. It says it is open-sourcing the verification artifacts.

## Signal's view and the caveats

Signal CTO **Ehren Kret** said in DeepMind's post that "using AI agents to translate live code into valid Lean theorems is a major breakthrough" and that the verification gives Signal "even greater confidence" in its privacy guarantees.

Axios, which interviewed DeepMind research scientist **Swarat Chaudhuri**, reported that the work remains a research project, not a commercial product. DeepMind is looking at building the technique into AI coding agents and combining it with Google's Project Zero and CodeMender bug-hunting and patching tools, Axios reported.

The result fits a run of machine-checked security work from frontier labs. In October, [Anthropic and Theorem said Claude produced Rocq-checked no-crash proofs](https://timesof.ai/2026/10/anthropic-theorem-claude-formal-proofs-123-oss-fuzz-libraries-risc-v) for 239 entry points in 123 libraries, limited to RISC-V builds. Axios names the model as Gemini 4 Carbon, the system [Google first released to vetted cyber defenders in October](https://timesof.ai/2026/10/google-gemini-4-carbon-fairwind-cyber-frontier).

## Limits

- A formal proof shows the code meets its specification, nothing more. Properties that were not specified, and flaws outside the verified code, are not covered.
- The figures and "first" claims are DeepMind's own. We read DeepMind's post and Axios's report, not the technical paper, and found no independent review of the proofs.
- DeepMind's post says more than six million lines of Lean; Axios reported more than three million. We could not resolve the difference.
- DeepMind's post names the model as Gemini Carbon; Axios calls it Gemini 4 Carbon.

## Sources

- [Google DeepMind: Introducing AlphaProof Code (November 10, 2026)](https://deepmind.google/blog/introducing-alphaproof-code/)
- [Axios: Google touts AI breakthrough, path to "unhackable" software (November 10, 2026)](https://www.axios.com/2026/11/10/google-code-verification-signal)