Google DeepMind's AlphaProof Code formally verifies Signal's encryption code

Google DeepMind introduced AlphaProof Code, a multi-agent framework in which human experts and AI agents write Lean specifications and Gemini Carbon-powered agents prove that code meets them. Applied to libsignal, Signal's reference implementation, the agents generated about 6.5 million lines of machine-checked proofs covering the post-quantum PQXDH handshake and Triple Ratchet at the AArch64 machine-code level, establishing forward secrecy, authentication, post-compromise security and handshake secrecy. DeepMind says the work took four weeks and is the first formal verification of a widely deployed protocol's implementation at that depth. No new vulnerabilities were found; when researchers reintroduced two previously fixed bugs, the system produced proofs showing those versions were insecure. The specification and proofs are being released publicly.