---
title: 'In the News: November 10, 2026 (Extra)'
description: "DeepMind says agents wrote Lean proofs that Signal's protocol code meets its security specs in four weeks; humans reviewed the specs and about 1% of the codebase."
canonical_url: 'https://darkfactory.dev/news/2026-11-10-extra'
markdown_url: 'https://darkfactory.dev/news/2026-11-10-extra.md'
collection: news
date_published: '2026-11-10T10:20:00-05:00'
date_modified: '2026-11-10T10:20:00-05:00'
---

# In the News: November 10, 2026 (Extra)


Google DeepMind says its agents produced machine-checked proofs that the code behind Signal's protocol meets human-reviewed security specifications. The claim is the vendor's, the paper was not read, and the useful part for anyone running agents is where the human review sat.

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

**[Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/)** · Pushmeet Kohli and Swarat Chaudhuri, Google DeepMind · November 10, 2026

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.