Google DeepMind's AlphaProof Proved Signal's Encryption With Math in Four Weeks
Google DeepMind has pulled off something cryptographers have talked about for years. On November 10, the lab said its AI agents mathematically proved that the code behind Signal’s encryption does what it promises, finishing in four weeks. The work covers the protocol guarding private chats in Signal, WhatsApp, and Google Messages, touching billions of conversations a day. The project is called AlphaProof Code. A five-person team guided Gemini Carbon agents as they generated more than six million lines of proof in Lean, a language built for checking mathematical arguments. Lean’s kernel then checked every line, and a proof that doesn’t hold gets thrown out. ...