zkdefi · notes · code · cv

LTL — the Lean Transparency Log

One sentence: a public, append-only Merkle accumulator of signed statements that the Lean 4 formal proofs of specific cryptographic Rust libraries, at specific git commits, machine-re-check with exactly their documented assumptions — so that you can trust a proof result by checking one signature and ~4 hashes in milliseconds, instead of running a theorem prover for hours.

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

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. Before signing this root, the provider Merkle-verified its own signing library's leaf (index 4, certificates 16/16) against this very tree — the signature vouches for the code that produced it, and the tree vouches for the signature's code. Tree size 8, 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 whole mirror. Nothing else.

#	Artifact	What it is	Where
1	`provider.ed25519.pub`	The trust anchor. The provider's public key — the only thing you take on trust, once. Compare the copy here with the copy in the GitHub mirror; they must be identical.	mirror
2	`<library>.attestation.json`	The claim. Which repo, which exact git commit, which theorems, which observed axiom cones, what machine protection — signed by the provider.	table above, 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. ~25 lines of stdlib Python verify it.	table above, or mirror `receipts/`
+	the full mirror clone	Maximal benefit: become a witness. Every leaf + every signed head ever issued + `verify.py` (stdlib-only). `python3 verify.py --all` recomputes the entire tree and every historical head — you then hold proof the log never equivocated within your clone.	`git clone https://github.com/saymrwulf/lean-transparency-log`

Attested libraries

component	artifact 2	artifact 3	status
`anza-ed25519-verified`	attestation	inclusion proof	16/16 proven
`betrusted-ed25519-verified`	attestation	inclusion proof	16/16 proven
`dalek-ed25519-verified`	attestation	inclusion proof	16/16 proven
`risc0-ed25519-verified`	attestation	inclusion proof	16/16 proven

Three ways to use it

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. Add --sth-store pins.json for split-view defense.

Zero-install audit: git clone https://github.com/saymrwulf/lean-transparency-log && python3 verify.py --all
Standard-library Python only. 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) with policy-gated consequences, and optionally verifies every signature through the proof-attested Ed25519 code path itself (--require-verified-verifier).

API

GET /v1/sth                      latest Signed Tree Head
GET /v1/sth-history              every head ever signed (witness material)
GET /v1/sth-consistency?first=N  consistency proof from your pinned size
GET /v1/proof?component=NAME     inclusion proof (artifact 3, freshly issued)
GET /v1/attestation?component=NAME   the claim (artifact 2)
GET /v1/entries?start=N&end=M    raw leaves
GET /v1/metadata                 log identity
GET /healthz

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 that statement is irrevocably part of the log every other customer and witness sees.

does not mean A verified binary. The proofs cover Rust source; clone the attested commit (the git hash is the content hash) and build it yourself — compiler and build are declared trusted base until the reproducible-builds program (R5) lands. Every attestation carries its full residual-risk list. Honesty about the boundary is the product.

The paper

LTL: the Lean Transparency Log (PDF, 4 pages) — the design in full: the trust model (observations, never verdicts), the self-certifying signature, the deployment with its retained failure leaves, and an exact account of what a verified receipt does and does not establish.

Log heads are signed offline; this service is read-only and holds no key material. Provider tooling, agent tooling, and the full course (12 Jupyter lectures) live in the pacta repository.