Google DeepMind's AlphaProof Code formally verifies Signal's encryption code
The gist
Google DeepMind's AlphaProof Code formally verified key security properties of Signal's actual code in about four weeks.
The result is research, not a product, and assumes perfect cryptography.
How it unfolded
- Apr 2026The Beneficial AI Foundation issued a challenge to formally verify the Signal protocol and Signal app with Lean.
- Nov 10, 2026Google DeepMind introduced AlphaProof Code and announced it had formally verified key security properties of the actual code underlying the Signal protocol.
- Nov 10, 2026A five-person team completed the project in about four weeks; agents generated over six million lines of Lean, resting on roughly 26,000 lines of trusted specifications and AArch64 semantics.
Key terms
- formal verification
- Proving or disproving a system's correctness against a formal specification using mathematical methods.
- multi-LLM agentic framework
- A computational system of multiple interacting intelligent agents, here built on large language models, that coordinate to solve problems.
- post-quantum
- Cryptographic algorithms designed to resist cryptanalytic attacks by quantum computers.
Source: Wikipedia