This site is a public notary for machine-checked proofs about cryptographic -software. A proof assistant — Lean 4, a program -that checks mathematical proofs mechanically — has verified precise statements about the code -that checks signatures: in four widely deployed Ed25519 libraries, in an -implementation of SLH-DSA (FIPS 205, the hash-based post-quantum signature -standard), and in the Merkle-tree machinery of this log itself. Every completed -proof check is recorded here as a signed, numbered entry that can never be altered or removed — -{len(entries)} entries so far, drawn live further down this page.
+Every known way of consuming formal verification fails on one of two +sides: either the cost stays with you (re-running a theorem prover), or the cost +disappears because you are asked to believe a label. This site holds the point in +between — it makes machine-checked proof results as cheap to check as one +signature and a handful of hashes, without turning them into trust. Every claim +the operator ever makes is recorded here permanently, bound to his key, and +scoped to its exact assumptions: he can never be believed, only held +accountable.
-Re-checking such proofs yourself takes a toolchain and real compute time. This log gives you -cheaper positions to stand on: in milliseconds you can verify that the operator is permanently -bound to every claim he ever made — and you can escalate, step by step, up to redoing -everything yourself. The ladder below lists every position, cheapest first.
+Concretely: a proof assistant — Lean 4, a +program that checks mathematical proofs mechanically — has verified precise +statements about the code that checks signatures: in four widely deployed +Ed25519 libraries, in an implementation of SLH-DSA +(FIPS 205, the hash-based post-quantum signature standard), and in the +Merkle-tree machinery of this log itself. Each completed proof check is one +signed, numbered entry that can never be altered or removed — {len(entries)} entries +so far, drawn live further down this page. How much of our work you re-verify is +your choice, from milliseconds to everything: