zkdefi · notes · code · cv

LTL — the Lean Transparency Log

Every known way of consuming formal verification fails on one of two sides: either the cost stays with you (re-running a theorem prover), or the cost disappears because you are asked to believe a label. This site holds the point in between — it makes machine-checked proof results as cheap to check as one signature and a handful of hashes, without turning them into trust. Every claim the operator ever makes is recorded here permanently, bound to his key, and scoped to its exact assumptions: he can never be believed, only held accountable.

Concretely: 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. Each completed proof check is one signed, numbered entry that can never be altered or removed — 19 entries so far, drawn live further down this page. How much of our work you re-verify is your choice, from milliseconds to everything:

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 ~5 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

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.

-----BEGIN PUBLIC KEY-----
MCowBQYDK2VwAyEAd6WIt2/WNJCcKMZGo67BQoZI84LbvLaYMvpwAWNXsxU=
-----END PUBLIC KEY-----

SHA-256 fingerprint 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a  ·  raw: /log-public-key  ·  curl -s https://ltl.zkdefi.org/log-public-key

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

-----BEGIN PUBLIC KEY-----
MDAwCwYJYIZIAWUDBAMUAyEAAiq/WvlW5b5jIu9pdVigtyjbM3c2CGjm+D6COsGf
qUs=
-----END PUBLIC KEY-----

SHA-256 fingerprint d92a8b6069f6ccb7f953a6fd35f34a11877549d431dde782491e04adf0b5191a  ·  raw: /log-slhdsa-public-key  ·  mirror: provider.slhdsa.pub

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:

leaf 0dalek ✗leaf 1anza ✗leaf 2risc0 ✗leaf 3betrusted ✗leaf 4dalekleaf 5anzaleaf 6risc0leaf 7betrustedleaf 8dalekleaf 9anzaleaf 10risc0leaf 11betrustedleaf 12accumleaf 13dalekleaf 14anzaleaf 15risc0leaf 16betrustedleaf 17accumleaf 18slh-dsanoded181bbe2fd…node3df0f44e1e…nodef3724e6671…node3bb1e72abb…node3253f2e4dc…node906823a876…node7e01627bcb…noded67b2bcdec…node58a462ffc2…node96be9a56c2…node04541cffd4…node65695789e3…noded564975516…node060a3e6950…nodede919cde8d…node9a15b9a137…nodeaca2c0af5d…nodede919cde8d…node04374a5e6e…nodede919cde8d…ROOT7ee2394068…Signed Tree Head — Ed25519 + SLH-DSA(7ee239406890…)signed by: verified-dalek-serial(verify path attested; signing itself not proven)

verified attestation — every certificate proven, every assumption list exactly as declared 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 13, certificates 44/44) 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 19, log id 205e4c389cb143e0….

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.

#ArtifactWhat it isWhere
1provider.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 the claim 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: hold the complete history yourself (rung 1 of the ladder). 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 https://github.com/saymrwulf/lean-transparency-log

Attested libraries

libraryclaim (attestation)proof of inclusion (receipt)certificates proven
anza-ed25519-verifiedattestationinclusion proof44/44 proven
betrusted-ed25519-verifiedattestationinclusion proof44/44 proven
dalek-ed25519-verifiedattestationinclusion proof44/44 proven
fips205-slhdsa-verifiedattestationinclusion proof11/11 proven
ltl-accumulator-verifiedattestationinclusion proof61/61 proven
risc0-ed25519-verifiedattestationinclusion proof44/44 proven

What a verified inclusion means — and what it does not

means The provider whose key you hold attests: the Lean proofs of the named repository at the named git commit re-check with exactly the documented assumptions — and this signed head irrevocably commits that statement to this view. Consumers who compare heads, or retain the public mirror, can expose any conflicting view.
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. 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 — 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.
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.15, August 2026 · DOI 10.5281/zenodo.22057482). The full design and its security analysis: what the log guarantees, stated as precise games with proofs — and what it deliberately does not guarantee, with the same honesty discipline as this page, at referee depth. It also tells the project’s best war story: the mechanized model caught our own deployed verifier omitting a single condition of RFC 9162 — invisible to ordinary testing, 3,867 wrong acceptances across 73,573 adversarial cases, zero after the one-line fix. If you read one thing, read the claim matrix at the end: every promise, what establishes it, and what remains assumed.

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