An append-only witness for "the proof still checks" — the Lean Transparency Log
The ed25519 proof pyramids have a failure mode that has nothing to do with the mathematics. The proofs are correct. But a proof is a claim about a specific commit of a specific repo re-checking with a specific set of axioms — and every part of that sentence decays. The repo advances. The toolchain updates. Six months on, "it verified" is something you remember rather than something you can point at. The proof didn't rot; the evidence that it holds right now did.
Two small projects address that, and they're two halves of one idea.
The log: lean-transparency-log
An append-only, Merkle-anchored ledger of attestations — signed statements that the Lean proofs of a named library, at a named commit, re-check with exactly their documented axiom cone. The structure borrows directly from Certificate Transparency (RFC 9162), because the problem is the same shape: make a claim publicly, permanently, and verifiably-by-anyone.
entries/NNNNNN.json— one leaf per attestation, append-only. The git
history of the repo is the log history.
sth-history.jsonl— every Signed Tree Head ever issued. This is the
witness channel: every cloner sees the same sequence of heads, so a split view (showing you one history and someone else another) is detectable.
receipts/<component>.receipt.json— an inclusion proof binding a specific
attestation to a signed head.
verify.py— a standalone checker, Python standard library only. No install,
no service trust: clone the repo, run it, confirm the Merkle math yourself.
The honesty rules are the interesting part, because a transparency log that only records good news is marketing with extra steps. The log retains early leaves that record a failed audit run — an append-only trust ledger keeps its history, including the parts where the check was red. Attestations cover the Rust source at a pinned commit — the git hash is the content hash, so you clone it and build it yourself; compilers are declared trusted base, out loud. And the tree heads are signed by the merkleized, proof-attested Ed25519 library itself, with each signature embedding the provider's own Merkle self-check of that library's leaf — the log verifies the tool that signs the log.
The tool: the proof-aware agent
The log answers "does this proof hold?" The companion tooling answers the question a downstream consumer actually has, which is narrower and sharper:
Does this theorem cover the exact code path that will protect my funds?
That's the question an autonomous economic agent must answer before it trusts a piece of cryptographic infrastructure — and it's not the same as "is there a proof." A proof can be immaculate and cover the wrong function. The tooling interprets the shipped Lean artifacts as evidence, checks that the attested certificate's axiom cone is exactly the documented one (three Lean foundations plus the named SHA-512/wire-format boundary — no silent growth), and refuses receipts that don't carry the signatures it requires. It runs locally, moves no funds, and makes no financial decision; it decides one thing only — whether the evidence is good enough to rely on.
Why both, and why now
The verification family proved the code. The book teaches people to read the proofs. This is the third leg: a way for a machine — or a skeptical human — to check, at any later moment, that a specific proof still holds under exactly the assumptions it claimed, without re-running the whole Lean toolchain and without trusting my say-so. Proof, pedagogy, and a witness that outlives my memory of having run it.
Live service, same data plus documentation: ltl.zkdefi.org. Clone the repo and run python3 verify.py --all to check the whole thing from first principles — which is the only endorsement of a transparency log that means anything.