AI Agents Proved Signal Properties Down to Machine Code. The Specification Still Needs You

A cryptographic protocol can be sound on paper while its implementation mishandles a state transition, a counter or a compromise. The hard question is whether the code people actually run preserves the promised properties. Google DeepMind’s AlphaProof Code project takes an unusually direct route: it connects formal proofs to a compiled AArch64 binary of libsignal, the reference implementation of the Signal protocol.

The team reports about 6.5 million lines of machine-checked Lean proof code. The key distinction is that the agents may search for proofs, but Lean’s small trusted kernel checks whether each proof follows from the approved statements. The result is an engineering workflow in which machine-generated proof labor can scale while the mathematical checker remains the final gate. ^[1]

What was actually proved

The paper focuses on a command-line harness around the unmodified Rust libsignal code, compiled with the stock Rust compiler to AArch64 Linux machine code. The properties concern Signal’s PQXDH handshake and Triple Ratchet. The authors report proofs for forward secrecy, authentication, post-compromise security and handshake secrecy, across symbolic and computational models. The symbolic analysis also considers a future attacker who can break Diffie–Hellman after the handshake. ^[2]

That matters because many formal analyses stop at an abstract protocol model. A model can establish that a design is secure if implementations follow its rules; connecting the result to compiled instructions addresses a harder refinement question: does this executable behave according to the model closely enough for the theorem to apply?

The framework has three main stages. Human experts and AI assistants draft and review Lean specifications of code and security goals. The unmodified implementation is compiled, and its machine instructions are interpreted through a formal AArch64 semantics. Then prover agents attempt to establish that the executable satisfies the approved specification. A gatekeeper checks the proof with Lean and checks that the theorem proved is the held-out specification, reducing the chance that a proof silently changes the target. ^[2]

The proof checker is not the whole trust story

“Machine checked” describes the proof object’s verification, not the automatic correctness of every premise. The paper is unusually useful because it lists the trusted boundary. A person must decide that the specification captures the intended security property. The work trusts Lean’s kernel, the modeled semantics, cryptographic assumptions in the computational proof and contracts for some routines called by the harness. It also scopes the execution environment: the guarantees describe a fresh process with constrained inputs, open files, environment and clock, not every operating system configuration. ^[2]

This is not a weakness unique to AI-assisted proof. Formal verification always proves a statement from assumptions; the difficult human task is choosing a statement that matches the real security question. An impeccable proof of an incomplete specification can still miss an important bug. Here, the authors say they reintroduced two previously fixed bugs and showed that the resulting binaries violate the symbolic theorems. That is a valuable check that the properties are sensitive to some real implementation mistakes, not evidence that every class of bug is covered. ^[2]

The paper also identifies limits: the computational proof is classical; some post-quantum healing properties are not established; the model constrains session and message assumptions; and scope does not include Signal group messaging, sealed sender or server-side protocols. Those details matter more than a broad “verified” label. The work increases confidence in particular claims about a particular artifact under stated assumptions.

Why AI changes the economics, not the logic

Formal verification has often been expensive because experts must translate an informal security goal into a precise specification, connect software to a formal model and build lengthy proofs. The project’s authors argue that proof generation is now more automatable, while specification engineering remains the bottleneck. In their design, humans choose the properties and resolve ambiguity; agents draft, critique and prove; a theorem checker rejects invalid proof terms. ^[2]

That division is more durable than treating an AI agent as a security auditor whose conclusion must be trusted. The agents can make mistakes without invalidating a checked theorem. But a human can still approve a weak theorem, an unmodeled dependency can remain outside scope, and the proof may describe a build different from the artifact users install. Correctness therefore depends on provenance: source revision, compiler, target architecture, harness, assumptions and binary hash should travel with the proof.

The authors’ public Lean development makes the work inspectable and reusable. It does not make formal methods plug-and-play. A team needs people who can model the threat, state the property, challenge the assumptions and maintain the proof as code evolves. A repository update that changes the compiled artifact can invalidate the assurance even if the high-level design appears unchanged. ^[3]

A practical way to start

Most teams do not need to begin by proving a messaging protocol. Choose a narrow boundary where failure has a clear cost: authorization checks for a payment transition, a parser for signed update metadata, a state machine controlling key rotation or a safety interlock. Write down the attacker capabilities and the property in plain language before translating it into a formal model.

Then keep three artifacts linked: the exact code or binary, the specification and its assumptions, and the proof result. Review the assumptions as carefully as the theorem. Test whether known historical bugs violate the property, as the Signal study did. Finally, make the release process fail closed when the artifact changes without a corresponding verification run.

The deeper lesson is not that AI makes software unhackable. It is that AI may lower the cost of exploring proofs, while a small checker can keep the correctness decision grounded in mathematics. The hard work shifts toward deciding what deserves to be proved and ensuring the theorem still describes the system that reaches users. For a related look at how AI-assisted security work is being evaluated, see our analysis of verifying a software supply-chain fix.