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>
Doc-freshness audit (2026-07-19): the homepage received these two
round-10 scope corrections in Tier 2 but the mirror README kept the old
wording — 'sole trust anchor' -> sole cryptographic identity anchor
(truth rests on each leaf's stated assumptions); 'the git hash is the
content hash' -> the commit identifies the committed git tree, not
dependencies or toolchains.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
GPT-5.6 live-site review + Fable live verification:
- verify.py §4: was fail-OPEN — no openssl ⇒ signatures 'skipped' ⇒
still 'OK'. Now fail-CLOSED (exit 2 unless --structural-only, which is
explicitly labelled a reduced check). --receipt was Merkle-path-only;
now verifies the receipt's STH signature, key fingerprint, log_id,
tree_size agreement, leaf_hash-vs-entry, and history membership before
the inclusion proof. --all now also checks latest-sth == final history
head and size == leaf count, and constant log_id. Adversarially tested:
fail-closed exit 2; forged unsigned-root receipt REJECTED (was the
'inclusion VALID' hole); honest receipt + full run still exit 0.
- README §8: I had written 'the first deployed transparency log to carry
proofs of its own honesty' this session — an overclaim (the corpus
proves properties of the accumulator MODEL, not operator honesty).
Now: 'kernel-checked proofs about the accumulator model underlying its
inclusion/consistency reasoning', 'first' softened to 'unaware of a
precedent'.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Broadened 'Rust libraries' framing to 'specific software'; noted the
first-of-its-kind self-attestation and the current 13-leaf head.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The log now carries kernel-checked proofs of its own accumulator
machinery. Entry 13 attests the ltl-accumulator-verified corpus at
freeze 172a1d0: 61 certificates, all proven with exact axiom cones,
single opaque-SHA-256 axiom boundary. Scope (in the leaf): the
mechanized recursive model is kernel-checked; deployed-verifier
correspondence is finite differential testing; the deployed
consistency verifier is not extensionally equal to the model and
relies on an unmechanized authentic-size/root invariant (gaps 14/15).
tree 12 -> 13, root 3488a2d0; head signed verified-dalek-serial.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The public face of the Lean Transparency Log: every leaf (including the
first run's honest audit-failure attestations), the full STH history
(witness channel), per-component receipts, the provider public key, and
a standalone stdlib-only verify.py.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
