Google DeepMind Says AI Verified Signal Code, Flagging 1% for Review

What AlphaProof Code checked

AlphaProof Code is a multi-agent framework for formal verification announced by Google DeepMind on 10 Nov 2026. According to DeepMind, its agents verified key security properties of libsignal, Signal’s reference implementation, at the machine-code level. These properties included forward secrecy, authentication, post-compromise security and handshake secrecy.

The team first worked with several models to translate Signal’s security goals into formal specifications. Human experts reviewed every specification, after which agents powered by Gemini wrote proofs in Lean. Lean’s checker accepts a proof only when every step holds. DeepMind says its agents then audited the proofs and identified areas for human review.

The project took four weeks and involved a team of five, according to DeepMind’s technical paper. The paper says “none of the authors wrote any proof code.” DeepMind reports more than six million lines of Lean proof, while the paper puts the figure at about 6.5 million lines, supported by roughly 26,000 lines of trusted specifications and machine semantics.

A proof still depends on human specifications

Formal verification proves that code meets a stated property for every input, rather than testing a sample of inputs. But the proof covers only the properties included in its specification. DeepMind’s paper says, “Once proofs become cheap, the hard question is what to prove,” adding that “The majority of our effort went not into proofs but into specifications.”

A specification defines what the code must guarantee, and DeepMind says it cannot be automatically checked. Assumptions that are too narrow can allow a buggy program to satisfy the specification. The Signal work also assumed perfect cryptography and did not verify the full Signal app, according to the source material.

DeepMind reports that two previously fixed bugs were reintroduced into an isolated copy of the code. In both cases, a machine-checked proof showed that the buggy version was insecure. The project found no new vulnerabilities in the checked parts of the protocol, according to the cited reporting.

Why agent-written pull requests still need review

The Signal project addresses a narrow, high-stakes codebase with specifications approved by human experts. Most everyday pull requests from coding agents do not have a comparable formal specification. They still need to be checked against a team’s rules, the requirements in a ticket and other project context.

Qodo says reviewing and validating AI-generated code is the main delivery constraint for 25.8% of developers and 26.0% of engineering leaders, based on its 2026 survey. In the same survey of 500 US developers and 300 US engineering leaders, 36.4% of developers said AI-generated code takes the same review time while requiring more mental effort.

Formal verification and pull request review therefore operate at different layers. AlphaProof Code provides a machine-checked answer about selected properties of one codebase. Qodo’s PR-layer approach reviews each change against a team’s REVIEW.md, custom instructions and linked ticket, while routing high-severity findings to the people responsible for deciding. The source presents the two methods as complementary: formal proofs can narrow human attention in a critical codebase, while everyday review remains necessary where requirements have not been written as formal specifications.