Each of our four verified ed25519 libraries went from 16 proven statements to 44. But the real story of the past month is uglier and more useful — what it took to make the script that PRINTS "all green" as trustworthy as the proofs behind it.
Ed25519 signatures are deterministic — same key, same message, same signature, forever. We used that to audit ourselves, re-signing an already-published record and comparing byte for byte. The bytes matched. The exercise still caught a real bug.
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 LaTeX/TikZ book plus compiling exercise files - now in its second edition (14 chapters, 132 pages) - 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.
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.