Testing software shows it works in the cases someone tried. A formal proof shows it behaves as specified in every case, but writing one has usually taken expert teams years. Google DeepMind says its AlphaProof Code system, which uses teams of AI agents, has done this for the core encryption code behind Signal’s one-to-one messaging in about four weeks.
The agents wrote about 6.5 million lines of proof in the Lean language, each step checked by Lean’s proof checker, against specifications that human experts reviewed. The proofs cover the code as compiled to run on a processor, not just the protocol design, and include guarantees such as keeping messages safe after a device is temporarily compromised. As a test, the team put two old, already fixed bugs back in, and the system proved those versions insecure. Signal’s chief technology officer, Ehren Kret, called the approach “a major breakthrough”.
The limits matter. The proofs assume the underlying cryptography is sound, cover a command-line build rather than the Android and iOS apps, and do not yet cover group chats, several linked devices or, in one part of the proof, quantum attackers. Google DeepMind has published the proofs so others can check them.