Optimistic by construction — what the log promises, and where the rollup analogy honestly stops
The announcement post covered what entry 13 is. This one is about what the design actually promises — and, just as deliberately, what it does not.
What is actually inside the tree
A persistent misreading of transparency logs is that they "contain the proofs." The Lean Transparency Log's tree contains none of the Lean mathematics. Each leaf is (the hash of) a verification-event record: a signed attestation that the operator, at a given time, ran the proof checks on a named repository at an exact commit, with an exact toolchain, and observed a specific result — every certificate verified, each with an exactly-listed axiom cone. The proofs live one hop away, in the subject repositories the record pins.
So a leaf is a statement about the operator's action — "I verified X" — which on its face sounds like "trust me." The design's whole point is the refinement that removes the trust: the claim names its own evidence. Because the leaf pins commit and toolchain, anyone can replay the verification and check the statement. The log converts
"I guarantee I verified the proofs (which live elsewhere)"
into
"I claim this, permanently and publicly, with enough detail that anyone can catch me lying — and I can never unsay it, edit it, or show a different history to someone else."
Three layers, three distinct guarantees, and most confusion comes from expecting one layer to do another's job. The Lean kernel guarantees the mathematics of the attested proofs, given their declared axioms — and nothing about what the operator later claims. The replay pin guarantees the claim is checkable — and not that anyone has actually checked it. The Merkle accumulator with signed heads guarantees inclusion, append-only history, and equivocation evidence — and not that any claim is true. The ledger notarizes; it does not referee.
The rollup resemblance — a bounded analogy
Optimistic rollups rest on one bet: claims are cheap to make and expensive to get away with. A sequencer posts state roots without proof; safety comes from anyone's ability to produce compact, transferable evidence of a specific fault. The LTL — like its ancestor, Certificate Transparency — sits at the same design point: record everything append-only, and make misbehavior produce publicly verifiable evidence.
That correspondence is genuine and useful. It is also an analogy with three honest disanalogies, not an equivalence — and the precise version is what makes it interesting. Two very different faults get conflated:
Fault 1: the operator rewrites or forks the log's history. This is what the mechanized corpus covers, and the result is a reduction, not a courtroom verdict. The consistency theorem says: if the verifier accepts a proof linking a pinned head to a rewritten history, a named extractor outputs a SHA-256 collision as two concrete byte strings. Read that exactly — it does not say "the operator is guilty"; it says "accepting this would break SHA-256." Under the standing judgment that nobody can produce such a collision, the attack simply cannot succeed — which is stronger than a fraud proof that convicts after the fact. The one place the operator is directly on the hook is equivocation: two conflicting signed heads at the same size, in one log context, are transferable evidence attributable to the key holder — that reduces to signature unforgeability, and it is the closest true analogue of a rollup fraud proof. The liveness caveat transfers too: someone must actually watch. An unwatched log, like an unwatched rollup, is safe only on paper.
Fault 2: a leaf's content is simply false — the operator claims a verification it never ran. This is the optimistic part, and the honest limit: the cryptography does not catch it. The Merkle machinery commits a false statement as faithfully as a true one. What catches it is independent replay — off-protocol work with a theorem prover, not a challenge transaction the log adjudicates. The log's contribution is to make the claim precise enough to replay and impossible to later unsay. Two things do compare favorably with rollups: the challenge window is effectively infinite (a false leaf cannot be reverted, only exposed — its permanence is the exposure), and there is no privileged adjudicator — every reader replays independently.
The three disanalogies, plainly: the extractors are reduction witnesses against a hash assumption, not on-protocol fraud proofs against the operator; fabricated leaves are caught only by off-protocol replay; and there is no bond, no slashing, no revert — consequences are reputational and out-of-band, exactly as in Certificate Transparency, where the "slash" is a browser distrusting a CA. The dual this estate implements instead of prover-side bonding is consumer-side defense: a quorum of independently attested verifiers on the consumer's side of the trust boundary.
The loop that needs no metaphor
Set the analogy aside and state the plain fact. Since 2026-07-16 the log carries, as one of its own entries, a kernel-checked mechanization of the soundness arguments its accumulator relies on — the collision extractors, the consistency binding, the pin-store safety — scoped honestly to the mechanized model and shipped with a fifteen-item ledger of what is not proven. The proofs about the machinery live inside the ledger the machinery protects.
You do not have to take any of this on my word — that is the entire point:
- Entry 13, leaf hash
8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a,
under head tree size 13, root 3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d — live at ltl.zkdefi.org/v1/sth, leaf and inclusion proof at /v1/attestation?component=ltl-accumulator-verified.
- Or clone the mirror
and run python3 verify.py --all — a fail-closed, standard-library verifier that re-checks every leaf, every signed head, and every receipt offline, with its adversarial self-test shipped beside it.