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.
The four ed25519 verification pyramids each ended their first post with an honest asterisk — the signature apex was proven at the byte level, and lifting it to the point level was deferred. That deferral is now closed, on all four forks: decompress is extracted and proven, the modular square root is proven, compress is canonical, and the acceptance criterion now reads as a real curve-point equation.
A 106-page LaTeX/TikZ book plus compiling exercise files - a curriculum that takes an undergraduate with zero formal-methods background to the point of reading, and extending, the real Lean 4 proofs in the ed25519/Pallas verification family.
The proof pyramid rebuilt against Solana's solana-ed25519 crate — its own Charon/Aeneas extraction, its own compiled certificates. Forks drift; theorems about the upstream prove nothing about the fork.
The fourth ed25519 target - the curve25519-dalek fork used by Betrusted/Precursor, the security-first open hardware device whose entire boot chain and update trust reduce to this code accepting the right signatures.
Machine-checked correctness for the ed25519 implementation everyone actually ships — field, group law, scalar arithmetic, and the EdDSA acceptance criterion itself — proven in Lean 4 about the Aeneas-transpiled Rust, not about a flattering re-model.
Verification of the Pallas field layer in zcash/pasta_curves — Montgomery-form 4×64-limb arithmetic, with the 255-bit modulus's primality machine-checked via a Lucas/Pratt certificate. A do-over of an earlier attempt that axiomatized exactly the statements that needed proving.
The third target of the ed25519 verification family - RISC Zero's curve25519-dalek fork (v4.1.3), the one that runs inside zkVM guests. A ZK proof attests that code ran; it does not attest that the code is correct. These certificates cover the half the SNARK can't.