DeepMind's AI proved that Signal's encryption code keeps its key security promises

Google DeepMind says its AI agents have mathematically proven that the code behind Signal's encryption for one-to-one chats delivers its main security promises. The work, announced on November 10, used a new framework called AlphaProof Code and checked the compiled program itself, the code that actually runs. According to DeepMind, this is the first time the implementation of a widely deployed cryptographic protocol has been formally verified by any method, with or without AI. The proof found no new flaws in the parts it covered.

Formal verification means writing down a security property as a mathematical statement and proving that the program always satisfies it, instead of testing it on examples. Most work on protocols like Signal stops at the design. DeepMind went down to the machine code: the team took libsignal version 0.105.4 and the spqr library, compiled them for 64-bit ARM Linux with the standard Rust compiler and reasoned about the resulting executable, the technical write-up says.

Researchers and several AI models first turned Signal's security goals into formal specifications, and humans reviewed every one. Then agents running on Gemini Carbon wrote the proofs in Lean, a language whose checker confirms every step automatically. The result is about 6.5 million lines of proof. The agents flagged roughly 1% of it for human review, and the whole project took four weeks. Among the ten proven theorems are forward secrecy, which keeps past messages safe if a key leaks later, and post-compromise security, which restores protection after a device has been temporarily hacked.

Read the full article on vpnlab.io: https://vpnlab.io/en/deepmind-ai-proves-signal-encryption-code-3297