2026-07-06 14:02:23 +00:00
# Lean Transparency Log — published mirror
This repository is the **git-published face** of a transparency log of
formal-verification attestations: signed statements that the Lean 4 proofs
2026-07-16 18:40:21 +00:00
of specific software, at specific git commits, re-check with exactly their
documented assumptions. Its first twelve leaves attest four cryptographic
2026-08-16 16:32:42 +00:00
Rust libraries (Ed25519 implementations); as of **its thirteenth entry (leaf index 12, 2026-07-16)**
2026-07-16 18:40:21 +00:00
the log also attests **its own accumulator machinery** — a kernel-checked
2026-07-16 21:46:28 +00:00
mechanization of the log's security analysis, so the log carries
kernel-checked proofs *about the accumulator model* underlying its own
inclusion and consistency reasoning, as one of its own entries (subject
2026-07-16 18:40:21 +00:00
[`ltl-accumulator-verified` ](https://github.com/saymrwulf/ltl-accumulator-verified );
2026-07-16 21:46:28 +00:00
scoped to the mechanized model — it does not prove operator honesty,
entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed
Six new leaves (tree 13 -> 19, root 7ee23940…):
[13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
generation recorded 16). The delta is the P0-P2 hardening
campaign: scalar statements bound, kernel-side axiom gate,
driver surface with cones, declaration coverage both directions,
the accounting identity.
[17] ltl-accumulator-verified — 61 certificates; the log again carries
proofs of its own Merkle machinery, at the hardened state.
[18] fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
over the SLH-DSA-SHA2-128s verify path, apex
fips205.slh_verify_128s_accepts_iff.
Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.
Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.
Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 15:11:59 +00:00
signing, or execution provenance). As of **2026-08** the log also attests
2026-08-16 16:32:42 +00:00
the **SLH-DSA (FIPS 205) verify-path proofs** (leaf 18)
entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed
Six new leaves (tree 13 -> 19, root 7ee23940…):
[13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
generation recorded 16). The delta is the P0-P2 hardening
campaign: scalar statements bound, kernel-side axiom gate,
driver surface with cones, declaration coverage both directions,
the accounting identity.
[17] ltl-accumulator-verified — 61 certificates; the log again carries
proofs of its own Merkle machinery, at the hardened state.
[18] fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
over the SLH-DSA-SHA2-128s verify path, apex
fips205.slh_verify_128s_accepts_iff.
Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.
Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.
Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 15:11:59 +00:00
([`fips205-slhdsa-verified`](https://github.com/saymrwulf/fips205-slhdsa-verified))
2026-08-22 16:41:44 +00:00
and its heads carry a **second, post-quantum SLH-DSA-SHA2-128s signature**
entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed
Six new leaves (tree 13 -> 19, root 7ee23940…):
[13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
generation recorded 16). The delta is the P0-P2 hardening
campaign: scalar statements bound, kernel-side axiom gate,
driver surface with cones, declaration coverage both directions,
the accounting identity.
[17] ltl-accumulator-verified — 61 certificates; the log again carries
proofs of its own Merkle machinery, at the hardened state.
[18] fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
over the SLH-DSA-SHA2-128s verify path, apex
fips205.slh_verify_128s_accepts_iff.
Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.
Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.
Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 15:11:59 +00:00
beside the required Ed25519 one. The current head is `latest-sth.json` —
this README deliberately names no tree size, so it cannot go stale.
2026-07-06 14:02:23 +00:00
Layout:
| Path | Content |
|---|---|
| `entries/NNNNNN.json` | one log leaf per file, append-only (git history mirrors log history) |
| `entries/<component>.attestation.json` | the newest attestation per library, for convenience |
| `receipts/<component>.receipt.json` | inclusion proof binding that attestation to the latest signed head |
| `sth-history.jsonl` | **every** Signed Tree Head ever issued — the witness channel: all cloners see the same heads |
| `latest-sth.json` | the current head |
entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed
Six new leaves (tree 13 -> 19, root 7ee23940…):
[13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
generation recorded 16). The delta is the P0-P2 hardening
campaign: scalar statements bound, kernel-side axiom gate,
driver surface with cones, declaration coverage both directions,
the accounting identity.
[17] ltl-accumulator-verified — 61 certificates; the log again carries
proofs of its own Merkle machinery, at the hardened state.
[18] fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
over the SLH-DSA-SHA2-128s verify path, apex
fips205.slh_verify_128s_accepts_iff.
Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.
Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.
Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 15:11:59 +00:00
| `provider.ed25519.pub` | the provider's Ed25519 public key — the REQUIRED identity anchor; each statement's truth additionally rests on the assumptions stated in its leaf |
| `provider.slhdsa.pub` | the provider's SLH-DSA-SHA2-128s public key (FIPS 205) — checks the ADDITIVE post-quantum head signature; needs OpenSSL >= 3.5, and verify.py degrades honestly below that |
verify.py: --all verifies every published receipt; binding fields required, not compare-if-present (round-12 GPT B4)
Round-12 review found two artifact-claim gaps: --all never touched
receipts, and receipt mode checked fingerprint/leaf_hash only when
present. Now:
- --all enumerates receipts/*.receipt.json and runs the full binding
list on each (type tag, STH signature, REQUIRED key fingerprint,
log_id vs log-metadata, STH membership in the published history,
REQUIRED leaf_hash vs the named entry, tree_size agreement, receipt
hash_algorithm + log_id consistency, inclusion proof).
- --receipt FILE routes through the same function.
- Malformed values (bad hex, missing sizes) are failures, not crashes.
- NEW verify_selftest.py: 11-case adversarial battery (mutated real
receipts must be REJECTED: no fingerprint, no leaf_hash, wrong type,
forged root, size mismatch, wrong log_id; honest controls pass;
structural-only never claims full; no-openssl exits 2). GREEN.
One bug caught by the honest controls during development: the new
hash-algorithm check assumed 'sha256' but deployed heads carry
'RFC9162_SHA256' - fixed against reality, plus receipt-level
hash_algorithm/log_id binding added.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-17 09:15:19 +00:00
| `verify.py` | standalone verifier (Python stdlib + the `openssl` binary; fails closed without them; `--all` covers every published receipt) |
| `verify_selftest.py` | adversarial self-test: proves the verifier's fail-closed paths reject mutated receipts |
2026-07-06 14:02:23 +00:00
Verify everything locally, no installation:
```bash
python3 verify.py --all
python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json
```
The online service (same data, live endpoints + customer documentation):
2026-07-06 17:15:03 +00:00
**https://ltl.zkdefi.org**
2026-07-06 14:02:23 +00:00
2026-08-22 16:41:44 +00:00
The design and its security analysis:
**https://ltl.zkdefi.org/paper** (DOI [10.5281/zenodo.22057482 ](https://doi.org/10.5281/zenodo.22057482 ))
2026-07-06 14:02:23 +00:00
The provider tooling, agent tooling, and course materials:
**https://github.com/saymrwulf/proof-aware-crypto-tooling-agent**
Honesty notes, always in force: attestations cover Rust **source** at a
2026-07-19 11:04:53 +00:00
pinned commit (clone it — the commit identifies the committed git tree,
not dependencies or toolchains — and build it yourself; compilers are
declared trusted base). The log deliberately
2026-07-06 14:02:23 +00:00
retains early leaves recording a **failed** audit run: an append-only
trust ledger keeps its history. Tree heads are signed by the merkleized,
proof-attested Ed25519 library itself, and each signature embeds the
entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed
Six new leaves (tree 13 -> 19, root 7ee23940…):
[13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
generation recorded 16). The delta is the P0-P2 hardening
campaign: scalar statements bound, kernel-side axiom gate,
driver surface with cones, declaration coverage both directions,
the accounting identity.
[17] ltl-accumulator-verified — 61 certificates; the log again carries
proofs of its own Merkle machinery, at the hardened state.
[18] fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
over the SLH-DSA-SHA2-128s verify path, apex
fips205.slh_verify_128s_accepts_iff.
Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.
Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.
Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 15:11:59 +00:00
provider's own Merkle self-check of that library's leaf. Heads additionally
carry a **deterministic SLH-DSA-SHA2-128s signature** over the same payload:
2026-08-22 16:41:44 +00:00
strictly additional, so Ed25519 remains the signature a consumer must check, and honest
entries 13-18: re-attest the estate at 44 certs/fork + first SLH-DSA leaf; heads now dual-signed
Six new leaves (tree 13 -> 19, root 7ee23940…):
[13-16] dalek/anza/risc0/betrusted-ed25519-verified — re-attested at 44
certificates each (27 main + 4 apex + 13 scalar; the leaf 8-11
generation recorded 16). The delta is the P0-P2 hardening
campaign: scalar statements bound, kernel-side axiom gate,
driver surface with cones, declaration coverage both directions,
the accounting identity.
[17] ltl-accumulator-verified — 61 certificates; the log again carries
proofs of its own Merkle machinery, at the hardened state.
[18] fips205-slhdsa-verified — FIRST post-quantum leaf: 11 certificates
over the SLH-DSA-SHA2-128s verify path, apex
fips205.slh_verify_128s_accepts_iff.
Heads from tree 14 on carry a second, ADDITIVE signature:
SLH-DSA-SHA2-128s (FIPS 205), deterministic, over the same payload as the
Ed25519 signature. provider.slhdsa.pub ships beside the Ed25519 key.
Ed25519 remains the signature consumers must check; verify.py now judges
slh_dsa fail-closed where present (INVALID/WRONG-KEY/NO-PUBKEY fail; older
heads report ABSENT, allowed; pre-3.5 OpenSSL degrades loudly, never
silently). The ml_dsa slot stays not_configured — truthfully.
Honesty, unchanged by any of it: the certificates cover VERIFICATION paths
of the extracted Lean models; no signing operation is proven for any
algorithm; leaves are Ed25519-signed at issuance only.
Append-only law checked byte-for-byte before this commit: entries
000000-000012 identical, the six prior heads an exact prefix of the
history. verify.py --all: RESULT OK [full]. verify_selftest.py: GREEN (13
cases). Quorum gate: 5-way Ed25519 + 2-way SLH-DSA (incl. the verifier
built from the pinned proven source), all accept, all reject corruption.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 15:11:59 +00:00
about scope — the estate's certificates cover the *verification* path of both
algorithms; no signing operation is proven for either, and leaves themselves
are Ed25519-signed at issuance only. Heads published before 2026-08 have no
SLH-DSA signature and verify.py reports them as `slh_dsa:ABSENT` , which is
allowed — an append-only log keeps its history.
