FORMAL VERIFICATION

AlphaProof Code produces machine-checked proofs for Signal cryptography

By IDAKIM Digital · Published November 11, 2026

DeepMind describes a research workflow combining human-reviewed specifications, AI-generated Lean proofs and kernel checking.

Google DeepMind introduced AlphaProof Code on November 10, describing research on key security properties of Signal’s cryptographic implementation. Human experts reviewed formal specifications derived from the security goals, after which Gemini Carbon-powered agents generated Lean proofs. Lean checked the proofs against those specifications. DeepMind reports that the work reached compiled implementation code, extending beyond protocol-design analysis, and took four weeks in this particular research effort. As a countercheck, researchers restored two previously fixed bugs in an isolated version and obtained machine-checked proofs of insecurity. The team is releasing formal-verification artifacts and a technical paper for community inspection. This is a distinct research result rather than a general claim that AI can certify any application. A valid proof still depends on the chosen properties, modeling assumptions and trusted components. It also does not establish the security of every interface, device or operational practice around a messaging system.

Why it matters

For critical software, define the property and trusted boundary before choosing an automated prover. Inspect the released artifacts and specification coverage; a passing test and a checked proof answer different questions.

Source: Google DeepMind · November 10, 2026

Product claims are attributed to the linked publisher. IDAKIM Digital has not independently tested these claims.