DeepMind reports formal proofs for specified Signal security properties

What happened: Google DeepMind announced AlphaProof Code on 10 November. Its human-guided agents produced formal proofs about specified security properties of libsignal, the Signal protocol’s reference implementation, at the compiled machine-code level. The accompanying research describes Lean-checked theorems and explicitly listed assumptions. DeepMind says the verification work took four weeks.

Why it matters: This is a concrete example of AI helping produce independently checkable mathematical evidence about software, rather than simply suggesting code or identifying likely bugs. It could lower the effort needed to verify security-critical components.

Caveat: The result covers specified properties under stated assumptions. It does not establish that the complete Signal application, every deployment, or future versions are immune to attack. The timeline is a researcher-reported result, not a general benchmark.

Dates: Research announcement and source publication, 10 November 2026; the four-week project preceded publication.