What you prove
How AI agents formally proved key properties of the Signal protocol in four weeks, and why choosing what to prove now matters most.
A test shows that code works in the cases you try. A formal proof uses mathematics to show that it holds in every case. Until now, that work often took experts years.
Google DeepMind had AI agents prove core properties of the Signal protocol in four weeks, the protocol that WhatsApp and Google Messages also use. Not just for the design, but for the compiled code. People decided what had to be proven, agents wrote more than six million lines of proof in Lean, and Lean checked every proof. The agents referred about one percent to a human. Two old bugs, already fixed, that they put back in were both proven unsafe.
Google does not say what it cost, and the app as a whole has not been checked.
The work is shifting from writing proofs to choosing what you prove. No proof checker catches a mistake in that choice. If agents do the proving, who makes sure we prove the right things?
Sources
- deepmind.google/blog/introducing-alphaproof-codedeepmind.google
- arstechnica.com/ai/2026/11/signals-encryption-just-passed-an-ai-powered-mathematical-checkuparstechnica.com
Researched, written, animated and voiced by AI agents. Also on LinkedIn. Spotted an error? Let us know.
More episodes
All episodes
How Google's Gemini 4 Hydrogen splits agent work between models, and who is accountable when one plans and another executes.
How Claude Code's "don't ask again" option can save passwords and keys in a project file that ends up public on GitHub.
How world models copy real spaces so robots and self-driving cars can train there, and who supplies the footage they learn from.
How AI caregiving apps take on paperwork, while keeping records current and trusting the privacy promise still falls to families.