DeepMind's AlphaProof verifies Signal protocol code; 7.5M-line Lean release audited
kevrussell · x · 2026-11-11
DeepMind announced that its team used AI (AlphaProof) to formally verify key security properties of the machine code underlying the Signal messaging protocol — claimed as the first deep formal verification of a widely deployed protocol's actual production code. Pushmeet Kohli framed it as frontier AI acting as a force multiplier against modern cyber threats, noting such efforts traditionally take teams decades.
Third-party honesty.tools read the released repo (google-deepmind/code-verification @808b4b7) and flagged:
- Scale checks out: 11,323 Lean files, 7.5M raw lines (fits "over six million", not the circulating "three million"); 37 hooked routines (23 crypto primitives + 14)
- Scope caveats: it's a static scan of AArch64 Linux libsignal-cli, not Signal's phone apps; no kernel check; 23 crypto primitives idealized, 14 contracts unproved vs real routines; keygen out of scope; TRUSTEDBASE.md missing
- Authors state they haven't run the kernel build and have no planted-bug results
Bottom line: a big, real artifact, but read the claims with its verification limits in mind.
More from Safety
- New York Launches First State-Led Independent AI System Testing Program — peterwildeford · 2026-11-11
- Valthos unveils Grove, an AI biodefense platform for identifying novel biological threats — graceisford · 2026-11-11
- Railway discloses Oct 21 breach: misconfigured OIDC binding exposed cloud credentials — letandrewcook · 2026-11-11
- New York AI safety law takes effect, OpenAI and Anthropic face new oversight — TechCrunch AI · 2026-11-11
- Critique: Was That 90% AGI Forecast Conditioned on No Policy Intervention? — austinc3301 · 2026-11-11
- Sayash Kapoor, Rishi Bommasani, Arvind Narayanan launch nonprofit STABL on AI societal bottlenecks — soumitrashukla9 · 2026-11-11