Google DeepMind formally verifies Signal’s encryption mathematically
Google DeepMind has announced AlphaProof Code, a system designed to transform software security specifications and implementation details into machine-checkable mathematical proof obligations. The team applied the new system to the cryptographic core of the Signal messaging protocol, generating and checking millions of lines of Lean language proofs over the course of several weeks.