Accountable Distribution of Machine-Checked Correctness Evidence

Abstract

Formal verification produces machine-checkable evidence, but consuming that evidence usually requires the original prover, dependency graph, source checkout, and substantial replay time. This paper studies a distinct cryptographic problem: how can a lightweight consumer obtain precise and accountable assurance about a deterministic proof replay with- out executing the verifier and without reducing the result to an opaque provider label? We define accountable replay attestation. A specialized operator performs an expensive replay once and publishes a structured observation through a signed append-only log. Con- sumers verify a signed tree head and logarithmic inclusion proof, pin history, and apply their own policy to the exact reported axiom-name sets for each theorem. The construction does not prove that the operator’s observation is true. It makes the claim immutable within a signed view, comparable across consumers, and attributable when incompatible signed views are compared. We instantiate the model as the Lean Transparency Log (LTL), using Lean 4 replay attestations and an RFC 9162 Merkle tree. We give explicit collision-extracting arguments for inclusion and consistency, lift them to scheme-level accountability games with a com- position theorem, and evaluate a live deployment over four production Ed25519 codebases and the verification path of SLH-DSA (FIPS 205), the hash-based post-quantum signa- ture standard. The public log contains nineteen leaves, including a Lean mechanization of the accumulator’s own security arguments (61 human-reviewed certificates with one project- specific uninterpreted SHA-256 boundary axiom) and, as its newest entry, eleven certificates over the SLH-DSA-SHA2-128s verifier. Since tree size 14 every signed head additionally carries a deterministic SLH-DSA co-signature — produced with the parameter set whose verification path the log itself attests. The mechanization effort also exposed, via differen- tial testing, a nontrivial model/implementation divergence — on malformed size claims, the deployed iterative consistency verifier was not extensionally equal to the recursive model proved in Lean (since closed; this paper reports the pre-closure measurements) — recorded explicitly in the corresponding log entry. The contribution is a cryptographic distribution model for machine-checked correctness evidence, with an end-to-end deployed instantiation that carries scoped proofs about its own accountability machinery.