Second, additive anchor — post-quantum. Heads from -tree 14 on additionally carry a deterministic SLH-DSA-SHA2-128s (FIPS 205) -signature over the same payload. The Ed25519 signature above remains the one every consumer must -check; this one is checked where tooling allows (OpenSSL ≥ 3.5). Its verify path is the -proof subject of leaf 18.
+Key 2 — SLH-DSA-SHA2-128s (FIPS 205), additive +post-quantum. Heads from tree size 14 on carry a second signature from this key; +older heads legitimately have none — an append-only log keeps its history. Check it where your +tooling allows (OpenSSL ≥ 3.5). The kind of code that verifies such signatures is itself +a proof subject of this log (leaf 18).
{slh_pem}
SHA-256 fingerprint {slh_fp}
· raw: {base or ''}/log-slhdsa-public-key
@@ -162,13 +162,14 @@ proof subject of leaf 18.
This key is the required cryptographic identity anchor — the one every consumer must check: it -authenticates that these statements were made by the operator (the same party the artifacts call “the provider”). It does not, by itself, make -those statements true — each attestation's truth additionally rests on the replay, theorem, -extraction and toolchain assumptions stated in that leaf (one signed entry of the tree below). Every tree head and attestation is -signature-checked against this key. -Pin it (save your own copy; from then on trust only what checks against that copy), and compare this copy byte-for-byte with the independently hosted -mirror copy; they must be identical. The first fetch is trust-on-first-use; the two-host byte-comparison is what bounds it.
+Two keys sign everything in this log. Neither makes a +claim true; they prove a claim comes from this operator, unchanged. Save your own copy +of both — that is called pinning: from then on you trust only what verifies against +your saved copies. Fetch each key from this page AND from the independently hosted mirror and +compare byte-for-byte; the copies must be identical. (The first fetch is trust-on-first-use; +comparing two independent hosts is what bounds it.)
+Key 1 — Ed25519, required. Every signed head and every attestation must +verify against it.
{pem}
SHA-256 fingerprint {escape(fingerprint)}
· raw: {base or ''}/log-public-key
@@ -221,93 +222,91 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
· code
· cv
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.
+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.
-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.
+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.
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.
openssl command (preinstalled on most Linux and macOS systems).
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.pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub-The
pacta CLI ships in the
+Your machine checks one Ed25519 signature and
+~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes — no proof assistant involved.
+The pacta tool 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.pip install . from a clone); about forty lines of ordinary Python do the same
+check, and the mirror’s verify.py contains exactly that core. Afterwards the
+claim — which repository, which exact source version, which theorems, which assumptions —
+is bound to the operator’s key inside a history he can neither rewrite nor deny.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).pacta automates the comparison; lecture 11 of the Jupyter course (same
+repository) teaches it step by step.
+Afterwards every verdict is your verdict — the operator’s labels can at
+most veto, never grant. The section “You hold the ruler” below is this rung in full.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.verification/check.sh.
+Clone the repository at the exact source version recorded in its log entry and run the script:
+the proof assistant re-checks every theorem on your machine and prints every assumption list.
+The operator is now out of the loop entirely.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 log is a Merkle tree: every entry (“leaf”) is hashed, hashes pair +up level by level, and a single 32-byte root fingerprints the entire history; the operator signs +that root. Changing any past entry would change the root — that is the tamper evidence. This +picture is computed from the live log at page render — the leaf hashes, nodes, root, and +signature are the real ones:
{tree_svg}verified attestation (all certificates proven, axiom cones boundary-exact) historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves 0–3: an early audit round that failed; leaves 4–7 re-attest the same four libraries cleanly)
-Every box above is computed from the live log at page render — leaf hashes, -internal nodes, the root, and the signature are the real ones. The library that signs the log is itself an entry in the log — what that entry proves is its verify path (no signing code is proven, here or anywhere) — and it checks its own entry before signing. In detail: before signing this +
The library that signs the log is itself an entry in the log — what that entry proves is its verify path (no signing code is proven, here or anywhere) — and it checks its own entry before signing. In detail: before signing this root, the provider Merkle-verified its own signing library's leaf (index {provenance.get('signing_library_leaf_index','?')}, certificates {escape(str(provenance.get('signing_library_certificates_proven','?')))}) @@ -335,7 +334,9 @@ which observed axiom cones (the exact set of assumptions each proof ultimately r
entries/<library>.receipt.jsonverify.py wraps that core with full fail-closed binding checks (stdlib hashing; signature checks shell out to the openssl binary).verify.py contains exactly that core, wrapped in
+fail-closed safety checks (stdlib hashing; signature checks shell out to the openssl binary).
receipts/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 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
-
-
python3 verify.py --all
-re-verifies all of it, paper-era and after, from a clone of the mirror.
+stays checkable against the retained history: the mirror clone from rung 1 of the
+ladder re-verifies all of it, paper-era and after.
Log heads are signed offline; this service is read-only and holds no -key material. Provider tooling, agent tooling, and the full Jupyter course live in the pacta repository.
+key material. Provider tooling, agent tooling, and the full Jupyter course live in the +pacta repository. +Software integrators: the machine interface behind every link on this page is described by the +OpenAPI document at/openapi.json — the
+pacta tool builds on it (head pinning, freshness policy, risk scoring R0–R5).