LTL — Lean Transparency Log

Key 2 — SLH-DSA (FIPS 205), 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 (entry 18).

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 · curl -s https://ltl.zkdefi.org/log-public-key

{slh_block}

LTL — the Lean Transparency Log

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.

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.

Choose where you stand — the trust ladder

Hold a copy of the history. — anyone; one minute.
You still trust: the content of every claim. You defeat: silent rewriting.
You need: Python 3 and the 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

This fetches the log’s public mirror — a git repository holding every entry and every signed head ever issued (a head is the signed root fingerprint of the tree at a given size) — and re-computes every hash and signature in it. A green result means the history you now hold is internally consistent and signed. Keep the folder: if the operator ever shows a different history to anyone else, your copy proves it. A log that shows different histories to different people (a “split view”) survives only until two holders compare.

Check that a claim is real and binding. — milliseconds.
You still trust: that the operator’s recorded observation is honest.
You need: four small files from the tables below — the two public keys, plus one library’s claim file (“attestation”) and its proof of inclusion (“receipt”).

pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub --slhdsa-public-key provider.slhdsa.pub

Your machine checks the required Ed25519 signature, the second (post-quantum) signature (needs OpenSSL ≥ 3.5; drop the second flag to skip it), 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); 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.

Judge by your own standards. — minutes.
Every entry records more than pass/fail: it lists the exact assumptions each proof rests on (its axiom cone). So you may ignore the operator’s verdicts entirely: write down which assumptions you accept, and have your tooling compare list against list, name by name. 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.

Re-run the proof check yourself. — about 30 minutes per library.
You still trust: that the published Lean statements mean what they say.
You need: a Lean 4 toolchain (free). Every attested repository ships one script, 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.

Rebuild everything from source. — weeks.
What remains trusted: Lean’s proof kernel, the Rust-to-Lean translation tools (Charon and Aeneas), and your compiler — the floor, which we name rather than hide. Every repository documents its full path: the pinned upstream Rust code, the extraction script that regenerates the Lean definitions byte-for-byte, and the theorem statements to read against the standards themselves (FIPS 205, RFC 9162, the curve equations). Reproduce any part; compare with what is published. After this rung you no longer need this site — that is the point. There is no rung 6: even here you trust a kernel, a compiler, and your hardware.

Two keys sign this log — pin these keys

The accumulator, live

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. Each leaf records one proof run: a batch of certificates — one machine-checked theorem each, together with its exact assumption list. This picture is computed from the live log at page render — the leaf hashes, nodes, root, and signature are the real ones:

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)

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','?')))}) against this very tree — so the signed tree contains an attestation of the source the operator reports its signing binary was built from. (An Ed25519 signature cannot by itself prove which binary generated it; execution provenance is reported, not proven, and the provenance fields live in the unsigned signature metadata.) Tree size {latest.get('tree_size',0)}, log id {escape(str(metadata.get('log_id',''))[:16])}….

What do I download? — the three artifacts, unambiguously

To benefit from the accumulator you need exactly three files per library, plus optionally the post-quantum key (provider.slhdsa.pub) and the whole mirror. Nothing else.

Attested libraries

What a verified inclusion means — and what it does not

You hold the ruler

#	Artifact	What it is	Where
1	`provider.ed25519.pub`	The identity anchor. The provider's public key — the required cryptographic identity you pin. It authenticates the operator's statements; their truth rests on each leaf's stated assumptions. Fetch it from BOTH independent locations and compare; the copies must be identical.	this site · mirror
2	`<library>.attestation.json`	The claim. Which repo, which exact git commit, which theorems, which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider.	table below, or mirror `entries/`
3	`<library>.receipt.json`	The proof of inclusion. Binds artifact 2 into the signed tree: leaf index, sibling hashes, the Signed Tree Head (STH). About forty lines of ordinary Python verify it; the mirror’s `verify.py` contains exactly that core, wrapped in fail-closed safety checks (stdlib hashing; signature checks shell out to the `openssl` binary).	table below, or mirror `receipts/`
+	the full mirror clone	Maximal benefit: become a witness. Every leaf + every signed head ever issued + `verify.py` (Python stdlib + the `openssl` binary for signatures; fails closed without them). `python3 verify.py --all` recomputes the entire tree and every historical head — you then hold a retained view that can later EXPOSE a conflicting head shown to someone else. (A single clone cannot by itself prove the log never split its view toward another consumer; that requires comparing heads across consumers.)	`git clone {mirror}`

The list of assumptions a certificate is allowed to rest on is not something this site hands you at verification time — it is a requirements card — a short plain-text file listing, by name, the assumptions you accept — that lives in your tooling, on your disk, and that you can read in five minutes or rewrite from first principles: Lean's three foundational axioms, plus — for the signature tiers only (the top proof layers, where full signature verification is proven) — named placeholders for SHA-512 (the hash function Ed25519 uses internally — the proofs treat it as an assumption, not as proven) and the byte-level wire format. Your tooling ignores this operator's pass/fail labels entirely and re-derives every verdict by comparing the attestation's observed axiom list (its cone) against your card, name by name. The operator is trusted to copy down what the proof kernel printed — never to interpret it.

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log (PDF, 25 pages, v0.12 — revised August 2026; the version is printed on the title page) — the trust decomposition (expensive verification produces an observation; transparency makes the observation accountable; consumer-local policy decides acceptance), collision-extracting soundness for inclusion and consistency, scheme-level accountability GAMES with an explicit composition theorem (head authenticity, position binding, history binding with a fully proved prefix-transport induction, context-scoped fork evidence — all discharged by named reductions), the policy boundary where operator labels can veto but never grant acceptance, and the measured model/deployment divergence reported as a result rather than hidden — now together with its closure: the divergence traced to one omitted RFC 9162 conjunct (Step 7's sn = 0), zero divergences after the one-line restoration, confirmed by a three-way regression. New in the August 2026 revisions: the deployment evaluated to its current nineteen-leaf, dual-signed state, an instantiation section for the SLH-DSA (FIPS 205) verify path — eleven certificates, five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the Ed25519 tiers.

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. 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).