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 sole cryptographic identity anchor: 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

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

The trust anchor — pin this key

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 whole mirror. Nothing else.

Attested libraries

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

Three ways to use it

#	Artifact	What it is	Where
1	`provider.ed25519.pub`	The identity anchor. The provider's public key — the sole 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}`

Quick check (any machine, milliseconds): download artifacts 1–3, then
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).

Zero-install audit: 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.

Autonomous agent: the pacta tool adds STH pinning, freshness policy, online refresh from this service, risk scoring (R0–R5, six named residual-risk classes) with policy-gated consequences, and optionally verifies every signature through the proof-attested Ed25519 code path itself (--require-verified-verifier).

API

What a verified inclusion means — and what it does not

does not mean A verified binary. The proofs cover Rust source; clone the attested commit (the commit id identifies the committed git tree — not external dependencies, toolchain downloads, or generated artifacts) and build it yourself — compiler and build are declared trusted base (assumed, not proven) until the reproducible-builds program lands and retires risk class R5. Every attestation carries its full residual-risk list — the enumerated assumptions inside its attestation.json. Honesty about the boundary is the product.

You hold the ruler

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 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 and the 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.

A card you write yourself will match this log's supply exactly — and that is engineered, not coincidence: the corpus was shrunk until every remaining axiom justifies its existence. If your card is stricter (say: "SHA-512 itself must be proven"), there is nothing here to negotiate — the gap is itemized, never blurred, and you have three honest options: accept a named line item, walk away, or prove the missing piece and enter it into this same log. If your ruler is stricter than our supply, your ruler is our roadmap. (The full walk-through is lecture 11 of the Jupyter course in the pacta repo.)

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.

Paper and log, one story. Since the August 2026 revisions the paper describes this deployment as it runs — nineteen leaves, dual-signed heads, the post-quantum verify path as leaf 18 with its own certificate appendix. The log is append-only and keeps growing past any paper revision; every number the paper states stays checkable against the retained history: python3 verify.py --all re-verifies all of it, paper-era and after, from a clone of the mirror.

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.