DeepMind says AlphaProof Code verified security properties of libsignal

Google DeepMind introduced AlphaProof Code and says the system proved key security properties of libsignal, the Signal protocol's reference implementation, at the machine-code level, The Hacker News reported. The work covers the post-quantum PQXDH handshake and Triple Ratchet, including authentication, forward secrecy, post-compromise security and handshake secrecy. Human experts guide an agent that writes specifications in Lean, a system for checking mathematical proofs. Autonomous agents then produce proofs accepted only when Lean's kernel checks them against the approved specifications. DeepMind says the work generated about 6.5 million lines of machine-checked proof code, resting on about 26,000 lines of trusted specifications and AArch64 machine-code semantics.