The log notarizes itself — entry 13
The Lean Transparency Log notarizes claims of the form "this exact version of this software was formally verified, and here is the receipt." It records them in an append-only, Merkle-anchored ledger so that nobody — including the operator — can quietly rewrite history or show two different histories to two different people. For its first twelve entries it did this for other people's software: four independent Ed25519 implementations, each with its own machine-checked proof corpus.
There was always one uncomfortable asymmetry. The log demands kernel-checked proofs of everyone else. What backed the log's own security — the argument that a forged inclusion receipt or a doctored history is impossible without breaking SHA-256 — was careful human mathematics. Correct, reviewed, but human.
As of today that asymmetry is gone. Entry 13 is the kernel-checked mechanization of the log's own accumulator: every theorem in the security analysis — inclusion completeness and soundness, consistency soundness, the pin-store safety property — rewritten in Lean 4 and checked by the same merciless kernel that checks the Ed25519 corpora, from a single stated assumption (SHA-256 is a hash function) with everything else derived mechanically. 61 certificates, all proven, all with their exact axiom cones audited. And it is appended into the log itself — the machinery now carries the proofs of its own honesty as one of its own entries.
What "honest" means here, precisely
The interesting part is what the entry does not claim. The proofs are about a mechanized model of the verifier. The deployed verifier is close but not extensionally identical — there is a known, measured seam where the shipped code accepts a slightly larger set of inputs than the proven model (a consistency proof presented under a dishonestly-labelled size), which real usage never supplies but which the model formally rejects. Rather than paper over it, the leaf says so: its scope block states, in the notarized record itself, that the mechanized model is what is kernel-checked, that deployment correspondence rests on finite differential testing plus one explicitly-named operational invariant, and that "the deployed verifier is formally verified" is not a claim it makes. A log whose whole purpose is accountability had better be accountable about its own limits, in writing, permanently.
This is optimistic accountability, not validity
If this feels like the accountability model behind optimistic rollups and Certificate Transparency, it should — it is the same genus. The log doesn't prevent a dishonest operator up front; it makes dishonesty manufacture its own evidence. The mechanized consistency-soundness theorem is, read the right way, a constructive fraud-proof generator: if anyone gets the verifier to accept a rewritten history, the theorem hands you a SHA-256 collision built from the attacker's own messages. What entry 13 adds — and what optimistic systems generally aspire to and rarely have — is a formally verified fraud-proof mechanism, sitting inside the very ledger it protects. (The long version: optimistic-accountability.md.)
Check it yourself
The point of all of this is that you don't have to trust the paragraph above. The log is live and the entry is fetchable and verifiable right now:
tree size 13 root 3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d
entry 12 ltl-accumulator-verified @ 172a1d0
leaf hash 8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50aThe signed head is at ltl.zkdefi.org/v1/sth; the entry's attestation and its inclusion receipt are served by the log; the old twelve-leaf head (bcd15f9d…) is a provable prefix of the new one — the log demonstrating on itself the exact consistency property it now carries a proof of. Fetch it, check the signature against the published key, verify the inclusion proof, and re-run the corpus with a stock public Lean if you want the proofs themselves. Nobody's word is required, which was the entire idea.