The Lean Transparency Log looks a lot like an optimistic rollup for verification claims — cheap to assert, expensive to get away with. The resemblance is real and worth having, but the precise version is better than the slogan. Three layers of guarantee, two very different kinds of fault, three honest disanalogies, and one loop that needs no metaphor at all.
The Lean Transparency Log has always notarized proofs about other people's software. As of today it notarizes the proofs about its own machinery — entry 13 is a kernel-checked mechanization of the log's own accumulator, appended into the log itself, verifiable end to end from the live service by anyone with a stock toolchain.
A verification proof is a claim about a specific commit. Claims rot — the repo moves, the axioms drift, "it verified once" becomes folklore. The Lean Transparency Log is an append-only, Merkle-anchored ledger of signed attestations that named proofs re-check with exactly their documented assumptions, plus the agent tooling that asks the only question a downstream consumer cares about.