Google DeepMind's AlphaProof Code uses AI agents to formally verify Signal's libsignal down to AArch64 machine code
- What it does and doesn't cover: the proofs assume the cryptographic primitives are secure and trust contracts for some low-level routines; no new Signal vulnerabilities were reported.
- Why it matters: if agents can make formal verification cheap, it becomes a defensive counterweight to AI-driven bug hunting. The Lean development is published for others to reuse.
Sources: Google DeepMind: Introducing AlphaProof Code (Nov 10, 2026) · AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (paper, Nov 10, 2026)