tl;dr: Google DeepMind used a new agentic framework called AlphaProof Code to formally verify the implementation of Signal's cryptographic protocol, generating over 6 million lines of Lean proofs in four weeks—a task that typically takes expert teams years. The system had humans define specifications while AI agents produced the proofs, flagging only ~1% of the codebase for human review, and successfully detected two reintroduced known bugs. DeepMind is open-sourcing the verification artifacts.