Back to News

DeepMind's AlphaProof Code verifies Signal protocol in four-week proof-of-concept

#deepmind#signal#formal verification#lean

Google DeepMind researchers used the agentic AI framework AlphaProof Code to formally verify the cryptographic guarantees of the Signal protocol in a four-week proof-of-concept. The agents wrote three million lines of proofs in Lean to verify Signal's core encryption, marking a breakthrough in verifying complex software at depth.

Coverage timeline

  1. Techmeme
    Google DeepMind researchers used agentic AI framework AlphaProof Code to verify the Signal protocol's cryptographic guarantees, in a four-week proof-of-concept (Lily Hay Newman/Wired)

    Lily Hay Newman / Wired : Google DeepMind researchers used agentic AI framework AlphaProof Code to verify the Signal protocol's cryptographic guarantees, in a four-week proof-of-concept — DeepMind researchers were able to formally verify that the widely used encryption protocol works as intended. Their stretch goal?

  2. Google DeepMind Blog
    Introducing AlphaProof Code: a breakthrough in verifying complex software at depth

    AlphaProof Code agents wrote three million lines of proofs in Lean to verify Signal’s core encryption.

Related stories

  • Anthropic open-sources FlashProve for cryptographic verification of AI model identity

    Anthropic released FlashProve, an open-source prototype that uses zero-knowledge cryptography to verify that an AI response came from a specific model, preventing routers or providers from swapping in cheaper models. Tested on a 400B-parameter mixture-of-experts model, it generates proofs at about 110 tokens per second on a single NVIDIA H100 GPU, with proof files around 19 MB per 1024-token request. The release includes proof generators, C++ and Lean verifiers, documentation, and formal proofs.

    3 reports · 3 sources

  • Google DeepMind Uses AI Agent Antigravity and ProtNLM to Discover Novel Antimicrobial Peptides

    On October 15, Google DeepMind published a technical demo showing how its AI agent platform Antigravity and ProtNLM model can discover novel antimicrobial peptides (AMPs) from protein databases. The workflow narrowed millions of UniProt records to a candidate bacteriocin from Streptococcus pseudopneumoniae, which has entered wet-lab validation.

    1 reports · 1 sources

  • Google DeepMind unveils Gemini 4 Carbon, tops AI benchmark

    Google DeepMind announced Gemini 4 Carbon, its next frontier model, claiming state-of-the-art performance in cybersecurity and long-horizon tasks. The model scored 59 on the Artificial Analysis Intelligence Index v5.0, ranking first ahead of Claude Opus 5.5 (58) and GPT-6 Astra (57). It is initially available only to select cybersecurity defense companies through the Fairwind program, with pricing at $2 per million input tokens and $10 per million output tokens, rising to $4 and $20 later.

    8 reports · 6 sources1013 points · 801 comments

  • Anthropic: Claude flags 493 security issues across 25 open-source projects

    Anthropic reported that Claude identified 493 security issues across 25 open-source projects, covering over 5 million lines of C, C++, Java, PHP, and Python code, including one vulnerability that went unnoticed for 21 years. The lab also announced a partnership with Theorem to use Claude for formally proving security properties at the assembly level across more than 100 real-world open-source libraries, extending formal verification to larger codebases.

    4 reports · 3 sources460 points · 310 comments

News updates every hour. Subscribe in your RSS reader to get new stories automatically.

Subscribe