Four weeks were enough for Google DeepMind to apply AlphaProof Code to security properties of libsignal, the reference implementation of the Signal protocol. The result goes beyond checking an abstract cryptographic design: the proofs concern the compiled binary for AArch64. The difference matters because a correct specification does not, by itself, guarantee that the program reaching devices retains the same properties.
The work does not prove that the entire Signal app is free of flaws, nor does it cover every part of the protocol. It focuses on key properties of its cryptographic core and on a specific version compiled for analysis. Its significance lies both in that scope and in the method: a system of AI agents generated millions of lines of formal proofs, while the decisions that determine what “secure” means remained subject to human review.
From the protocol model to the executable
Formal verification expresses program properties through mathematical specifications and proves that the code satisfies them. In this case, the team tackled libsignal, the reference implementation of the Signal protocol. Google DeepMind’s work covered the PQXDH and Triple Ratchet session-establishment protocols, with properties such as forward secrecy, post-compromise security, and secrecy of the initial exchange. The technical paper also distinguishes between the symbolic and computational models, two ways of reasoning about cryptographic guarantees.
The leap beyond much of the previous verification work lies in the level examined. According to the researchers, earlier efforts had focused on abstract models, reimplementations adapted for verification, or narrower properties. AlphaProof Code, by contrast, connected protocol guarantees to unmodified libsignal code, compiled with the standard Rust compiler to AArch64 machine code. The team describes the result as the first proofs of protocol security properties for an unmodified, widely deployed implementation.
The process combines four components: people and agents draft and review the Lean specification; Rust code is compiled into an executable; Lean represents the semantics of the machine code; and proving agents attempt to prove the agreed theorems. A control component accepts a proof only if the Lean kernel verifies it and confirms that it refers to the approved specification.
flowchart TD A["Expertos y agentes redactan la especificación"] --> B["Revisión y aprobación humana"] B --> C["Rust se compila a AArch64"] C --> D["Lean representa el ejecutable"] D --> E["Agentes generan pruebas"] E --> F["Kernel de Lean comprueba la prueba"] B --> G["Supuestos y contratos revisados"] G --> F
The scale of the result is striking: the technical paper counts around 6.5 million lines of Lean generated by the agents. But that volume does not mean millions of lines that a person must accept on trust. Lean checks the proofs with its kernel; if a demonstration contains a logical error, it should not pass that check. Google DeepMind’s publication summarizes the output as more than six million lines and says the agents flagged only one percent of the examined codebase for human review.
The specification remains the critical point
The verifier can confirm that an implementation satisfies a theorem; it cannot decide whether that theorem expresses the guarantee an organization actually needs. The specification defines the properties, input conditions, and assumptions about the environment. An overly restrictive assumption or a weakly formulated property can allow the code to “prove” something insufficient. Google DeepMind acknowledges that developing and validating this specification requires expert judgment, iteration, and review.
In Signal’s case, the agents helped adapt existing formal models, but simply transferring them verbatim was not enough: earlier models treated the initial exchange and the ratchet separately, and did not include the deployed post-quantum ratchet. The team had to compose and extend these specifications with human guidance. Reviewer agents searched for weaknesses, and the researchers tested that the assumptions were satisfiable and that the theorems held in concrete executions, to reduce the risk of a vacuous proof.
What remains within the trusted computing base also matters. The work formalizes AArch64 semantics and has Lean check that the represented bytes correspond to the executable, but the researchers explain that they cannot prove that real hardware and operating systems behave exactly as those semantics describe. In addition, the analysis depends on contracts for some external routines and on assumptions about cryptographic primitives. The proof is rigorous within those limits; it does not eliminate them.
In this sense, the proofs produced by the agents are less delicate than the claims they are asked to prove. Lean can reject a flawed proof, but it cannot by itself detect a specification that omits a relevant threat or assumes too much about the environment. This division explains why the system does not make verification an entirely autonomous task: it automates the search for proofs, not the responsibility for defining the goal.
What reintroduced bugs reveal
To test whether the method could distinguish correct code from vulnerable code, the team reintroduced two previously fixed bugs into isolated versions of libsignal. AlphaProof Code proved that the faulty variants did not satisfy the security theorems. WIRED also reports that analysis of the current code found no new vulnerabilities in the parts examined. The result validates the process’s ability to detect those known bugs, but it does not support the conclusion that every error, anywhere in the application, will be found.
The specific scope is a crucial distinction for companies seeking to interpret these proofs. The entire Signal mobile app or all its components were not verified; the cryptographic core defined by the project was examined, with an executable linked to a small test program. Nor does the proof become a universal guarantee against attacks: the properties tested and the models used establish which attacks are ruled out under the stated assumptions.
“We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that,”
— Swarat Chaudhuri, Google DeepMind researcher
Caution is also warranted when considering the timeline. The project took four weeks, compared with years of expert work that, according to DeepMind, verification of this complexity would have required using previous methods. But WIRED notes that the team built on prior formal verification work carried out by Signal. This is not a measurement of the cost of applying the system from scratch to any product: Google DeepMind conducted this analysis as a research project at no charge and did not disclose its cost. Google also did not comment on whether it plans to offer a commercial formal verification product or service.
The opportunity—and the outstanding cost—for companies
For teams maintaining critical software, the potential shift lies in the cost of producing deep proofs about existing code. The technical paper notes that previous formal verification projects for important systems took person-years; it cites twenty for the seL4 microkernel and six for the CompCert compiler. Those systems were also written with verification in mind. libsignal represents a different challenge: analyzing pre-existing production code, compiled without modification, and carrying the properties through to the executable.
The reduction in time could broaden the range of components that justify a formal effort, rather than reserving it solely for systems designed from the outset around mathematical proofs. Google DeepMind proposes extending the approach to medical device firmware and power grid software, and mentions combining it with systems such as CodeMender. For a company, this opens up an avenue for evaluation; it does not yet prove that the process is affordable or reproducible for every codebase.
That is the main trade-off: less manual work building proofs in exchange for a sustained investment in specifications, review of assumptions, and understanding of the runtime environment. The millions of generated lines reduce the burden of writing proofs, but they do not replace specialists who can decide whether the properties are appropriate, or the people responsible for defining which external components are trusted. Nor does the percentage requiring human review mean that 99% of the system was left entirely unsupervised: it means that, according to DeepMind, the agents concentrated manual review on a fraction of the code analyzed.
Google DeepMind has published the specifications and proofs so others can examine and reuse them. This openness makes it possible to study the method and its formal decisions; the next practical challenge will be to determine how much of this work can be transferred to other systems and at what cost. In Signal’s case, the proof reaches the compiled cryptographic code, but not the entire application around it.
Sources: The Decoder, Google DeepMind, Google DeepMind researchers, WIRED
