Introducing AlphaProof Code: a breakthrough in verifying complex software at depth

Google DeepMind researchers used AlphaProof Code, a multi-LLM agentic framework combining human expertise with AI agents, to formally verify key security properties of the actual code underlying the Signal protocol, generating over six million lines of Lean. The verification took four weeks, and when two previously fixed bugs were reintroduced into an isolated version of Signal's code, the system produced machine-checked proofs that the buggy versions were insecure. DeepMind is open-sourcing its formal verification artifacts.