LTL — Lean Transparency Log

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.

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.

{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

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.

Choose where you stand — the trust ladder

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.

“I just want the history held honest.” — anyone, one minute.
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.

“I trust the operator’s reports; bind him to them.” — milliseconds.
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.

“I accept his observations — not his judgment.” — minutes; the rung most people miss.
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).

“I don’t trust his observations — I’ll run the proofs myself.” — about 30 minutes per library.
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.

“I trust none of it — I’ll rebuild the whole path.” — weeks.
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)

The accumulator, live

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 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 additive post-quantum key (provider.slhdsa.pub) and the whole mirror. Nothing else.

Attested libraries

One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone).

What a verified inclusion means — and what it does not

You hold the ruler

For your tooling — the raw API

#	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). A one-page Python core verifies it — printed as Appendix C of the paper; the shipped `verify.py` wraps that core with full fail-closed binding 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}`

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.

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.