Overview
- Google DeepMind used an agentic framework called AlphaProof Code with Gemini Carbon models to turn Signal’s security goals into formal Lean specifications and machine-checked proofs of parts of the protocol implementation.
- The agents produced over six million lines of Lean that check implementation-level properties, including guarantees about message protection before and after a device is temporarily compromised.
- DeepMind tested the system by reintroducing two long-fixed, real bugs into isolated Signal code and the agents correctly flagged those versions as insecure.
- The research team open-sourced the specification and proof artifacts and used a human–AI workflow in which human experts reviewed about one percent of the code that agents flagged for attention.
- DeepMind says the result is a research milestone but it covers only portions of the Signal mobile implementation and leaves open questions about how to scale the method and make it cost-effective for larger codebases and critical systems.