AlphaProof Code and Signal: What the Security Proof Actually Covers

A proof establishes a statement, not a slogan

Formal verification starts by stating what a program must satisfy. A proof checker then verifies that a proposed proof establishes that statement from the definitions and assumptions provided.

That gives a different kind of evidence from running a test suite. Tests examine chosen executions. A formal theorem can cover every execution permitted by its model, but only for the property actually stated.

The distinction matters because an incorrect or weak specification can still have a valid proof. If the statement omits an attack or assumes away an important condition, proof checking does not turn it into a stronger claim.

AlphaProof Code's authors place human work at that boundary: choosing the properties, reviewing the definitions and deciding whether the resulting specification expresses the intended security goal^[1].

The verification target is a particular executable

The paper targets libsignal's one-to-one session code, specifically libsignal v0.105.4 with SPQR v1.6.0. The researchers wrapped the unmodified crates in a command-line harness called libsignal-cli and compiled it into a statically linked AArch64 Linux executable^[2].

The main theorems cover the harness's init, send and recv operations. Key generation is not verified; keys enter as part of the setup. The exact execution environment also matters, including the process model and assumptions about memory and other inputs.

Those details are not footnotes to discard. They identify the artifact and behavior the proof concerns. A theorem about that executable is not automatically a theorem about every build, operating system, UI feature or configuration that uses related source code.

The paper explicitly says the results concern its build of libsignal-cli, run as a fresh process, rather than Signal's own applications. The authors discuss conditions under which the result is relevant to other environments, but that transfer itself depends on preserved behavior.

Why machine-code verification is a meaningful step

Earlier verification can reason about a protocol design or an implementation written to be easy to verify. This project connects protocol-level security properties to the compiled code of an existing implementation.

The authors compile the unmodified library with a stock toolchain and reason about the resulting AArch64 bytes. That moves the assurance closer to what a machine executes and avoids needing to assume that the compiler translated the relevant source correctly^[1].

It does not remove every trusted component. The model of AArch64 execution, the Linux process environment, the theorem definitions and contracts for some called routines still matter.

The right takeaway is a changed trust boundary, not no trust boundary. The work reduces one gap between an abstract protocol argument and a deployed implementation while retaining explicit assumptions elsewhere.

Humans review the specification; Lean checks the proof

AlphaProof Code uses AI assistance to draft and review formal specifications under human guidance. Once a specification is approved, proof generation can proceed against that fixed goal. Lean's kernel checks the resulting proof rather than asking a person to read millions of proof lines^[1].

The project also checks that the proof establishes the intended held-out statement, not an easier substitute. Specification changes are separately reviewed and logged.

This is why the line count is not the security conclusion. Millions of lines indicate the scale of the proof development, but confidence depends on whether the statement is right and the checker accepted the proof of that exact statement.

A useful analogy for developers is a strict test expectation. Passing a test after silently weakening its assertion is not the same result. Formal proof needs a disciplined version of that boundary, with explicit statements and controlled changes.

The symbolic and computational results are different

The paper presents both symbolic and computational security proofs. They are not interchangeable labels for one guarantee.

In the symbolic model, cryptographic operations are idealized. The analysis can reason about protocol events and secrets under those abstractions. The paper describes ten symbolic theorems, including forward secrecy, post-compromise security, handshake authentication and handshake secrecy under specified compromise conditions^[2].

The computational model reasons about bit strings and a bounded probabilistic attacker. Its theorem gives a bound connecting an attack on the protocol to attacks on underlying cryptographic assumptions. The authors state important restrictions on that game and bound.

This means “it assumes perfect cryptography” is an incomplete summary of the whole paper. That phrase may describe an aspect of a symbolic argument, but the research also includes a computational theorem with its own assumptions and limits. A careful account should preserve both.

Post-quantum language needs a precise qualifier

The verified code includes the PQXDH handshake and Triple Ratchet. That does not mean every stated result gives a complete post-quantum guarantee for the entire messaging system.

The symbolic work includes handshake secrecy against an attacker that later breaks Diffie-Hellman, modeling an important quantum-related threat. The computational theorem covers classical attackers, not quantum attackers^[2].

The discussion section is also explicit that neither proof establishes SPQR's intended post-quantum healing property. That is listed as a direction for strengthening the work, not a result already delivered.

Keeping those distinctions does not make the research unimportant. It makes clear which assurance has been added and which questions remain. A broad “quantum-proof Signal” headline would erase that useful information.

The computational bound has practical limits

The computational section restricts the setting, including fixed message lengths, no multi-device state and particular conditions on attacker actions and session promotion. It also limits when some compromises are permitted^[2].

The authors say the statistical terms make the bound vacuous at some larger scales, especially when many messages begin new epochs. “Vacuous” here means the numerical bound stops providing a useful guarantee in that regime. It does not by itself demonstrate an exploit against Signal.

That distinction is easy to lose in a short summary. A proof limitation is a reason not to claim more than the theorem. It is not automatically evidence that the actual system is broken.

Conversely, a valid theorem in the bounded setting should not be advertised as a useful computational guarantee at any scale. The scope and numerical behavior belong beside the claim.

Expand ↗

Image viewer

Zoom to inspect. Scroll to pan.

−100%+

FitRotate×

Some routines remain behind trusted contracts

The paper does not prove every low-level cryptographic primitive from its machine-code implementation. Some calls are replaced by contracts expressing the behavior and security assumptions the rest of the proof uses.

Those contracts include cryptographic routines and several non-cryptographic routines. The trusted base also includes the semantics and definitions on which the theorem depends. The paper describes testing of the semantics against other execution models, but that testing does not make the trusted definitions disappear^[2].

A reviewer therefore has a smaller and more focused set of assumptions to inspect than the full generated proof development. Smaller is valuable, but it is not the same as zero.

For an engineering team reading a formal-verification claim, ask which parts are proved, which are modeled by contracts and which depend on external assumptions. A diagram that clearly shows those boundaries is more informative than a single “verified” badge.

Historical bugs help test the specification

The researchers reintroduced two previously fixed libsignal bugs and proved that the modified binaries violated their symbolic security theorems. That checks whether the specification can reject known wrong behavior rather than accepting every implementation^[1].

The project also uses checks aimed at vacuous specifications, such as establishing that assumptions can be jointly satisfied. These checks address a real failure mode: a theorem can be trivially true if its premises are impossible.

Neither technique proves the specification covers every relevant property. They are additional evidence that it catches meaningful failures and is not empty in an obvious way.

This is one of the most useful developer lessons in the paper. Test the strength of the specification, not only whether a proof can be found. A machine-checked answer to the wrong question remains the wrong assurance.

What the work does not verify

The stated scope excludes the whole mobile app and its surrounding user experience. The discussion names group messaging, sealed sender and server-side protocols as possible future expansions^[2].

The results also do not establish that a user's device is uncompromised, that a recipient will keep a message private or that every app feature has been formally verified. Those are different questions from the theorem's protocol and binary behavior.

Do not use the paper to recommend changing a personal security practice or to claim that one messenger is absolutely secure. Such a recommendation would require a threat model and evidence beyond the result explained here.

Outside reporting from Ars Technica likewise cautions that the work does not formally verify the entire Signal mobile app. That is useful context, not an independent rerun of the proofs^[3].

A practical way to read the next AI-verification claim

Start with the exact target: source version, compiled artifact and covered operations. Then read the theorem's property, attacker model and environment. Finally, identify the trusted definitions and exclusions.

Ask whether a proof was actually checked and whether the published materials let another expert inspect or rerun it. Keep that separate from the claim that a general-purpose AI model is reliable. Here, proof checking is the mechanism for rejecting invalid generated proofs.

For ordinary product development, combine the relevant assurance methods rather than declaring one a universal replacement for the others. Formal proofs, tests, review and deployment controls answer different questions.

The coding-model comparison looks at capability evidence for choosing tools. This result illustrates a different standard: generated work can be checked against an exact formal claim instead of judged only by how convincing it looks. The Genie explanation addresses the separate business problem of defining and limiting an ongoing agent job.

A substantial result with a deliberately stated boundary

AlphaProof Code demonstrates that AI-assisted formal verification can reach a large, existing cryptographic implementation at the machine-code level. The reported proof development is substantial, and the human-reviewed specification remains central.

Its value is clearest when the boundary stays visible: a particular executable, explicit properties, two different security models, trusted assumptions and stated exclusions.

That is a stronger explanation than either “Signal is now proven unhackable” or “it is only theory.” The paper adds specific assurance. Reading precisely tells us what that assurance is.

FAQ

Sources

1. 01Google DeepMind: AlphaProof Code research and HTML paper (opens in a new tab)
2. 02Research paper PDF: target, security models, trusted base and limitations (opens in a new tab)
3. 03Ars Technica: Signal's encryption and the scope of the AI-powered check (opens in a new tab)