DeepMind reports agents formally verified Signal's protocol code, with humans reviewing the specifications

DeepMind describes AlphaProof Code as a multi-LLM agentic framework in which human experts and AI decide what to prove and a group of agents does the proving. Its researchers worked with models to turn Signal's security goals into formal specifications, and "human experts reviewing every one" of them. Agents powered by Gemini Carbon then generated over six million lines of Lean, and audited the proofs to flag the roughly one percent of the codebase that needed a second human look. DeepMind says the proofs cover the compiled code, not just the protocol design, and that the process took four weeks, a task it says historically takes expert teams years. As a check, it reintroduced two previously fixed Signal bugs into an isolated copy; in both cases it says the system produced a machine-checked proof that the buggy version was insecure. Signal's CTO, Ehren Kret, is quoted in the post endorsing the work. DeepMind says it is open-sourcing the verification artifacts. The post links a technical paper, which this edition did not read, so the scope of what was proven rests on DeepMind's summary.

Why it matters: The structure is a verification loop with the human work moved to the specification, where a wrong spec makes every proof meaningless, while Lean checks the agents' output mechanically. If the artifacts hold up when others run them, that is a concrete pattern for gating agent-written code on a checker instead of on reviewer attention. Until then, the four-week and one-percent figures are DeepMind's.