Introduction
On November 10, Google DeepMind published AlphaProof Code research on compiled libsignal code, including forward secrecy and authentication. Agents help draft specifications and proofs; Lean checks the arguments against human-approved statements. Research paper
A formal check can ask whether a stated property holds across a modeled setting. Review the property, code and assumptions before interpreting that guarantee.
Which Signal code is covered
The target is one-to-one PQXDH setup and Triple Ratchet messaging, in unmodified libsignal crates wrapped in an AArch64 Linux command-line executable. This is a specific build, not all Signal applications. Verification setup
The result depends on specifications, machine-code semantics and contracts for routines represented by hooks. Cryptographic assumptions remain part of the argument. The paper also states limits, including side channels outside the attacker model and no guarantee against a quantum adversary in its computational bounds. The symbolic result separately covers handshake secrecy against a future quantum attacker. Trusted base and limitations
Those boundaries belong beside the result when it is discussed or reused. A proof statement about one binary does not automatically describe a differently linked build, its surrounding application or the device running it.
A correct proof can answer too small a question
Consider a fictional invoice calculator. We ask for a guarantee that its output is never negative. A function that always returns zero satisfies that condition for every input. It is still useless for calculating an invoice.
For an invented order with a $100 subtotal and $8 tax, outputs of $0, $100 and $108 all satisfy the nonnegative condition. Only $108 satisfies the separate rule that this example’s total equals subtotal plus tax, with no discounts, shipping or other adjustments.
The second rule is more useful, but it is still a narrow one. It does not specify a currency, rounding behavior or whether retrying a payment charges the customer twice. Each is another question to define and check. This is a conceptual arithmetic example, not a Lean proof, a payment implementation or a test of Google’s or Signal’s work.
For a product team, this makes specification review concrete. Before asking an AI system to prove a statement, give a reviewer examples of correct and unacceptable behavior. Then ask whether the proposed statement actually distinguishes them. If the zero-total calculator passes the statement, adding more proof effort to that statement cannot fix the missing requirement.
Carry a scope note with the artifact
We made a short, editable worksheet for reviewing a proposed verification claim. It separates the target artifact, the property, the input domain, assumptions and exclusions. Its invoice example is fictional; the blank fields are intended for a team’s own review.
Download the proof-scope worksheet
For a real project, we would use it to record:
- Which exact source revision, binary or build the claim names.
- The accepted behavior and an example that should violate it.
- Which inputs and operating conditions the statement covers.
- Which components or behaviors the argument assumes rather than establishes.
- What must be reviewed again when the artifact or specification changes.
This note should stay attached to the result. A dashboard label saying “verified” is difficult to assess after the statement, build and exclusions have been separated from it. Our worksheet is a writing and review aid; filling it in does not verify software.
What is available to inspect
The public repository provides proof developments, a paper-to-code map and build/check instructions. It pins Lean and Rust toolchains and documents additional prerequisites. Its optional comparator check replays headline theorems in a fresh Lean kernel and is supported on Linux. The repository also distinguishes its own license from third-party material, including libsignal. Repository and reproduction instructions
We inspected the published paper and repository instructions. We did not install the toolchain, rebuild the binary or replay the proofs, so this article does not independently reproduce the researchers’ verification. The repository is material to inspect and reproduce with the stated tools; this report does not establish a general-purpose service that can certify an arbitrary application.
A useful near-term application of the research is to choose one consequential rule in a small, well-defined component and make its scope explicit. That creates a reviewable target for verification work. The promise is stronger evidence about stated behavior, with enough context for the next person to know where it applies.
