One sentence: a public, append-only Merkle
-accumulator (a hash tree that only ever grows) of signed statements that the Lean 4 formal proofs of specific
+ What happened here, in plain terms: we took real cryptographic
+code — four production Ed25519 signature libraries and the verification path of
+SLH-DSA (FIPS 205), the post-quantum signature standard — and machine-checked
+mathematical proofs about it with the Lean 4
+proof assistant. Re-checking those proofs yourself takes a toolchain and about half
+an hour of compute per library. This site is the shortcut that does not ask for
+blind trust: a public, tamper-evident ledger of signed statements about every proof
+check we ran — so you decide how much of our work you re-verify, from a millisecond
+signature check to redoing everything. The same thing, in one precise sentence: a public, append-only Merkle
+accumulator (a hash tree that only ever grows) of signed statements that the Lean 4 formal proofs of specific
cryptographic Rust libraries, at specific git commits, re-check by machine with exactly
their documented assumptions — so that you can trust a proof result by checking
one required signature (Ed25519) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in
milliseconds, instead of running a theorem prover for hours. Every rung below is a legitimate place to stand. Each states what you still take
+on trust, what you do, what it costs, and what you know afterwards. Climb one rung
+at a time — the whole service is built so that you can. One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone). Humans never need these directly; every link on this page already uses them. They
+exist so that your software — a CI job, an autonomous agent, a package
+resolver — can consume the log without scraping HTML. The Choose where you stand — the trust ladder
+
+Still trusted: everything — but lying becomes attributable.
+git clone https://github.com/saymrwulf/lean-transparency-log && cd lean-transparency-log && python3 verify.py --all
+Python plus the system openssl binary; fails closed without it.
+Afterwards you hold every leaf and every Signed Tree Head (STH) ever issued. If the
+operator ever shows anyone a conflicting history, your copy exposes it — you are a
+witness. A split view (the operator showing different histories to different
+consumers) survives only until two witnesses compare.
+Still trusted: that the recorded observations are honest.
+Download the three artifacts (key, claim, inclusion proof — table below), then:
+pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub
+The pacta CLI ships in the
+pacta repository
+(pip install . from a clone); a one-page Python core (the paper’s
+Appendix C) does the same check without it. Add --sth-store pins.json to
+remember every head you accept. Afterwards the exact claim — repository, commit,
+theorems, assumptions — is cryptographically pinned to the operator’s key inside an
+append-only history: he can never rewrite or deny it. What he observed, you
+have not yet checked.
+Still trusted: the recorded axiom lists; not the operator’s pass/fail labels.
+Compare each attestation’s recorded assumption cones against a requirements card
+you write yourself — pacta automates the comparison, and lecture 11 of the
+Jupyter course
+walks through it.
+Afterwards every verdict is your verdict, re-derived from your
+own ruler; operator labels can veto but never grant acceptance (details in
+“You hold the ruler” below).
+Still trusted: the published Lean sources and the extraction that produced them;
+not the operator’s execution. Clone the attested repository at its pinned
+commit and press its check button (verification/check.sh) with a Lean 4
+toolchain: the kernel re-checks every certificate on your machine and the axiom
+audit prints the exact assumption cones.
+Afterwards the theorem prover accepted on your hardware —
+the operator is out of the loop entirely.
+Still trusted: Lean’s kernel, the extraction tools, and your compiler — the floor,
+which we name rather than hide. Pin the upstream Rust source yourself, extract it to
+Lean with Charon/Aeneas (every repository ships its extract.sh, pinned
+toolchain versions, and byte-pinned generated models for comparison), re-read the
+theorem statements against FIPS 205 / RFC 9162 / the curve equations, and re-prove
+or audit each certificate.
+Afterwards you have reproduced the estate and no longer need us —
+which is the point. There is no rung above this one: even here you trust a kernel, a
+compiler, and your silicon. Anyone offering zero trust is selling something.The trust anchors — pin these keys (one required, one additive)
{_trust_anchor_html(log, metadata, base, mirror)}
@@ -284,30 +353,6 @@ consumers.)
Three ways to use it
-
-pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub
-
No Lean, no Rust, no account. The pacta CLI ships in the pacta repository (pip install . from a clone). Add --sth-store pins.json to remember every Signed Tree Head (STH) you accept — your defense against a split view (the operator showing different histories to different consumers).git clone {mirror} && cd lean-transparency-log && python3 verify.py --all
-
Standard-library Python plus the system openssl binary (signature checks fail closed without it). You become a witness of the whole history.--require-verified-verifier).API
-GET {base}/v1/sth latest Signed Tree Head
-GET {base}/v1/sth-history the published head history (witness material)
-GET {base}/v1/sth-consistency?first=N consistency proof from your pinned size
-GET {base}/v1/proof?component=NAME inclusion proof (artifact 3, freshly issued)
-GET {base}/v1/attestation?component=NAME the claim (artifact 2)
-GET {base}/v1/entries?start=N&end=M raw leaves
-GET {base}/v1/metadata log identity
-GET {base}/healthz
-
What a verified inclusion means — and what it does not
For your tooling — the raw API
+pacta CLI
+builds on them: STH pinning, freshness policy, risk scoring (R0–R5, six named
+residual-risk classes) with policy-gated consequences, and optionally
+--require-verified-verifier, which checks every signature through the
+proof-attested Ed25519 code path itself.GET {base}/v1/sth latest Signed Tree Head
+GET {base}/v1/sth-history the published head history (witness material)
+GET {base}/v1/sth-consistency?first=N consistency proof from your pinned size
+GET {base}/v1/proof?component=NAME inclusion proof (artifact 3, freshly issued)
+GET {base}/v1/attestation?component=NAME the claim (artifact 2)
+GET {base}/v1/entries?start=N&end=M raw leaves
+GET {base}/v1/metadata log identity
+GET {base}/healthz
+
+
The paper