Google DeepMind researchers deployed AI agents powered by Gemini to generate over six million lines of Lean to mathematically prove key security properties of the code underlying the Signal protocol. Signal's cryptographic mechanisms protect billions of conversations in products such as Google Messages and Signal itself. The project tackled a longstanding industry bottleneck: verifying the mathematical soundness of compiled code at production depth.
Formal verification provides mathematical proof that software runs correctly without flaws. While protocol verification historically stops at the architectural design level, real-world vulnerabilities often exploit the gap between design and implementation. As the DeepMind research team documented, bridging this gap makes proofs vastly more complex, yet the automated framework narrowed the scope of mandatory human scrutiny to an operational fraction.
"Our verification process took just four weeks – a task that historically takes expert teams years – proving that Signal's core cryptographic code delivers the security protections our experts specified."
Automating the generation of valid Lean theorems alters the economics of cryptographic auditing. Instead of funding multi-year specialized engineering reviews, organizations can focus human oversight strictly on the areas identified as requiring judgment. When factoring in enterprise adoption, implementation costs will depend heavily on licensing factors, underlying model compute overhead, and the specialized personnel required to write initial formal specifications before broader commercial deployment materializes across industrial environments over the next three to five years outside of benchmark protocol tests.
The Human Review Boundary
How did the system allocate labor between autonomous agents and human specialists?
The framework relied on a division of responsibilities where humans and models drafted formal parameters while automated systems generated and checked the proofs. Researchers collaborated with a mix of models to translate Signal's security goals into formal mathematical specifications, with human experts reviewing every specification. Following that baseline, AlphaProof Code audited the generated proofs and highlighted areas that needed a second look by a human, which accounted for just one percent of the codebase.
The research, developed by Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli, applied this division directly to live software implementations. Verifying that production code strictly matches its cryptographic design has traditionally demanded manual formalization. The resulting artifacts demonstrated mathematical proofs that messages remain protected before and after a device is temporarily compromised.
Implementation Defenses and Market Scope
To test whether multi-model agentic systems can reliably detect flaws in executable code rather than merely confirming abstract specifications, researchers reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both instances, AlphaProof Code produced a machine-checked proof confirming that the buggy version was insecure.
"AlphaProof Code is a novel agentic framework for formal verification at unprecedented depth that combines human expertise with AI agents."
Google DeepMind stated that verifying Signal's core cryptography lays the groundwork to secure other systems, including medical device firmware and power grid software, and announced it is open-sourcing its formal verification artifacts for community use. Pairing formal verification with automated defense agents like CodeMender is presented as an answer to agent-driven cyber threats.
Open-sourcing formal verification artifacts invites enterprises to eliminate human auditing overhead, yet the math still demands expert researchers to write the initial formal specifications and manually inspect the flagged edge cases.
What it signals
Exactly one percent of the codebase requiring manual human review turns mathematical security proof from an academic exercise into a workable engineering process. According to Google DeepMind, the whole verification run took just four weeks rather than the multi-year efforts previously needed from entire expert teams. Autonomous agents absorb the bulk of mechanical theorem generation, leaving specialists to police the initial specifications. Machine proof generation turns critical software auditing from a multi-year slog into a targeted review of model output.