Summary
- AlphaProof Code generated approximately 6.5 million lines of machine-checked proof covering selected security properties of compiled libsignal code.
- The work examines the PQXDH handshake and Triple Ratchet, with guarantees depending on distinct stated attacker models and cryptographic assumptions.
- The result does not establish that every component of the Signal application or every possible attack scenario is secure.
Researchers at Google DeepMind have used AI agents to mathematically verify selected security properties of compiled Signal protocol code, demonstrating a method for checking whether cryptographic software behaves according to a formally approved specification.
The research, published on 10 November, introduces AlphaProof Code, a framework that combines human-guided specification writing with autonomous proof generation and a separate mathematical verification system.
Applied to libsignal, the reference implementation of the Signal protocol, the system produced approximately 6.5 million lines of proof code in Lean, a programming language and theorem prover used for formal verification.
The researchers report completing the work in approximately four weeks, covering security properties associated with Signal’s post-quantum PQXDH handshake and Triple Ratchet.
The proven properties include authentication, forward secrecy, post-compromise security and message confidentiality, subject to the mathematical definitions and assumptions used in the project. The paper’s guarantee against a quantum adversary concerns handshake secrecy in its symbolic model; other properties are established under the specified classical or additional attacker models rather than a universal quantum-security claim.
Verification moves beyond protocol design
Cryptographic protocols are frequently evaluated through mathematical models describing how messages, keys and adversaries behave. Such models can establish strong guarantees for a design but do not independently prove that the software implementing it follows those rules.
AlphaProof Code attempts to narrow that gap by reasoning about compiled machine code, rather than only an abstract protocol specification or specially rewritten reference implementation.
The researchers compiled the existing Rust implementation using a standard compiler and examined its behaviour through a formal model of AArch64 machine code.
Human researchers worked with AI agents to define the properties the compiled code should satisfy. Once specifications were reviewed and approved, other agents generated candidate proofs that were checked by Lean’s kernel.
The separation is essential. An AI system may propose faulty mathematical reasoning, but the trusted proof checker accepts only proofs that satisfy the formal rules of the verification environment.
That process cannot eliminate mistakes in the specification itself. If a property omits a relevant attack scenario, a mathematically valid proof can still leave the omitted risk outside its scope.
The work also depends on assumptions concerning cryptographic primitives, machine-code semantics and supporting functions. Those dependencies form part of the trusted basis on which the conclusions rest.
Post-compromise protection receives scrutiny
Signal’s cryptographic protocol is designed to protect conversations even when some secret material is exposed. Forward secrecy limits what an attacker can learn about earlier communication after obtaining certain later keys.
Post-compromise security concerns the restoration of protection for subsequent communication when an attacker no longer retains access to previously compromised material.
These guarantees depend on how communicating devices create new secrets, authenticate their peers and update cryptographic state. They require more than encrypting each message individually.
The project examines the interactions between PQXDH and Triple Ratchet, introducing further complexity associated with post-quantum cryptography and the continual evolution of session keys.
To test whether the framework could distinguish correct and incorrect code, researchers reintroduced two previously fixed libsignal defects into isolated versions of the implementation.
AlphaProof Code produced machine-checked results demonstrating that the altered implementations violated the relevant specified security properties.
Those tests support the framework’s ability to detect these two known defects. They do not prove that it will identify every unknown vulnerability or operate equally well on unrelated software.
Formal guarantees remain bounded
The research provides a different type of assurance from conventional vulnerability scanning. Testing samples selected program behaviours, while formal verification can establish that every behaviour represented in a defined mathematical model satisfies a particular requirement.
That distinction can be valuable for cryptographic software whose protections are relied upon by many applications and organisations, although the scope of the verified component must remain clear.
Verification of compiled cryptographic routines does not encompass every aspect of a messaging service. User interfaces, operating systems, devices, network services and supporting application code may contain vulnerabilities outside the proved functions.
Nor does it establish that the underlying assumptions remain valid after implementation changes, compiler modifications or deployment to a different architecture.
DeepMind has published the paper and associated proof artefacts for examination. The project demonstrates that AI-assisted formal methods can reach complex production implementations while leaving decisions about specifications and trusted assumptions to human specialists.
The result establishes guarantees for selected aspects of libsignal under the paper’s stated models. It does not constitute a general security certification for the complete Signal application or every possible attack scenario.
