"It's a system that is fundamentally built for human AI collaboration," said Swarat Chaudhuri.
AlphaProof Code: a human-guided, multi‑agent verification workflow
Google DeepMind researchers used AlphaProof Code, a multi-agent framework, to produce a machine-checked proof that ties protocol-level security guarantees to a real cryptographic implementation. AlphaProof Code combines a human-guided agent that writes a Lean specification, agents that assess machine-code semantics, and agent-authored proofs that the Lean kernel then checks against the specification. For the Signal work, the team assigned Gemini Carbon agents to generate Lean code that would prove the correctness of the libsignal implementation.
What the verification covers: PQXDH, Triple Ratchet, and libsignal guarantees
The DeepMind effort formally verified Signal’s post-quantum PQXDH handshake and the Triple Ratchet mechanism. According to the researchers, those proofs validate the design of libsignal’s forward secrecy, authentication, post-compromise security, and handshake secrecy. The researchers emphasize that the outcome is theoretical: the verification assumes perfect cryptography and “doesn't guarantee the computational secrecy of bytes,” but they call the result “a meaningful assertion of correctness.”
The cyber insurance questionnaire just landed. Now what?
SOC 2, HIPAA, insurance renewals - someone has to own security strategy. Nubivance provides fractional CISO leadership without the full-time salary.
Get a security leadHow the team scaled the job: agents, millions of lines, and a rapid cadence
The project combined machine output and human review at scale. After the researchers translated Signal’s security goals into a human-reviewed mathematical specification, Gemini Carbon agents generated roughly 6.5 million lines of Lean code. The team then performed an auditing pass and flagged portions that required human review. DeepMind reports the Signal verification took four weeks of work from a team of five and “quite a few tokens.”
Context and comparisons offered by the researchers
DeepMind researchers framed the achievement against the historical effort required for formal verification: they note that formally verifying the seL4 microkernel took 20 person‑years and that the verified CompCert C compiler took six years to develop. The team argues AlphaProof Code can drastically reduce the cost and time of formal verification, though they acknowledge the current work is not the final word on scaling or specification practices.
Swarat Chaudhuri on verification versus specification and next steps
Chaudhuri told The Register that the project shifted the hard question in formal methods from proving theorems to deciding what to prove. “In formal methods, we always had this belief that verification is the hard bit,” he said. “Now we are able to do that. So now the question is what are we verifying? … That process is fundamentally human-in-the-loop, but we devised a process of trying to scale it up to the extent possible with AI.”
He described a research focus beyond proof: AlphaProof Nexus, a related DeepMind project, targets mathematics, and Chaudhuri said the next step is to apply these techniques during software design. “We really believe that the next frontier is not going to be proof but specification in this kind of research,” he said. “And so that's why we took on this domain where that was actually a hard problem.”
What this means for technologists, open-source maintainers, and the Beneficial AI Foundation
- Technologists and security teams: AlphaProof Code demonstrates a workflow to move from security goals to machine-checked proofs, but it also highlights the central task of writing precise, human-reviewed specifications—the step the researchers identify as the next frontier.
- Open-source maintainers and auditors: the project shows machine agents can produce large bodies of Lean code that still require human auditing; maintainers will need processes to review flagged portions rather than treat agent output as final.
- The Beneficial AI Foundation: DeepMind’s result is explicitly presented as a step toward the April challenge to formally verify the Signal protocol and Signal app with Lean, advancing the foundation’s stated goal by demonstrating a practical human–AI verification pipeline.
The verification of PQXDH and the Triple Ratchet represents a technical milestone rather than a complete security guarantee. DeepMind’s team — Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli — has shown that multi‑agent AI plus human review can produce machine-checked proofs at a speed and scale that researchers argue was previously impractical. The next questions the team has highlighted are concrete: how to write the specifications that capture the right security properties, how to fold these methods into the software design process, and how to scale the approach beyond a single protocol to “code at large.”
