proof-aware-crypto-tooling-agent/paper/ltl.tex

% Reconstructed directly from the 1344-line rejected ltl.tex and its PDF,
% using reinvention-outline.md and the live 13-leaf deployment as factual patch.
\documentclass[11pt]{article}
\usepackage[a4paper,margin=1.02in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,tabularx,array}
\usepackage{enumitem}
\usepackage{xcolor}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,fit,decorations.pathreplacing,calc}
\usepackage[colorlinks=true,linkcolor=blue!55!black,citecolor=blue!55!black,urlcolor=blue!55!black]{hyperref}
\hypersetup{pdftitle={Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log},pdfauthor={Olaf Horvath},pdfsubject={Transparency distribution of formal-verification replay evidence},pdfkeywords={formal verification, transparency log, Lean, Ed25519, Merkle tree, attestation}}
\lefthyphenmin=2 \righthyphenmin=3

\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\theoremstyle{remark}
\newtheorem{remark}{Remark}

\newcommand{\Hh}{\mathsf{H}}
\newcommand{\hleaf}{\mathsf{h}_{\rm leaf}}
\newcommand{\hnode}{\mathsf{h}_{\rm node}}
\newcommand{\MTH}{\mathsf{MTH}}
\newcommand{\Root}{\mathsf{Root}}
\newcommand{\Path}{\mathsf{Path}}
\newcommand{\ConsRec}{\mathsf{ConsRec}}
\newcommand{\Obs}{\mathsf{Obs}}
\newcommand{\Policy}{\mathsf{Policy}}
\newcommand{\Fp}{\mathbb{F}_{2^{255}-19}}
\newcommand{\code}[1]{\texttt{\detokenize{#1}}}

\definecolor{deepblue}{RGB}{43,61,112}
\definecolor{deepgreen}{RGB}{28,111,71}
\definecolor{softgray}{RGB}{245,247,249}

\lstset{basicstyle=\ttfamily\small,frame=single,rulecolor=\color{black!15},
backgroundcolor=\color{softgray},columns=fullflexible,keepspaces=true,
showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em}

\title{\textbf{Accountable Distribution of Machine-Checked Correctness Evidence}\\[3pt]
\large A Transparency Model and the Lean Transparency Log}
\author{Olaf Horvath\\
\small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805}
\date{July 2026 \quad (v0.5)}

\begin{document}
\maketitle

\begin{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 without executing the
verifier and without reducing the result to an opaque provider label?

We define \emph{accountable replay attestation}. A specialized operator performs
an expensive replay once and publishes a structured observation through a
signed append-only log. Consumers 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 an explicit composition theorem,
formalize the consumer pinning and policy boundaries, and evaluate a live
deployment over four production Ed25519 codebases. The public log contains thirteen leaves; its thirteenth
leaf attests a Lean mechanization of the accumulator's own security arguments
(222 inventoried environment constants, 61 human-reviewed assumption cones,
and a single uninterpreted SHA-256 axiom). The mechanization effort also exposed, via differential testing, a nontrivial
implementation boundary: the deployed iterative consistency verifier is not
extensionally equal to the recursive model on malformed size claims. The leaf records
this limitation explicitly. The resulting contribution is a cryptographic
distribution model for machine-checked correctness evidence, together with an
end-to-end deployed instantiation that carries scoped proofs about its own
accountability machinery.
\end{abstract}

\section{Introduction}\label{sec:intro}

Formal verification has made it possible to connect production cryptographic
software to machine-checked mathematics. Systems such as HACL*, EverCrypt,
Fiat-Crypto, and Aeneas demonstrate different routes from implementation to
proof~\cite{hacl,evercrypt,fiatcrypto,aeneas}. Yet the standard assurance story
quietly assumes a capable consumer: one that can retrieve the exact source,
reconstruct the verifier environment, resolve dependencies, and spend minutes
or hours replaying a corpus.

That assumption is often false. A package resolver selecting a cryptographic
backend, a deployment controller enforcing a proof requirement, or an
autonomous custody agent may have milliseconds and a small trusted computing
base, not a theorem prover and thirty minutes of kernel time per candidate.
This creates a problem that is logically downstream of proof construction:

\begin{quote}
\emph{How can a consumer that cannot execute the prover obtain precise,
accountable evidence about a proof replay, without collapsing the result into
an opaque provider verdict?}
\end{quote}

A detached signature on the word ``verified'' authenticates an issuer but does
not bind an ordered history, expose silent replacement, or give consumers a
compact state that can be pinned and required to grow. Shipping the complete
proof and checker preserves direct verification but may defeat the cost and
portability objective. Committees distribute trust but do not themselves fix
the semantics of the attested result. Succinct proofs of verifier execution
would provide validity rather than mere accountability, but require a circuit or
verified-VM representation of the prover and are not yet the deployment
assumption of the artifacts studied here.

We therefore study a narrower primitive: \emph{accountable delegation of
deterministic proof replay}. The operator still observes the replay. The
cryptographic layer does not make that observation true. Instead, it makes the
observation exact, persistent, attributable, and locally policy-checkable.
Independent replay remains the mechanism for challenging a fabricated
observation.

\paragraph{Central thesis.}
The contribution is not a new Merkle tree and not a new theorem prover. It is a
trust decomposition for distributing machine-checked correctness evidence:

\begin{center}
\fbox{\parbox{0.91\linewidth}{
\textbf{Expensive deterministic verification produces an observation.
Transparency makes that observation accountable. Consumer-local policy decides
whether the observation is acceptable.}}}
\end{center}

The Lean Transparency Log (LTL)\footnote{The acronym collides with linear
temporal logic~\cite{pnueli}; we note the collision once and rely on context.}
is the complete instantiation evaluated in this paper. Its subjects are four
Rust Ed25519 codebases with Lean~4~\cite{lean4} certificates against extracted
models. Its thirteenth public leaf attests the Lean corpus
that mechanizes the log's own accumulator arguments. Thus the paper's central
claim survives replacement of Lean, Ed25519, or RFC~9162 by other components;
what is essential is the distribution and accountability model.

\paragraph{Contributions.}
\begin{enumerate}[leftmargin=1.7em,itemsep=3pt]
\item \textbf{A distribution model for machine-checked evidence.}
We define replay attestations, distinguish observation from verdict, and state
what a lightweight consumer learns without executing Lean.
\item \textbf{A cryptographic accountability layer.}
Using the RFC~9162 tree unchanged, we define signed views, inclusion receipts,
local history pinning, and transferable same-size fork evidence. We give
explicit collision-extracting soundness arguments specialized to the consumer
algorithms, and lift them to scheme level: concrete games for position
binding, history binding, and fork evidence, discharged by explicit
reductions (\S\ref{sec:games}).
\item \textbf{Boundary-conformance policy.}
Each leaf records the exact axiom names reported by Lean. Consumers compare
those observations with their own policy; operator labels can veto but cannot
grant acceptance. We state clearly that axiom-name equality is not semantic
identity of theorem statements.
\item \textbf{A deployed cryptographic case study.}
The log contains twelve historical replay leaves for four verified Ed25519
codebases and a thirteenth leaf for the accumulator's own Lean corpus. The
entry-13 corpus carries an environment-derived audit inventory of 222 compiled
constants, 61 human-reviewed certificate cones, and a single uninterpreted
SHA-256 axiom.
\item \textbf{A negative deployment result.}
Differential testing found that the deployed iterative RFC-style consistency
verifier and the recursive model proved in Lean are not extensionally equal:
there are malformed size/root combinations accepted only by the deployed
verifier. We characterize 3,867 divergences in 73,573 pinned boundary tests
--- every one deployed-accepts-only --- and scope the public attestation
accordingly.
\end{enumerate}

\paragraph{Non-claims.}
LTL does not prove that the operator honestly reported a kernel run; independent
replay remains the way to detect a fabricated observation. It does not prove
binary correspondence, compiler correctness, extraction faithfulness,
side-channel resistance, SHA-512 correctness, or execution provenance of the
signing binary. The present leaf schema identifies theorem declarations by
repository commit and name, not by a canonical digest of their elaborated Lean
types. These are explicit boundaries, not hidden qualifications.

\section{The distribution problem}\label{sec:problem}

\subsection{Three evidence modes}

Let a subject repository at commit $g$ contain theorem declarations
$T_1,\dots,T_q$. A deterministic verifier execution produces an observation
$O_g$ containing success/failure and the reported assumption cone of each
$T_i$. There are three natural ways to consume this result.

\begin{description}[leftmargin=1.5em,itemsep=4pt]
\item[Direct replay.] The consumer reconstructs the verifier environment and
checks $O_g$ itself. This gives the strongest provenance, but has high
operational cost.
\item[Detached attestation.] A provider signs $O_g$. This is cheap to consume,
but provides no append-only history and no common value for clients to pin.
\item[Transparent attestation.] The provider signs a tree head committing
$O_g$ as one leaf among an ordered history. A consumer verifies inclusion and
persists a head. Incompatible views become attributable when compared.
\end{description}

The third mode is useful precisely when replay is expensive but the result is
stable and deterministic. It does not dominate direct replay: it replaces
local computation with a narrower trust in the replay provider.

\subsection{Why transparency rather than a signature database?}

Suppose an operator signs every replay result independently. Authenticity of
an individual record follows from signature verification, but four properties
are absent:
\begin{enumerate}[leftmargin=1.7em,itemsep=2pt]
\item no signed value commits to the ordered set of all records;
\item the signer commits to no complete ordered history, so omission or
replacement is not detectable by a fresh consumer and carries no compact
consistency proof;
\item two consumers cannot compare a single compact view identifier;
\item a consumer cannot demand that its previously accepted history only grow.
\end{enumerate}
An append-only Merkle tree supplies these missing interfaces. At the current
deployment size, logarithmic proof size is not the decisive benefit;
\emph{history binding} is.

\subsection{Design alternatives}

Table~\ref{tab:alternatives} places the construction among the natural
alternatives, read as a design taxonomy rather than an empirical comparison.
Local replay and proof transport keep semantic checking with the consumer at
high operational cost; detached signatures and committees lower consumer cost
but commit to no ordered history (a committee distributes trust in the
observation; it does not by itself make the record's history accountable);
succinct proofs of replay would upgrade accountability to validity at the
price of proving the prover. LTL occupies the low-consumer-cost point that
still binds an ordered, signed, pinnable history --- and deliberately does not
buy validity of the observation itself.

\begin{table}[t]
\centering\small
\begin{tabularx}{\textwidth}{@{}lXXXX@{}}
\toprule
Mechanism & Consumer cost & Semantic checker & History accountability & Main residual cost \\
\midrule
Local replay & high & consumer & local only & prover/toolchain deployment \\
Proof transport / PCC & medium--high & consumer checker & optional & proof/checker portability \\
Detached signed result & low & provider & statement-level only & replaceable history \\
Committee replay & low & committee & none without an additional log & membership trust \\
Succinct proof of replay & low & circuit/VM verifier & optional & proving the prover \\
LTL & low & provider observes; consumer applies policy & signed append-only views & observation honesty \\
\bottomrule
\end{tabularx}
\caption{Evidence-distribution alternatives. LTL targets low-cost consumers
while retaining an attributable history; it does not remove trust in the
replay observation.}
\label{tab:alternatives}
\end{table}

\section{Model and trust decomposition}\label{sec:model}

\subsection{Roles and objects}

The system has three logical roles.
\begin{description}[leftmargin=1.5em,itemsep=4pt]
\item[Subject maintainer.] Publishes source and proof artifacts at a commit.
\item[Replay operator.] Executes the declared verifier procedure, constructs
an attestation, appends it to the log, and signs tree heads.
\item[Consumer.] Holds the log public key and a local policy; verifies receipts
and optionally persists a previous head.
\end{description}

A replay attestation $a$ contains at least
\[
(\textsf{repo},g,\textsf{toolchain},\textsf{environment},
  [(N_i,s_i,A_i)]_{i=1}^{q}),
\]
where $N_i$ is a declaration name, $s_i$ is replay status, and $A_i$ is the
observed axiom-name set. The deployed schema additionally carries diagnostics,
resource controls, scope, and exclusions.

\begin{definition}[Attestation-transparency scheme]
An attestation-transparency scheme is a tuple
\[
\Pi=(\mathsf{KeyGen},\mathsf{Append},\mathsf{ProveIncl},
\mathsf{VerifyIncl},\mathsf{ProveCons},\mathsf{VerifyCons},\mathsf{Verdict})
\]
over a hash function and signature scheme. $\mathsf{Append}$ commits the
canonical serialization of an attestation as the next leaf and returns a signed
tree head. $\mathsf{Verdict}$ is parameterized by consumer-local policy and
does not consume an operator verdict as positive evidence.
\end{definition}

\begin{definition}[Accountable replay distribution]
Fix an operator public key and a consumer that persists accepted signed heads.
A replay-distribution scheme is \emph{accountable} if the following hold:
(i) every accepted attestation is position-bound to a signed view; (ii) a
consumer accepts a later view only as the same view or a verified extension;
(iii) two valid equal-size heads with unequal roots form transferable evidence
that the key holder signed incompatible views; and (iv) positive acceptance of
a theorem boundary is a function of recorded observations and consumer-local
policy, not of an operator verdict.
\end{definition}

The definition is intentionally an accountability property, not a validity
property. It says when conflicting claims become attributable; it does not
cryptographically prove that the replay observation was honestly produced.
Throughout, ``accountability'' means signed-view and history accountability;
observation validity remains external to the mechanism.
Section~\ref{sec:games} states clauses (i)--(iv) as games and explicit
reductions and proves the construction satisfies them.

\begin{figure}[t]
\centering
\begin{tikzpicture}[
  node distance=8mm and 8mm,
  b/.style={draw,rounded corners=2pt,align=center,minimum height=10mm,minimum width=29mm,font=\small},
  a/.style={-{Latex[length=2mm]},thick,draw=black!60}
]
\node[b,fill=blue!6] (subject) {subject source\\and proof corpus};
\node[b,fill=green!7,right=of subject] (replay) {expensive\\deterministic replay};
\node[b,fill=yellow!10,right=of replay] (att) {structured replay\\observation};
\node[b,fill=blue!6,right=of att] (log) {signed append-only\\view};
\node[b,fill=green!7,below=12mm of log] (consumer) {lightweight consumer\\signature + hashes + policy};
\draw[a] (subject)--(replay);
\draw[a] (replay)--(att);
\draw[a] (att)--(log);
\draw[a] (log)--(consumer);
\draw[a,dashed] (consumer.west) -| node[pos=.25,below,font=\scriptsize]{targeted independent replay} (replay.south);
\end{tikzpicture}
\caption{Trust decomposition. The log authenticates and orders the replay
operator's observation; it does not replace the theorem prover or make the
observation true.}
\label{fig:decomposition}
\end{figure}

\subsection{What is and is not transferred}

A verified receipt establishes a statement of the form:
\begin{quote}
The holder of public key $pk$ signed a tree head committing, at position $m$,
to a leaf in which the operator reports that the named declarations at commit
$g$ replayed with the recorded axiom-name sets.
\end{quote}
It does not establish that the operator's report is true. Nor does it identify
the semantics of a theorem from its name alone. This separation is central:

\begin{center}\small
\begin{tabular}{@{}ll@{}}
\toprule
Layer & What it contributes \\
\midrule
Lean kernel & validity of a checked term relative to declarations and axioms \\
Replay pipeline & binding of source, toolchain, theorem names, and observations \\
Attestation signature & attribution of one replay statement \\
Merkle log & position binding and append-only view commitments \\
Consumer policy & acceptability of the recorded boundary \\
Independent replay & detection of fabricated operator observations \\
\bottomrule
\end{tabular}
\end{center}

\subsection{Adversary model}

The network adversary may replay, delay, suppress, or substitute messages. The
operator may be malicious: it may construct arbitrary leaves, sign arbitrary
heads, label results arbitrarily, and present different signed views to
different consumers. We assume collision resistance of SHA-256 for the log,
EUF-CMA security of the head-signature scheme, and correct initial acquisition
of the operator public key.

The model deliberately does not cryptographically exclude fabricated kernel
observations. That is a statement about a physical execution on the operator's
machine. The mechanism instead makes the claimed execution target precise
enough for a third party to replay.

\subsection{Consumer goals}

Each goal below is formalized as a game in Section~\ref{sec:games}.

\begin{description}[leftmargin=1.5em,itemsep=5pt]
\item[G1: Position-bound membership.] If a consumer accepts leaf $d$ at index
$m$ against signed head $(n,r)$, then $d$ occupies position $m$ in a leaf list
committed by $r$, except under hash collision or signature forgery.
\item[G2: Local append-only history.] A consumer that persists $(n,r)$ accepts
a later view only if it is the same view or a verified extension. Two valid
heads of equal size and unequal roots are transferable evidence that the key
holder signed incompatible views. Unequal-size forks require retained
history, gossip, or a witness.
\item[G3: Policy separation.] The operator's positive label cannot make a
certificate acceptable. The consumer recomputes boundary conformance from
observations and local policy. Operator failure labels may be treated as a
conservative veto.
\end{description}

\subsection{Boundary conformance, not semantic identity}

For certificate $c$, let $\Obs_a(c)$ be the axiom-name set recorded in leaf
$a$, and let $\Policy(c)$ be the consumer's allowed set. Define
\[
\mathsf{boundary\_ok}_a(c) \iff \Obs_a(c)=\Policy(c).
\]
Exact equality detects both additional assumptions and drift in the declared
assurance interface. A missing expected axiom is not automatically a logical
defect: it may indicate a strengthened theorem, a changed statement, a bypassed
abstraction boundary, or stale policy. The consumer therefore rejects or
requires review rather than interpreting the drift.

This predicate is intentionally narrower than ``the intended theorem was
proved.'' The deployed system identifies a declaration by repository commit
and name. A stronger future schema should include canonical digests of the
elaborated theorem type and of the types of declarations in its axiom cone.

\section{Construction}\label{sec:construction}

\subsection{RFC 9162 tree}

Let $\Hh$ be SHA-256. For byte string $d$ and 32-byte values $x,y$ define
\[
\hleaf(d)=\Hh(\mathtt{0x00}\parallel d),\qquad
\hnode(x,y)=\Hh(\mathtt{0x01}\parallel x\parallel y).
\]
For leaf list $D=[d_0,\ldots,d_{n-1}]$:
\[
\MTH([])=\Hh(\epsilon),\qquad \MTH([d])=\hleaf(d),
\]
and for $n>1$,
\[
\MTH(D)=\hnode(\MTH(D[0{:}k]),\MTH(D[k{:}n])),
\]
where $k$ is the largest power of two strictly smaller than $n$. Inclusion and
consistency proofs are the RFC~9162 algorithms~\cite{ct2}.

\subsection{Signed tree heads}

A tree head contains schema-version and type tags, a log identifier, tree
size, root hash, timestamp, and hash-algorithm identifier. The canonical JSON serialization of
those fields is signed with Ed25519. The log identifier and version tag prevent
cross-log and cross-protocol replay.

The current implementation records signing-backend provenance alongside the
signature, but that provenance is not execution attestation: an Ed25519
signature does not identify the program that produced it. The public system
therefore treats the claimed signing implementation as operator-reported
context, not as a property proved by the signature.

\subsection{Receipts and pinning}

A receipt contains the leaf index, sibling path, and signed head. A consumer
first verifies the head signature and then reconstructs the root. For history,
a local pin $(n_{\rm pin},r_{\rm pin})$ evolves as follows:
\begin{itemize}[leftmargin=1.6em,itemsep=2pt]
\item same size: accept iff roots match; otherwise retain both signed heads as
same-size fork evidence;
\item larger size: accept iff a consistency proof verifies, then update;
\item smaller size: reject as rollback.
\end{itemize}
Freshness is an external availability policy. A persisted pin detects rollback
relative to local history; it does not prove that a client sees the globally
latest signed head.

\section{Security analysis}\label{sec:security}

This section states the consumer-facing arguments in the form used by the Lean
mechanization. The proofs are elementary but explicit: successful false
openings yield concrete SHA-256 collisions rather than appealing to an informal
``Merkle trees are secure'' statement. The explicitness is load-bearing: over a
fixed-width hash a bare ``some collision exists'' is vacuously true by
counting, so each soundness statement is about a named extractor function, and
the corpus pins a machine-checked non-vacuity guard for every extractor.

\subsection{Inclusion}

Let $\Root(v,m,n,P)$ recursively fold value $v$ at position $m$ through proof
path $P$ using the same largest-power-of-two decomposition as $\MTH$. Both
$\Root$ and $\ConsRec$ are partial (the mechanization's \code{Option}):
malformed shapes return a distinguished rejection value, and an equation such
as $\Root(\cdot)=\MTH(D)$ asserts acceptance with that output.

\begin{lemma}[Domain separation]
For all byte strings $d$ and 32-byte values $x,y$,
$\mathtt{0x00}\parallel d \neq \mathtt{0x01}\parallel x\parallel y$.
\end{lemma}
\begin{proof}
The first byte differs.
\end{proof}

\begin{theorem}[Inclusion completeness]
For every non-empty $D$, every $m<|D|$,
\[
\Root(\hleaf(D[m]),m,|D|,\Path(m,D))=\MTH(D).
\]
\end{theorem}
\begin{proof}
By structural induction on $|D|$. The singleton case is immediate. For a split
$D=L\|R$, the honest path is the recursive path inside the side containing $m$
followed by the other side's root. The induction hypothesis reconstructs the
selected child root, and the final node hash reconstructs $\MTH(D)$.
\end{proof}

\begin{theorem}[Inclusion soundness: position binding]
There is an explicit extractor $\mathcal{E}_{\rm incl}$ such that, given $D$,
$m<|D|$, $d\neq D[m]$, and a path $P$ satisfying
\[
\Root(\hleaf(d),m,|D|,P)=\MTH(D),
\]
$\mathcal{E}_{\rm incl}(D,m,d,P)$ returns two distinct SHA-256 preimages with
the same digest.
\end{theorem}
\begin{proof}
Recompute the honest tree and replay the accepting reconstruction from the root
downward. At each visited internal node, compare the adversarial and honest
node preimages. If they differ while their digests agree, output the collision.
Otherwise both child values agree and descent continues along the path. At the
terminal leaf, equality of digests with $d\neq D[m]$ yields a leaf-hash
collision. Domain separation rules out interpreting a leaf preimage as a node
preimage without already producing a collision.
\end{proof}

\subsection{Consistency}

The recursive verifier $\ConsRec(n_0,n_1,C,b,r_0)$ reconstructs an old and new
root from proof $C$, a flag $b$ indicating whether the old root is implicit,
and pinned value $r_0$. Malformed shapes return rejection.

\begin{theorem}[Consistency soundness of the recursive model]
There is an explicit extractor $\mathcal{E}_{\rm cons}$ such that, whenever
$|D_0|=n_0\le n_1=|D_1|$, $D_0\neq D_1[0{:}n_0]$, and
\[
\ConsRec(n_0,n_1,C,\top,\MTH(D_0))
   =(\MTH(D_0),\MTH(D_1)),
\]
$\mathcal{E}_{\rm cons}(D_0,D_1,C)$ returns a SHA-256 collision.
\end{theorem}
\begin{proof}
The new-root component is a hash fold over the shape of the $n_1$ tree. Compare
it with the honest $D_1$ tree. Either the first differing preimage gives a
collision, or every consumed proof node equals the corresponding honest node.
In the latter case, the old-root component is the canonical fold of the honest
prefix $D_1[0{:}n_0]$, so acceptance implies
$\MTH(D_0)=\MTH(D_1[0{:}n_0])$. The two equal-sized leaf lists differ; descend
through their identically shaped honest trees to extract the first hash
collision.
\end{proof}

The theorem's hypothesis pins the honest old root $\MTH(D_0)$. The deployed
flow has no mechanized supplier of that pin; the next subsection measures what
the iterative verifier does when size claims alone steer its walk.

\begin{proposition}[Pin-store safety]
Assume EUF-CMA security of the head signature and collision resistance of
SHA-256. A consumer following the pin transition accepts only a nondecreasing
sequence of sizes whose exhibited leaf lists are prefix-related. Two accepted
heads under the same key with equal size and unequal roots are transferable
evidence that the key holder signed incompatible views.
\end{proposition}
\begin{proof}
Rollback is rejected syntactically. At equal size the transition is accepted
only with equal roots; if the two exhibited equal-length leaf lists differed,
whole-tree binding would extract a SHA-256 collision, so under collision
resistance the lists are equal. A larger head is accepted only after a
consistency proof, so non-prefix acceptance yields a collision by the previous
theorem. Equal-size unequal roots with valid signatures are two conflicting
statements attributable to the key holder, except under signature forgery.
\end{proof}

\begin{proposition}[Policy separation]
For fixed local policy $\Policy$, the boundary-conformance result for every
certificate is a function only of $\Obs_a(c)$ and $\Policy(c)$. An operator
label cannot change a nonconforming observation into a conforming one.
\end{proposition}
\begin{proof}
The comparison is set equality and takes no positive operator verdict as input.
A deployment may conservatively treat an operator failure label as a veto, but
a veto cannot grant acceptance.
\end{proof}

\subsection{Scope of the deployed consistency claim}

The Lean theorem covers the recursive predicate above. The deployed iterative
verifier follows the familiar RFC bit-navigation algorithm. Differential
testing discovered that the two verifiers are not extensionally equal on
malformed size claims, every observed divergence being accepted only by the
iterative verifier: for example, a valid proof for a $2\to3$ transition can
be accepted under the false old-size claim $1\to3$ when paired with the size-2
root. The mechanism is elementary: the iterative algorithm seeds its
reconstruction with the supplied old root and consults the size claims only as
bit-navigation state, so several distinct old-size claims navigate one proof
identically. In 73,573 lied-size boundary cases, 3,867 divergences were
observed; all were one-sided (deployed accepts, recursive model rejects).

The intended consumer flow binds $(n_0,r_0)$ in local persistent state and
binds $(n_1,r_1)$ together in a signed head. The present corpus does not prove
a refinement theorem from that operational invariant to the recursive
predicate. Consequently the public attestation says exactly this: the model is
proved; deployment correspondence is finite-tested and relies on an
unmechanized authentic-size/root invariant.

\subsection{Scheme-level games and a composition theorem}\label{sec:games}

The theorems above bind single artifacts to a reference leaf list. This
subsection lifts them to the scheme: precise experiments for the accountability
clauses of Definition~2, and a theorem that the construction satisfies them.
Two modeling choices deserve emphasis. First, the replay operator \emph{is} the
adversary and legitimately holds the signing key, so the position-binding and
history games contain no secrets and no oracles; any adaptive interaction can
be replayed into a single output, and the games are therefore non-interactive
--- mirroring the deployment, in which receipt verification itself is
non-interactive. Signatures constrain a different party: the frame-resistance
game, in which a third party attempts to fabricate equivocation evidence
against a key holder who never equivocated. Second, SHA-256 is a fixed,
unkeyed function, so ``collision resistance'' cannot be a probability
statement over a key space; following the human-ignorance
treatment~\cite{rogaway}, every hash statement below is an \emph{explicit
reduction} --- a named algorithm transforming a winning transcript into a
concrete collision --- which is the scheme-level continuation of the corpus's
named-extractor discipline.

\paragraph{Accepted-artifact syntax.}
Fix the algorithms of Section~\ref{sec:construction}. A head $h=(n,r;\sigma)$
carries the canonical signed payload of \S4.2; $\mathsf{Vf}_{pk}(h)=1$ iff its
signature verifies. An \emph{opening} of leaf $d$ at index $m$ under $(n,r)$
is a path $P$ with $m<n$ and $\Root(\hleaf(d),m,n,P)=r$ (acceptance in the
Option sense of \S\ref{sec:security}); write $\mathsf{Open}(d,m,n,P,r)=1$. An
\emph{extension} from $(n_0,r_0)$ to $(n_1,r_1)$ is exactly a pin-rule
transition: either $n_0=n_1$ and $r_0=r_1$, or $n_0<n_1$ and
$\ConsRec(n_0,n_1,C,\top,r_0)=(r_0,r_1)$ for the supplied proof $C$; write
$\mathsf{Ext}(n_0,r_0,n_1,r_1,C)=1$.

\paragraph{Game $\mathsf{PB}$ (position binding).}
$\mathcal{A}$ outputs $(n,r,m,d,P,d',P')$ and wins iff $d\neq d'$ and
\[\mathsf{Open}(d,m,n,P,r)=\mathsf{Open}(d',m,n,P',r)=1.\]

\begin{theorem}[Scheme position binding]\label{thm:pb}
There is an explicit algorithm $\mathcal{B}_{\rm pb}$ that, whenever
$\mathcal{A}$ wins $\mathsf{PB}$, outputs two distinct byte strings with equal
SHA-256 digests, using at most the $2(\lceil\log_2 n\rceil{+}1)$ hash
evaluations of replaying the two openings.
\end{theorem}
\begin{proof}
Both accepting folds have the shape determined by $(m,n)$ and output the same
root $r$. Walk from the root downward along the path of $m$, maintaining that
the two transcripts agree on the current node's value. At an internal node the
transcripts present preimages $\mathtt{0x01}\|a\|b$ and
$\mathtt{0x01}\|a'\|b'$ with equal digests; since child values have fixed
32-byte width, the argument pairs are recoverable from the preimages, so
unequal pairs are a collision and equal pairs propagate agreement one level
down. If no disagreement occurs, the leaf presents $\mathtt{0x00}\|d$ and
$\mathtt{0x00}\|d'$ with equal digests and $d\neq d'$ --- a collision. Since
the shapes coincide, every comparison is leaf-to-leaf or node-to-node; domain
separation would in addition make any cross-type coincidence itself a
collision of distinct strings.
\end{proof}

\begin{lemma}[Prefix transport]\label{lem:transport}
Suppose $n_0<n_1$ and $m<n_0$, and that
\[\mathsf{Ext}(n_0,r_0,n_1,r_1,C)=1, \qquad \mathsf{Open}(d,m,n_1,P,r_1)=1.\]
There is an explicit algorithm
returning either a SHA-256 collision or a path $P_0$, assembled from the
values of $C$ and $P$, such that $\mathsf{Open}(d,m,n_0,P_0,r_0)=1$.
\end{lemma}
\begin{proof}[Proof sketch]
The accepted $\ConsRec$ transcript reconstructs $r_1$ as a fold over the
$n_1$-tree down to a frontier: the maximal perfect subtrees canonically
covering $[0,n_0)$ and the proof nodes covering $[n_0,n_1)$; its consumed
values are the entries of $C$ and, where the recursion bottoms out on the old
side, the pinned $r_0$ itself. Compare the opening's fold with this transcript
from the root down, as in Theorem~\ref{thm:pb}: either some shared node splits
into unequal recoverable argument pairs --- a collision --- or agreement
propagates until the path of $m$ enters the frontier subtree $T^*$ containing
$m$, at which point the opening's value at $T^*$ equals the transcript's value
$s^*$ there. Below $T^*$, the tail of $P$ is an accepting opening of $d$
within $T^*$ against $s^*$. Above $T^*$, the transcript's old-root component
folds the frontier values covering $[0,n_0)$ to $r_0$, and the siblings of
$T^*$ on the path to the root of the $n_0$-tree are all among the inputs and
intermediate values of that fold. Concatenating the tail of $P$ with those values yields
$P_0$; $\Root$ replays the same computation and outputs $r_0$. When $n_0$ is a
power of two, $T^*$ is the whole old tree, the spine is empty, and $P_0$ is
the tail of $P$ alone. Same-size extensions ($r_0=r_1$) transport identically.
\end{proof}

\paragraph{Game $\mathsf{HIST}$ (local history binding).}
$\mathcal{A}$ outputs a chain $h_0,\dots,h_k$ with transitions certified by
$\mathsf{Ext}$ for each consecutive pair --- precisely a state sequence a
consumer's pin can traverse; signature checks are omitted because the
adversary holds the key, so they constrain nothing --- together with indices
$a<b$, an index $m<n_a$, and openings with
$\mathsf{Open}(d,m,n_a,P,r_a)=\mathsf{Open}(d',m,n_b,P',r_b)=1$ and
$d\neq d'$. $\mathcal{A}$ wins iff everything verifies.

\begin{theorem}[History binding]\label{thm:hist}
There is an explicit algorithm $\mathcal{B}_{\rm hist}$ that, whenever
$\mathcal{A}$ wins $\mathsf{HIST}$, outputs a SHA-256 collision, using
$O(k\log n_k)$ hash evaluations.
\end{theorem}
\begin{proof}
Sizes along the chain are nondecreasing, so $m<n_a\le n_i$ for all $i\ge a$.
Apply Lemma~\ref{lem:transport} to the opening under $h_b$ and the transition
into $h_b$: either a collision, or an accepting opening of $d'$ at $m$ under
$h_{b-1}$. Iterating down to $h_a$ yields a collision or an accepting opening
of $d'$ at $m$ under $(n_a,r_a)$; together with the given opening of
$d\neq d'$ there, Theorem~\ref{thm:pb} extracts the collision.
\end{proof}

\paragraph{Game $\mathsf{FORK}$ (fork evidence).}
Define the evidence predicate $\mathsf{Ev}(h,h')=1$ iff
$\mathsf{Vf}_{pk}(h)=\mathsf{Vf}_{pk}(h')=1$, the tree sizes are equal, and
the roots differ. \emph{Completeness} is by construction: if the key holder
signs two equal-size heads with unequal roots, the pair itself satisfies
$\mathsf{Ev}$ --- producing the evidence requires retention and comparison,
not cooperation. \emph{Frame resistance} is a game: a challenger runs
$\mathsf{KeyGen}$ and signs, on the operator's behalf, the canonical payloads
the operator actually issues (query set $Q$); the adversary, without the key,
outputs $(h,h')$ and wins iff $\mathsf{Ev}(h,h')=1$ and at least one of the
two canonical payloads is not in $Q$. (If both payloads are in $Q$, the key
holder really did sign two equal-size heads with unequal roots --- the
evidence is genuine, not a frame.)

\begin{theorem}[Frame resistance]\label{thm:fork}
For every $\mathcal{A}$ there is an explicit $\mathcal{B}_{\rm fr}$ with
$\mathbf{Adv}^{\mathsf{FORK}}(\mathcal{A})\le
\mathbf{Adv}^{\text{euf-cma}}(\mathcal{B}_{\rm fr})$.
\end{theorem}
\begin{proof}
A winning pair contains a head whose canonical payload was never queried to
the signing oracle; its valid signature is an existential forgery, which
$\mathcal{B}_{\rm fr}$ outputs. (Payloads are injective on $(n,r)$ by the
canonical serialization of \S4.2, so distinct claimed views cannot collapse
to one queried message.)
\end{proof}

\begin{lemma}[Policy separation]\label{lem:policy}
For every leaf $a$ and certificate $c$, the verdict computed by
$\mathsf{Verdict}$ equals $[\Obs_a(c)=\Policy(c)]$; it reads no operator
label, and acceptance consults the operator's status only as a veto. This is a
deterministic property of the $\mathsf{Verdict}$ algorithm, by construction
(\S\ref{sec:model}); it is not a hardness statement.
\end{lemma}

\begin{definition}[Accountable replay distribution, formal]\label{def:formal}
A scheme is \emph{accountable} if explicit reductions
$\mathcal{B}_{\rm pb},\mathcal{B}_{\rm hist}$ as above exist, fork evidence is
complete with frame resistance bounded by EUF-CMA, and $\mathsf{Verdict}$
satisfies policy separation. This formalizes clauses (i)--(iv) of
Definition~2: $\mathsf{PB}$ gives position binding, $\mathsf{HIST}$ the local
append-only history, $\mathsf{FORK}$ transferable same-size evidence, and
Lemma~\ref{lem:policy} policy separation.
\end{definition}

\begin{theorem}[Accountability of the construction]\label{thm:main}
The LTL construction --- the RFC~9162 tree, the canonical signed heads of
\S4.2, the pin rule of \S4.3, and the policy verdict of \S\ref{sec:model} ---
is an accountable replay-distribution scheme, with
$\mathcal{B}_{\rm pb}$, $\mathcal{B}_{\rm hist}$, and $\mathcal{B}_{\rm fr}$
the explicit algorithms of Theorems~\ref{thm:pb}--\ref{thm:fork}.
\end{theorem}

\begin{remark}[What is mechanized, what is not]\label{rem:gamescope}
The games are stated for the scheme's specified verifiers --- the recursive
model whose honest-reference specializations are kernel-checked in entry~13
(the named extractors and per-step pin safety). The two-transcript comparisons
of Theorems~\ref{thm:pb} and~\ref{thm:hist} and the prefix-transport lemma are
paper-level proofs in the same discipline, not part of the mechanized corpus;
Game~$\mathsf{HIST}$ supplies, at paper level, the multi-step closure that the
corpus leaves external. Applying any of these statements to the deployed
iterative verifier inherits the refinement boundary of the previous subsection
unchanged.
\end{remark}

\section{Lean and Ed25519 instantiation}\label{sec:instantiation}

\subsection{Proof corpus}

The initial subjects are upstream \code{curve25519-dalek}/\code{ed25519-dalek}
(one implementation: the curve crate and the signature crate atop it) and
three deployed forks: Solana/Anza, RISC~Zero, and Betrusted --- all
implementations of Ed25519~\cite{eddsa,rfc8032}. Aeneas
provides a functional translation route from Rust to theorem-prover models;
its design uses Rust ownership information to avoid explicit memory reasoning
for a large class of safe Rust programs~\cite{aeneas}. A recent independent
experience report likewise applies a Rust-to-Lean pipeline to cryptographic
code~\cite{klaus2026}.

Each fork's corpus contains sixteen reviewed certificates covering:
\begin{itemize}[leftmargin=1.6em,itemsep=2pt]
\item five-limb field arithmetic over $\Fp$ with value and bound preservation;
\item complete twisted-Edwards group operations~\cite{edwards,twisted};
\item scalar arithmetic modulo the Ed25519 group order;
\item encoding, decoding, and constructive point decompression;
\item a four-stage lifting ladder from byte-level verifier acceptance to a
mathematical point equation.
\end{itemize}

The signature apex can be summarized as follows. Let $k$ be the challenge
scalar produced by an opaque SHA-512 boundary and let $r_1$ be the raw $R$ bytes
from the signature. The corpus separates:
\begin{description}[leftmargin=1.5em,itemsep=2pt]
\item[T1:] acceptance iff the verifier's recomputed compressed bytes equal
$r_1$;
\item[T2:] those recomputed bytes are the canonical encoding of
$[k](-A)+[s]B$;
\item[T3:] canonical encoding is injective on valid curve points;
\item[T4:] acceptance iff constructive decompression of $R$ yields
$[k](-A)+[s]B$.
\end{description}

The separation keeps residual assumptions visible. SHA-512 and selected
wire-format interfaces are opaque boundaries at the apex; lower arithmetic and
group certificates use the foundational Lean axioms observed in the corpus.

\subsection{Replay attestation}

For every certificate the operator records:
\begin{lstlisting}
name
status
observed_axioms
expected_axioms          # audit trail; consumer policy is local
axiom_status
diagnostics
\end{lstlisting}
The attestation also records repository URL and commit, Lean and Lake versions,
replay diagnostics, and resource controls. Missing cones are
\code{unverifiable}; they are never interpreted as empty.

\subsection{Operational self-reference}

The service reports that tree heads are generated using a binary built from the
same Ed25519 source family whose verification-path certificates appear in the
log. Before signing, the operator recomputes inclusion of the newest signing-
library leaf in the tree. This is useful operational coherence, but not proof
of execution provenance. The signature authenticates the tree-head payload; it
does not reveal the program that produced it. Reproducible builds or execution
attestation would be required to establish that stronger claim.

\section{Deployment and evaluation}\label{sec:deployment}

The evaluation asks four questions: (E1) can substantial proof-replay evidence
be consumed without deploying Lean; (E2) does the public history retain failed
and superseded observations rather than silently replacing them; (E3) can the
accumulator's own arguments be placed under the same attestation discipline;
and (E4) does mechanization expose mismatches between the proved model and the
deployed verifier?

\subsection{Public state}

As of 16 July 2026, the public log contains thirteen leaves and current root
\begin{center}
\path{3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d}.
\end{center}
Every signed head issued since public mirroring began is retained --- six
heads, at tree sizes 8 through 13 --- together with every leaf and receipt, in
an append-only Git mirror; a clone re-verifies the entire log offline with the
repository's standalone verifier.
The first twelve leaves are three four-fork replay generations. Leaves 0--3
record a failed audit run and remain permanently visible. Leaves 4--7 record a
clean replay. Leaves 8--11 re-attest rewritten repository histories rather
than replacing the old leaves. A leaf whose pinned commit ceases to be
distributed decays from a replayable claim to a historical record; consumers
act only on attestations whose subjects they can retrieve.

Leaf 12 (the thirteenth entry) attests the accumulator corpus at commit
\begin{center}\small\ttfamily
172a1d0653f489d5b7cb73ac7942a57cbb496532
\end{center}
It records 61/61 reviewed
certificates as proven with exact expected/observed cones. The corpus audit
also inventories 222 compiled environment constants and permits exactly one
boundary axiom, \code{LTLAcc.sha256}.

\begin{figure}[t]
\centering
\begin{tikzpicture}[
  >=Latex,
  box/.style={draw,rounded corners=2pt,minimum width=1.03cm,minimum height=.52cm,font=\scriptsize,align=center},
  fail/.style={box,fill=black!6,draw=black!45,text=black!60},
  ok/.style={box,fill=green!7!white,draw=deepgreen,text=deepgreen!80!black},
  acc/.style={box,fill=blue!7!white,draw=deepblue,text=deepblue},
  arrow/.style={->,draw=black!55}
]
\foreach \i in {0,...,3} {\node[fail] (l\i) at (1.08*\i,0) {\i\\failed};}
\foreach \i in {4,...,7} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
\foreach \i in {8,...,11} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
\node[acc,minimum width=1.3cm] (l12) at (1.08*12,0) {12\\accumulator};
\draw[decorate,decoration={brace,mirror,raise=5pt},black!45]
  ($(l0.south west)+(-.05,0)$)--($(l3.south east)+(.05,0)$)
  node[midway,below=11pt,font=\scriptsize]{run 1};
\draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
  ($(l4.south west)+(-.05,0)$)--($(l7.south east)+(.05,0)$)
  node[midway,below=11pt,font=\scriptsize]{run 2};
\draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
  ($(l8.south west)+(-.05,0)$)--($(l11.south east)+(.05,0)$)
  node[midway,below=11pt,font=\scriptsize]{run 3};
\node[draw,rounded corners,fill=softgray,minimum width=4.3cm,minimum height=.7cm,font=\small] (sth) at (6.7,1.65)
  {signed head: size 13, root \code{3488a2d0...}};
\draw[arrow] (l12.north) -- (sth.south east);
\draw[arrow] (l6.north) -- (sth.south west);
\end{tikzpicture}
\caption{The public 13-leaf deployment. Failure leaves are retained; entry 13
attests the accumulator corpus itself, scoped to the recursive model.}
\label{fig:deployment}
\end{figure}

\subsection{Mechanization coverage}

Entry 13 is not a claim that the whole service is formally verified. The Lean
corpus covers the recursive Merkle model, inclusion completeness and
collision-extracting soundness, the consistency extractor, and the Merkle-layer
share of pin-store safety. The abstract root-binding lemma from the paper is
mechanized through the specializations needed by the extractors rather than as
one quantified hash-fold theorem. Signature unforgeability, execution
provenance, the full signed-head state machine, asymptotic cost, and the
refinement from the deployed iterative consistency verifier remain outside the
corpus.

\begin{center}\small
\begin{tabularx}{\textwidth}{@{}lXX@{}}
\toprule
Layer & Mechanized evidence & Explicit boundary \\
\midrule
Merkle definitions & MTH, Root, Path, recursive ConsRec & single SHA-256 boundary axiom \\
Inclusion & completeness and named collision extractor & collision resistance interpreted externally \\
Consistency & recursive-model soundness and extractor & no general consistency-completeness theorem \\
Pinning & per-step monotonicity and prefix correctness & signature layer and multi-step closure external \\
Deployment refinement & finite differential harness & no theorem for iterative verifier under authentic-pair invariant \\
Policy separation & deterministic tooling logic and regression tests & not mechanized in the entry-13 corpus \\
Scheme-level games (\S\ref{sec:games}) & paper-level explicit reductions & two-transcript comparisons and prefix transport not mechanized \\
\bottomrule
\end{tabularx}
\end{center}

\subsection{Cost and reproducibility}

A replay of one Ed25519 fork requires approximately 30 minutes of end-to-end
guarded replay time under the pinned environment, a figure corroborated by the
inter-leaf issuance spacing visible in the published log. Receipt verification requires one Ed25519
signature and a logarithmic number of SHA-256 node computations. The
accumulator corpus is independently reviewable with a pinned public Lean
release; an environment-derived inventory fails closed on added, removed, or
axiom-smuggling declarations.

The fidelity harness compares the Lean-definition transliteration with the
deployed Python algorithms over pinned finite families:
\begin{center}\small
\begin{tabular}{@{}lrrl@{}}
\toprule
Family & Cases & Divergences & Interpretation \\
\midrule
Inclusion & 230,271 & 0 & baseline and out-of-range families \\
Consistency baseline & 230,016 & 0 & honest and mutation families \\
Lied-size consistency & 73,573 & 3,867 & all deployed-accepts-only \\
\bottomrule
\end{tabular}
\end{center}
Finite testing is not a proof of extensional equality. Here it served a more
valuable purpose: it falsified an overbroad equivalence claim and supplied a
stable regression boundary.

\begin{remark}[Model/deployment seam]
For malformed size claims, the deployed iterative verifier and the recursive
model are not extensionally equal. In all 3,867 divergences observed across
the pinned families the deployed verifier accepted and the model rejected; the
reverse direction was not observed, and no global inclusion relation between
the two acceptance sets is claimed.
The public attestation therefore scopes soundness to the recursive model and
states the additional operational assumption: roots and sizes must be bound by
the authenticated pin-store and signed-head flow. This invariant is not
mechanized in the present corpus.
\end{remark}

\subsection{Consumer prototypes and version exactness}

The implemented internal consumer is a quorum-custody signing prototype: its
inbound boundary accepts a log-derived statement only when independently
attested verifier backends agree, and its policy consumes recorded
observations, never operator labels. Separately, an informal check found a
production codebase whose vendored Ed25519 dependency matches an attested
subject at family level but not at the attested version; the model treats a
family-level match as conferring nothing, because attestations are
version-exact by construction. Neither observation is an evaluation claim;
both indicate how the policy boundary is consumed in practice.

\subsection{Proof portability across forks}

Pure mathematical lemmas are largely reusable, while extraction-facing scripts
diverge where code structure and generated names diverge. In the deployed
corpora, the RISC~Zero and Betrusted signature-layer proof files differ by 27
changed lines (tracking one fork's optimization barrier and the forks'
differing operation order), other extraction-facing files differ by tens to
hundreds of lines, and pure carry and field lemmas remain byte-identical. This supports a practical conclusion: verification is portable
above the representation boundary and target-specific where implementation
structure actually differs.

\section{Related work}\label{sec:related}

\paragraph{Transparency.}
Certificate Transparency introduced publicly auditable append-only logs for
certificate issuance~\cite{ct1,ct2}; Crosby and Wallach developed efficient
tamper-evident history trees~\cite{crosby}; Dowling et al. formalized security
notions for secure logging and CT~\cite{dghs} --- the games of
\S\ref{sec:games} adapt that two-transcript style to replay attestation, with
the operator as first-class adversary and policy separation as a deterministic
functionality. CONIKS applies transparency to
key directories~\cite{coniks}. LTL reuses the authenticated data structure but
changes the payload and trust semantics: a leaf is an observation of a proof
replay, not an issuance event or key binding.

\paragraph{Software supply-chain attestations.}
In-toto expresses supply-chain steps and link metadata~\cite{intoto}. Sigstore
combines ephemeral signing, identity, and transparency to reduce software-
signing adoption barriers~\cite{sigstore}. LTL is complementary: it concerns
what a theorem prover reportedly accepted and which assumptions remained, not
who built or signed a binary. A complete assurance chain should eventually
combine both.

\paragraph{Proof transport and verified cryptography.}
Proof-carrying code ships a proof to a consumer-side checker~\cite{pcc}. LTL
serves consumers that cannot deploy that checker and therefore accepts a
different trust trade. HACL*, EverCrypt, and Fiat-Crypto demonstrate verified
cryptographic implementation pipelines~\cite{hacl,evercrypt,fiatcrypto};
Computer-aided frameworks such as EasyCrypt address scheme-level security
proofs~\cite{easycrypt}; Aeneas targets functional verification of Rust
through translation~\cite{aeneas}.
LTL does not compete with those systems: it distributes accountable statements
about their replay.

\paragraph{Verification of transparency protocols.}
Cheval et al. mechanize transparency-protocol reasoning~\cite{cheval}.
The entry-13 corpus approaches the composition from the opposite direction: it
mechanizes accumulator arguments and then logs that replay result. The
remaining refinement from the deployed state machine to the recursive model is
explicitly open.

\section{Limitations and research agenda}\label{sec:limitations}

The subject corpus maintains a numbered ledger of fifteen known gaps together
with their closure options; this section groups the load-bearing ones.

\paragraph{Operator observation trust.}
A malicious operator can fabricate a replay report. Signatures and Merkle
proofs make the lie attributable and persistent; they do not make it true.
Targeted independent replay is the corrective mechanism.

\paragraph{Theorem identity.}
Names and repository commits are not canonical semantic identifiers, and
commit identifiers are SHA-1-based --- a weaker binding than the log's own
SHA-256 tree. A future
schema should commit to elaborated theorem-type digests, axiom declaration-type
digests, and an environment or replay-manifest digest.

\paragraph{Source-to-binary gap.}
The evidence concerns source models at pinned commits. Reproducible builds,
compiler validation, binary measurement, and side-channel evidence are outside
the present result.

\paragraph{Witnessing and key distribution.}
The deployment has one operator and trust-on-first-use key distribution. A Git
mirror gives retaining observers a common public view, but does not force all
isolated clients to receive that view. Independent witnesses or gossip are the
natural next deployment step.

\paragraph{Consistency refinement.}
The recursive model is proved; the iterative deployment diverges from it on
malformed inputs, every observed divergence being deployed-accepts-only. The strongest closure is either to deploy
$\ConsRec$-equivalent semantics or to mechanize the signed-head and pin-store
flow and prove the authentic-pair refinement theorem.

\paragraph{Signed provenance.}
Signing-backend metadata is operator-provided context and should be committed
inside the signed tree-head payload. Even then it would remain an assertion,
not execution proof.

\paragraph{From accountable replay to cryptographic proof of replay.}
A longer-term direction is a succinct proof that a fixed proof-checker binary
accepted a fixed corpus. Such a system could reduce operator-observation trust,
but would introduce a new verified-execution stack. LTL supplies an
intermediate accountability layer and a public corpus against which that future
system can be evaluated.

\section{Conclusion}

Formal verification solves the production of correctness evidence; it does not
by itself solve distribution to consumers that cannot execute the verifier.
This paper isolates that second problem and gives a cryptographic answer based
on accountable replay attestation. The operator's observation remains trusted,
but its content is structured, its history is signed and append-only, its
assumption boundary is subject to consumer-local policy, and incompatible views
become attributable when compared.

The Lean Transparency Log demonstrates the complete construction. It amortizes
expensive replay over lightweight consumers, retains failed and superseded
observations, and carries a scoped attestation of the accumulator's own Lean
corpus as entry 13. Just as importantly, the mechanization and differential
harness exposed a mismatch between the recursive model and the deployed
consistency verifier. Recording that mismatch in the public leaf is not a
failure of the method; it is evidence that the trust decomposition is doing
useful scientific work.

The next step is not to claim trustlessness. It is to close specific boundaries:
canonical theorem-type commitments, reproducible source-to-binary linkage,
independent witnesses, signed provenance commitments, and a proved refinement
between the deployed signed-head flow and the recursive model. Accountable
replay attestation provides an immediate infrastructure layer while those
stronger validity mechanisms are developed.

\section*{Artifact availability}
The live service is \url{https://ltl.zkdefi.org}. Entry 13 has leaf hash
\begin{center}\small\ttfamily
8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a
\end{center}
and is included in the size-13 head with root
\begin{center}\small\ttfamily
3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d
\end{center}
The public artifacts are available at:
\begin{itemize}[leftmargin=1.5em,itemsep=1pt]
\item append-only mirror: \href{https://github.com/saymrwulf/lean-transparency-log}{\texttt{saymrwulf/lean-transparency-log}};
\item accumulator mechanization: \href{https://github.com/saymrwulf/ltl-accumulator-verified}{\texttt{saymrwulf/ltl-accumulator-verified}};
\item provider and consumer tooling: \href{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}{\texttt{saymrwulf/proof-aware-crypto-tooling-agent}}.
\end{itemize}
A clone of the mirror re-verifies every numbered leaf, every published signed
head, and every published receipt offline via \code{python3 verify.py --all}
(Python standard library plus an \code{openssl} binary; the verifier fails
closed if signature checking is unavailable, and its adversarial self-test
ships beside it).

\section*{Acknowledgments}
The author designed the system and is responsible for every claim. Claude
(Anthropic) and GPT (OpenAI) were used as critical assistants in proof-corpus,
tooling, and manuscript review. Their output was not accepted as evidence;
claims were retained only after human review or reproducible artifact checks.

\begin{thebibliography}{22}
\itemsep2pt
\bibitem{ct1} B. Laurie, A. Langley, E. K\"asper. Certificate Transparency.
RFC 6962, 2013.

\bibitem{ct2} B. Laurie, E. Messeri, R. Stradling. Certificate Transparency
Version 2.0. RFC 9162, 2021.

\bibitem{crosby} S. A. Crosby, D. S. Wallach. Efficient Data Structures for
Tamper-Evident Logging. USENIX Security, pp. 317--334, 2009.

\bibitem{dghs} B. Dowling, F. G\"unther, U. Herath, D. Stebila. Secure
Logging Schemes and Certificate Transparency. ESORICS, LNCS 9879, pp.
140--158, 2016.

\bibitem{sigstore} Z. Newman, J. S. Meyers, S. Torres-Arias. Sigstore:
Software Signing for Everybody. ACM CCS, pp. 2353--2367, 2022.

\bibitem{intoto} S. Torres-Arias, H. Afzali, T. K. Kuppusamy, R. Curtmola,
J. Cappos. in-toto: Providing farm-to-table guarantees for bits and bytes.
USENIX Security, pp. 1393--1410, 2019.

\bibitem{coniks} M. S. Melara, A. Blankstein, J. Bonneau, E. W. Felten,
M. J. Freedman. CONIKS: Bringing Key Transparency to End Users. USENIX
Security, pp. 383--398, 2015.

\bibitem{pcc} G. C. Necula. Proof-Carrying Code. ACM POPL, pp. 106--119,
1997.

\bibitem{cheval} V. Cheval, J. Moreira, M. Ryan. Automatic verification of
transparency protocols. IEEE EuroS\&P, pp. 107--121, 2023.
doi:10.1109/EuroSP57164.2023.00016. arXiv:2303.04500.

\bibitem{easycrypt} G. Barthe, B. Gr\'egoire, S. Heraud, S. Zanella
B\'eguelin. Computer-Aided Security Proofs for the Working Cryptographer.
CRYPTO, LNCS 6841, pp. 71--90, 2011.

\bibitem{aeneas} S. Ho, J. Protzenko. Aeneas: Rust verification by
functional translation. Proc. ACM Program. Lang. 6 (ICFP): 711--741, 2022.

\bibitem{lean4} L. de Moura, S. Ullrich. The Lean 4 Theorem Prover and
Programming Language. CADE-28, LNCS 12699, pp. 625--635, 2021.

\bibitem{hacl} J.-K. Zinzindohou\'e, K. Bhargavan, J. Protzenko,
B. Beurdouche. HACL*: A Verified Modern Cryptographic Library. ACM CCS,
pp. 1789--1806, 2017.

\bibitem{evercrypt} J. Protzenko et al. EverCrypt: A Fast, Verified,
Cross-Platform Cryptographic Provider. IEEE S\&P, pp. 983--1002, 2020.

\bibitem{fiatcrypto} A. Erbsen, J. Philipoom, J. Gross, R. Sloan,
A. Chlipala. Simple High-Level Code for Cryptographic Arithmetic---With
Proofs, Without Compromises. IEEE S\&P, pp. 1202--1219, 2019.

\bibitem{eddsa} D. J. Bernstein, N. Duif, T. Lange, P. Schwabe, B.-Y. Yang.
High-speed high-security signatures. J. Cryptographic Engineering 2(2):
77--89, 2012.

\bibitem{rfc8032} S. Josefsson, I. Liusvaara. Edwards-Curve Digital
Signature Algorithm (EdDSA). RFC 8032, 2017.

\bibitem{edwards} D. J. Bernstein, T. Lange. Faster addition and doubling on
elliptic curves. ASIACRYPT, LNCS 4833, pp. 29--50, 2007.

\bibitem{twisted} D. J. Bernstein, P. Birkner, M. Joye, T. Lange,
C. Peters. Twisted Edwards curves. AFRICACRYPT, LNCS 5023, pp. 389--405,
2008.

\bibitem{pnueli} A. Pnueli. The temporal logic of programs. IEEE FOCS, pp.
46--57, 1977.


\bibitem{rogaway} P. Rogaway. Formalizing Human Ignorance:
Collision-Resistant Hashing without the Keys. VIETCRYPT, LNCS 4341, pp.
211--228, 2006.

\bibitem{klaus2026} N. Klaus, J. Conejero, P. Tolmach. A Rust-to-Lean
Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
2026.

\end{thebibliography}

\appendix

\section{End-to-end claim matrix}\label{app:matrix}
\begin{center}\small
\begin{tabularx}{\textwidth}{@{}XXX@{}}
\toprule
Consumer conclusion & Established by & Remaining assumption \\
\midrule
Leaf occupies index $m$ under head $h$ & inclusion proof and signed head & SHA-256 collision resistance; correct public key; EUF-CMA of the head signature \\
Head was authorized by the log identity & Ed25519 verification & correct key acquisition; EUF-CMA \\
New pinned head extends old pinned head & consistency proof & SHA-256 collision resistance; recursive-model soundness; authentic size/root pairing for deployment \\
Equal-size unequal roots conflict & two valid signatures & correct public key; EUF-CMA; operationally, a retaining observer must compare the heads \\
Observed cone matches local boundary policy & exact set equality & semantic identity of named declarations \\
Operator claims the kernel produced the observation & attestation signature and leaf inclusion & correct provider key; EUF-CMA \\
Kernel actually produced the recorded observation & not cryptographically established; independently checkable by replay & operator and replay-pipeline honesty, or faithful independent replay \\
Source corresponds to deployed binary & not established & reproducible build and compiler assurance \\
Claimed signer implementation produced STH & not established & execution provenance \\
\bottomrule
\end{tabularx}
\end{center}

\section{Deployed entry-13 scope}\label{app:entry13}
The thirteenth public leaf contains the following deployment constraint,
quoted verbatim, in its machine-readable scope block:
\begin{quote}\small
Attestation scope: this corpus kernel-checks the listed theorems about the
mechanized recursive accumulator model. Correspondence with the deployed
inclusion verifier is supported by finite differential testing over the pinned
families. The deployed consistency verifier is not extensionally equal to the
model; applying the mechanized soundness result to the deployed consumer flow
additionally relies on an unmechanized authentic-size/root invariant
(KNOWN-GAPS 14/15).
\end{quote}
Its exclusions name SHA-256 collision resistance, deployed-verifier extensional
equality, the signature/STH layer, and asymptotic cost claims.

\section{Compact receipt-verification core}\label{app:verifier}
The following code is only the Merkle inclusion core. A complete receipt
verifier must additionally validate the signed tree head, log identifier,
tree-size binding, public-key fingerprint or pinned key, leaf hash, and receipt
schema. The published log-repository verifier implements that full binding
list for every published receipt --- the binding fields are required, never
compare-if-present --- and fails closed when signature checking is
unavailable.
\begin{lstlisting}[language=Python]
import hashlib

def H(data):
    return hashlib.sha256(data).digest()

def h_leaf(data):
    return H(b"\x00" + data)

def h_node(left, right):
    return H(b"\x01" + left + right)

def split_below(n):
    return 1 << ((n - 1).bit_length() - 1)

def take(path, used):
    if used >= len(path):
        raise ValueError("proof exhausted")
    return path[used]

def root(value, index, size, path, used=0):
    if size == 1:
        return value, used
    k = split_below(size)
    if index < k:
        left, used = root(value, index, k, path, used)
        return h_node(left, take(path, used)), used + 1
    right, used = root(value, index-k, size-k, path, used)
    return h_node(take(path, used), right), used + 1

def verify_inclusion(leaf, index, size, path, expected_root):
    if size <= 0 or index < 0 or index >= size:
        return False
    try:
        result, used = root(h_leaf(leaf), index, size, path)
    except ValueError:
        return False
    return used == len(path) and result == expected_root
\end{lstlisting}

\section{Four Ed25519 verification tiers}\label{app:tiers}
\begin{center}\small
\begin{tabular}{@{}lll@{}}
\toprule
Tier & Meaning & Upstream Lean declaration \\
\midrule
T1 & byte-level acceptance equation & \code{verify_accepts_iff} \\
T2 & canonical encoding lift & \code{verify_accepts_iff_point} \\
T3 & injectivity / point equation & \code{verify_accepts_iff_point_eq} \\
T4 & constructive decompression lift & \code{verify_accepts_iff_decompress} \\
\bottomrule
\end{tabular}
\end{center}

\end{document}