Google DeepMind's AlphaProof Code Formally Verifies Signal's Encryption in 4 Weeks
DeepMind's AlphaProof Code used Gemini agents to generate 6M lines of Lean proofs, verifying Signal's cryptographic protocol down to machine code.
- DeepMind's AlphaProof Code formally verified Signal's cryptographic protocol at the compiled-code level.
- Gemini Carbon agents generated over 6 million lines of Lean proofs in four weeks.
- Human experts only reviewed 1% of the codebase; Lean mechanically checked the rest.
- System correctly flagged two reintroduced historical bugs as insecure, confirming it isn't rubber-stamping.
- First deployed cryptographic protocol ever verified down to machine instructions by any method.
- Artifacts open-sourced at google-deepmind.github.io/code-verification, with a technical paper available.
Google DeepMind says it has formally verified key security properties of compiled cryptographic code used by Signal and Google Messages. Its new AlphaProof Code framework generated proofs that were checked by Lean, a proof assistant with a small verification kernel. The project took four weeks and covered software that protects billions of messages each day.
DeepMind describes the work as the first AI-assisted formal verification of a widely deployed cryptographic protocol at this depth, as well as the first implementation-level verification of such a protocol by any method. The proof addresses a persistent engineering risk: a protocol may be secure in its mathematical model while its implementation mishandles keys, state transitions, or edge cases.
A proof that reaches the binary
Formal verification expresses software requirements as mathematical statements and supplies proofs that each statement follows from the program’s behavior. Most protocol analyses stop at an abstract design. AlphaProof Code connects human-approved security specifications to the covered compiled implementation, reducing the gap between the protocol model and the instructions executed by the analyzed build.
The verified properties include forward secrecy, which limits exposure of older messages after a current key is compromised, and post-compromise security, which allows future messages to become secure after an attacker loses access and the cryptographic ratchet advances.
| Layer | What was checked |
|---|---|
| Protocol behavior | Ratchet state transitions, forward secrecy, and recovery after temporary key compromise. |
| Implementation | The target properties hold for the covered compiled code under the project’s execution model. |
| Proof validity | Lean’s kernel mechanically checks every accepted proof term. |
| Specification mapping | A trusted gatekeeper confirms that generated theorems correspond to specifications approved by human experts. |
| Scope limits | The result does not certify the entire application, operating system, hardware, metadata handling, or behavior absent from the specification. Timing leakage and hardware faults also remain outside the guarantee unless explicitly modeled. |
Signal CTO Ehren Kret said the approach increases confidence in the implementation’s privacy guarantees by translating live code into valid Lean theorems. The assurance remains tied to the verified version, build assumptions, formal specification, and modeled environment.
Three stages, one checked result
AlphaProof Code divides the verification campaign among human experts and several model-driven agents. Humans retain control over the security requirements and review the resulting specifications, while agents perform most of the proof construction and auditing.
- Specification. Researchers used multiple models to translate Signal’s security requirements into formal statements. Human experts reviewed and approved each specification.
- Proof generation. Agents powered by Gemini produced over three million lines of machine-checked proof in Lean. Lean accepted only proofs that its kernel could validate.
- Audit. Additional agents examined the proof corpus for suspicious assumptions, weak statements, and areas requiring expert review. The process directed humans to roughly 1 percent of the material.
The trust boundary excludes the proof-generating models. Their output can contain errors or irrelevant arguments, but those artifacts fail unless Lean can check them. The trusted components are the proof kernel, the gatekeeper that connects theorems to approved requirements, and the human-reviewed specifications.
Four weeks and two planted bugs
A four-week verification run represents a substantial reduction in labor compared with hand-built formal-methods projects, which have often required years of specialist work. Projects such as seL4, HACL*, and CompCert addressed different systems and proof goals, so their timelines are useful context rather than direct benchmarks.
DeepMind also tested whether the workflow could reject insecure code. Researchers restored two previously fixed vulnerabilities in an isolated version of Signal’s implementation. According to the company, AlphaProof Code generated machine-checked evidence that each modified build violated the relevant security property. That evidence provides a stronger diagnostic than an incomplete proof attempt, which can also result from missing lemmas, insufficient compute, or faulty tooling.
Where the economics work
Formal verification pays off most readily when code changes slowly, failures carry high costs, and engineers can state the required behavior precisely. AlphaProof Code may reduce proof-writing costs, but experts still have to define the properties, approve the formal model, review flagged material, and repeat verification after relevant changes.
| Workload | Verification case | Main constraint |
|---|---|---|
| Cryptographic libraries | Strong, because security properties can often be stated mathematically. | Side channels and platform-specific behavior require separate models. |
| Bootloaders and firmware | Strong for compact components with stable interfaces. | Hardware assumptions must be explicit. |
| Consensus protocols | Strong when safety and liveness requirements are precise. | Distributed timing and fault models increase complexity. |
| Medical and grid controllers | Potentially strong for small, high-consequence control paths. | Certification rules and physical behavior extend beyond software proofs. |
| Rapidly changing product code | Limited when requirements and interfaces change frequently. | Specification maintenance can outweigh the value of each proof run. |
Developers can inspect the proofs
DeepMind has published the Signal specifications and proof artifacts in an artifact repository, accompanied by a technical paper. Researchers can inspect the formal claims, replay the available checks, and extend the work to related implementations.
The AlphaProof Code framework has not been released as a general-purpose package. The public materials provide proofs and specifications rather than an installable service for verifying arbitrary repositories.
Maintenance is the next benchmark
Production value will depend on how efficiently teams can update proofs when source code, compiler settings, target architectures, or specifications change. Reproducible builds, incremental proofs, independent audits, and integration with release pipelines will determine whether the four-week result can become a repeatable engineering process.
DeepMind is also developing CodeMender, an agent intended to find and patch vulnerabilities. Combining automated repair with machine-checked verification could give security teams a path from defect discovery to a formally validated fix. AlphaProof Code provides a concrete test of that approach while leaving final authority with explicit specifications, a small proof checker, and human review.
Comments
