docs: the pre-Green full-scan repairs — ESTATE/llms/evidence to the 19-leaf world, leaf-index numbering unified, instruction traps closed

ESTATE.md was still the 2026-07-22 snapshot (13 leaves, v0.9, 'SLH-DSA
NOT in the log'); llms.txt still said thirteen leaves, 23 pages, and
linked the retired /paper/v0.x routes; README repeated the stdlib-only
verify.py trap the site just fixed; evidence/README called the July
capture's 16/16 attestations 'definitive' and its 8-leaf state current.
All brought to truth. Entry numbering standardized on 0-based leaf
index with 'the thirteenth entry' as the ordinal gloss (docs, lab
manual, security note, mirror README template). Operator-machine path
removed from provider/README.

ESTATE.md

@@ -7,10 +7,11 @@ including the two self-referential loops that make the estate hard to
 keep in one head. Maintained here in pacta because pacta is the
 machinery hub and the only repo that changes freely.
 
-State snapshot (2026-07-22): log **13 leaves**, root `3488a2d0…`, key
+State snapshot (2026-08-16): log **19 leaves**, root `7ee23940…`, key
-fingerprint `874c8a00…`, paper **v0.9 camera-ready (23 pp)**, five
+fingerprint `874c8a00…`, heads dual-signed (Ed25519 + SLH-DSA) since
-attested components, one campaign open (SLH-DSA — **eleven
+size 14, paper **v0.11 (25 pp, revised August 2026)**, six attested
-certificates**), pacta suite 144 green.
+components (SLH-DSA verify path = leaf 18, the first post-quantum
+entry), pacta suite 153 green.
 
 ```mermaid
 flowchart LR
@@ -23,20 +24,20 @@ flowchart LR
     s6["fips205-source"]
   end
   subgraph V["VERIFIED SUBJECTS"]
-    d["dalek-ed25519-verified<br/>44 certs today · attested at 16 (leaf 8 · signer source)"]
+    d["dalek-ed25519-verified<br/>attested 44/44 (leaf 13 · signer source; earlier gens 0/4/8)"]
-    a["anza-ed25519-verified<br/>44 certs today · attested at 16 (leaf 9)"]
+    a["anza-ed25519-verified<br/>attested 44/44 (leaf 14; earlier gens 1/5/9)"]
-    r["risc0-ed25519-verified<br/>44 certs today · attested at 16 (leaf 10)"]
+    r["risc0-ed25519-verified<br/>attested 44/44 (leaf 15; earlier gens 2/6/10)"]
-    b["betrusted-ed25519-verified<br/>44 certs today · attested at 16 (leaf 11)"]
+    b["betrusted-ed25519-verified<br/>attested 44/44 (leaf 16; earlier gens 3/7/11)"]
     p["pasta-pallas-verified<br/>field layer only · NOT attested"]
-    f["fips205-slhdsa-verified<br/>11 certs proven · reviewer attest-with-conditions · NOT in the log"]
+    f["fips205-slhdsa-verified<br/>11 certs proven · attested — leaf 18 (first post-quantum)"]
-    c["ltl-accumulator-verified<br/>61 certs · entry-13 subject · frozen 172a1d0"]
+    c["ltl-accumulator-verified<br/>61 certs · leaf 12 subject · re-attested leaf 17 (hardened)"]
   end
   subgraph M["MACHINERY — pacta + operator-held"]
     prov["provider service<br/>check · append · publish · site code · templates (CI-pinned)"]
     sig["dogfood signer<br/>verified-dalek binary"]
     lib["consumer library<br/>receipts · pin store · R0–R5"]
     wal["warden (code)<br/>quorum wallet · MCP · cockpit (local, read-only)"]
-    pap["paper<br/>v0.9 + v0.1/v0.2 archives"]
+    pap["paper<br/>v0.11 (archives in git history)"]
     crs["course + llms.txt<br/>14 notebooks"]
     key["SIGNING KEY (offline)"]
     ops["operational log state<br/>the true accumulator"]
@@ -81,7 +82,7 @@ flowchart LR
   d ==>|"LOOP 1: built from"| sig
   sig ==>|"LOOP 1: signs the log"| ops
   mir ==>|"LOOP 1: contains the signer's own attestation (leaf 8)"| d
-  c ==>|"LOOP 2: attested as entry 13"| prov
+  c ==>|"LOOP 2: attested as leaf 12 (13th entry)"| prov
   mir ==>|"LOOP 2: carries proofs about its own accumulator"| c
   classDef src fill:#f1f3f5,stroke:#8a93a0,color:#1c2430
   classDef sub fill:#e2f2e9,stroke:#1e7f4f,color:#1c2430
@@ -110,7 +111,7 @@ paper says so explicitly.)
 **Loop 2 — the self-attestation.** `ltl-accumulator-verified` is a Lean
 corpus proving soundness of the log's own accumulator *model*
 (extractors, consistency binding, per-step pin safety). It was attested
-into the log as **entry 13** — the log carries kernel-checked proofs
+into the log as **leaf 12** (the log's thirteenth entry) — the log carries kernel-checked proofs
 about its own machinery, scoped honestly (recursive model, not the
 deployed verifier; see the corpus KNOWN-GAPS ledger).
 
@@ -120,10 +121,10 @@ deployed verifier; see the corpus KNOWN-GAPS ledger).
 |---|---|---|---|
 | `curve25519-dalek-source`, `anza-cryptography-source`, `risc0-…-source`, `betrusted-…-source`, `pasta_curves-source` (+ `xous-core`, `litex-boards` context) | upstream | pinned inputs to extraction | **frozen — never modified** |
 | `fips205-source` | upstream | verbatim snapshot of `integritychain/fips205` (pure-Rust FIPS 205 / SLH-DSA); upstream pin `30bac08`, snapshot head `a3ce8e8` — deviations: CI workflows stripped + the documented Aeneas-compat/de-plumbing patch series (each commit individually justified) | pinned; moves only for transparent, individually-justified Aeneas-compat patches (nothing proposed upstream) |
-| `dalek-` / `anza-` / `risc0-` / `betrusted-ed25519-verified` | subject | Rust source + Lean proofs; 44 certs each today (27 main + 4 apex + 13 scalar; 16 at the leaf 8–11 attestations, generations at 0–7) | attested commits fixed; branches carry substantial post-attestation proof work (scalar layer, apex tier, hardening rounds), staged for re-attestation |
+| `dalek-` / `anza-` / `risc0-` / `betrusted-ed25519-verified` | subject | Rust source + Lean proofs; 44 certs each, attested 44/44 as leaves 13–16 (2026-08-08); earlier 16-cert generations at leaves 8–11, first generations at 0–7 | attested commits fixed |
 | `pasta-pallas-verified` | subject | field layer proven; curve layer pending; **not attested** | changes freely |
-| `fips205-slhdsa-verified` | subject | SLH-DSA (FIPS 205) verify-path campaign, parameter set SLH-DSA-SHA2-128s; **11 certificates proven, `check.sh` green with an 18-attack self-test, outside-reviewer attest-with-conditions**; not appended to the log | changes freely — campaign |
+| `fips205-slhdsa-verified` | subject | SLH-DSA (FIPS 205) verify-path campaign, parameter set SLH-DSA-SHA2-128s; **11 certificates proven, `check.sh` green with an 18-attack self-test**; attested — leaf 18 (2026-08-08), the log's first post-quantum entry | attested commit fixed |
-| `ltl-accumulator-verified` | subject | 61-cert corpus about the log's accumulator model; **entry-13 subject**, frozen `172a1d0` | frozen; doc-only commits allowed |
+| `ltl-accumulator-verified` | subject | 61-cert corpus about the log's accumulator model; **leaf 12 subject**, frozen `172a1d0`; hardened model re-attested as leaf 17 (2026-08-08) | frozen; doc-only commits allowed |
 | `proof-aware-crypto-tooling-agent` (this repo) | machinery | provider service, consumer library, warden (+ local read-only cockpit), dogfood signer, paper, course, tests | **changes freely — the hub** |
 | `lean-transparency-log` | published | the public mirror: leaves, heads, receipts, fail-closed `verify.py` + selftest | **generated by publish** — canonical files here, templates in pacta, CI-pinned |
 | `verifying-crypto-with-lean` | published | undergraduate book; zero coupling to log state | changes freely |

README.md

@@ -207,15 +207,18 @@ The log uses:
 - `RFC9162_SHA256` Merkle leaf/node hashing with `0x00` leaf and `0x01` node domain separation.
 - Signed Tree Heads over canonical JSON tree-head payloads.
 - OpenSSL Ed25519 signatures today.
-- An additive `SLH-DSA-SHA2-128s` / FIPS 205 slot: verify path proven (fips205-slhdsa-verified, checked by `pacta-verify-slhdsa` built from the pinned proven source); signing deterministic and parameter-locked; published heads remain Ed25519-only until the next publication.
+- An additive `SLH-DSA-SHA2-128s` / FIPS 205 slot: verify path proven (fips205-slhdsa-verified, checked by `pacta-verify-slhdsa` built from the pinned proven source); signing deterministic and parameter-locked. Since tree size 14 (2026-08-08) every published head carries this co-signature alongside Ed25519; earlier heads keep their single signature, recorded as absent-not-failed.
 - An explicit `ML-DSA-65` / FIPS 204 signature slot that is `unavailable` unless the host has a real backend. If an agent policy requires both signatures, verification fails closed.
 
 The deployed instance ([ltl.zkdefi.org](https://ltl.zkdefi.org),
 mirror [`lean-transparency-log`](https://github.com/saymrwulf/lean-transparency-log))
-is live at **13 leaves**. Entry 13 (2026-07-16) attests the log's own
+is live at **19 leaves** (2026-08-08). Entry 12 (2026-07-16) attests the log's own
 accumulator machinery — a kernel-checked mechanization of the log's
 security analysis ([`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified)),
-appended into the log itself and scoped to the mechanized model. The
+appended into the log itself and scoped to the mechanized model; entries
+13–16 re-attest the four Ed25519 forks at 44 certificates each, entry 17
+the accumulator's hardened model, and entry 18 the SLH-DSA verify path —
+the log's first post-quantum entry. The
 producer path that generated it now emits a `scope` block into each leaf
 (guarantees / exclusions / deployment-constraints), so a leaf carries its
 own honest scope, not just a claim card.
@@ -321,7 +324,9 @@ The log has three synchronized faces, transport being orthogonal to trust:
 2. **Git mirror** ([saymrwulf/lean-transparency-log](https://github.com/saymrwulf/lean-transparency-log), mirrored on Forgejo):
    every leaf, every signed tree head (the WITNESS CHANNEL - all cloners
    see the same heads), per-component receipts, the provider public key,
-   and a standalone stdlib-only `verify.py`. Anyone: `python3 verify.py --all`.
+   and a standalone `verify.py` (Python stdlib + the system `openssl`
+   binary; fails closed without it). Anyone, from inside a clone:
+   `python3 verify.py --all`.
 3. **HTTP service** (deployed at `ltl.zkdefi.org`, see
    `DEPLOY.md`): read-only CT-style endpoints + customer docs. The web
    process never touches private keys - heads are signed offline; a

docs/security-2026-07-23-consistency-terminal-check.md

@@ -68,14 +68,14 @@ return old_hash == old_root_hash and new_hash == new_root_hash and sn == 0
 
 This defect is the corpus's Known Gap 14: the project's own fidelity harness
 **found** the divergence (3,867 deployed-accepts-only cases in a pinned
-73,573-case family) and recorded it in public log entry 13. What the two-way
+73,573-case family) and recorded it in public log leaf 12 (the thirteenth entry). What the two-way
 harness could not do was assign blame — with only the deployed verifier and the
 Lean model disagreeing, and both labelled "RFC 9162", the divergence was filed
 as a scoped gap rather than a conformance bug. A post-appeal review round added
 the missing third oracle (a faithful RFC verifier), which showed the deployed
 side was the deviant one, and traced it to the omitted Step 7.
 
-Public log entry 13 and the attested accumulator commit are unchanged: the
+Public log leaf 12 and the attested accumulator commit are unchanged: the
 historical experiment remains truthfully recorded and reproducible at the
 tagged pre-fix commit. The IACR submission PDF is unchanged. The corpus
 Known-Gaps ledger records this closure.

docs/warden-lab-manual.md

@@ -705,7 +705,7 @@ tripwire that screams when the map forks from itself.
     Ed25519 implementation that is itself verified and attested *inside the
     log it signs* (leaf 8). The tool guards the evidence; the evidence
     covers the tool.
-  - **Loop 2, the self-attesting mechanization:** entry 13 of the log is the
+  - **Loop 2, the self-attesting mechanization:** leaf 12 of the log (its thirteenth entry) is the
     kernel-checked mechanization of the very soundness arguments the log's
     accumulator relies on. The proofs about the machinery live inside the
     ledger the machinery protects — scoped honestly, with a published list
@@ -975,7 +975,7 @@ boolean.
 
 **6.1** Loop 1: the log's signing machinery runs on an Ed25519
 implementation that is itself verified and attested inside the log it
-signs (leaf 8). Loop 2: entry 13 is the kernel-checked mechanization of
+signs (leaf 8). Loop 2: leaf 12 is the kernel-checked mechanization of
 the accumulator arguments the log itself relies on — the proofs about the
 machinery live in the ledger the machinery protects.
 **6.2** Because "what is running" is invisible from any single machine and

evidence/README.md

@@ -4,18 +4,24 @@ Signed, transparency-logged attestations from a REAL guarded replay of the
 four `saymrwulf/*-ed25519-verified` repositories (2026-07-06/07, ~30 min of
 Lean re-checking per fork under `lean-guard` memory caps).
 
+This directory is a dated capture, kept byte-stable on purpose: every file
+verifies against the head it cites. The live log has since grown (19 leaves,
+dual-signed heads); `python3 verify.py --all` in the public mirror re-checks
+today's full state.
+
 | File | What it is |
 |---|---|
 | `<fork>-ed25519.attestation.yaml` | Signed proof-check attestation: repo commit, environment, machine-protection block, and all 16 certificates with their OBSERVED axiom cones (the four apex tiers carry the fork's exact documented boundary) |
 | `<fork>-ed25519.receipt.yaml` | RFC 9162-style inclusion receipt binding the attestation into the transparency log (tree size 8), with a consistency anchor |
 | `provider.ed25519.pub` | The provider's public key (the PRIVATE key never leaves `provider/state/`, which is gitignored) |
-| `log-metadata.json`, `latest-sth.yaml` | Log identity and the latest Signed Tree Head |
+| `log-metadata.json`, `latest-sth.yaml` | Log identity and the Signed Tree Head at capture time (tree size 8) |
 | `log-audit.txt` | Monitor self-check output (recomputed root matches the signed root) |
 
-The log holds EIGHT leaves: entries 0-3 are the first run's attestations,
+At the time of this capture (2026-07) the log held eight leaves: entries 0-3 are the first run's attestations,
 which honestly record an AUDIT FAILURE (two bugs in pacta's audit step,
-since fixed - see the commit history); entries 4-7 are the definitive
+since fixed - see the commit history); entries 4-7 are that run's
-16/16-proven attestations. An append-only trust ledger keeps its bad day.
+16/16-proven attestations (the forks were later re-attested at 44/44 as
+leaves 13-16; the live log now holds nineteen leaves). An append-only trust ledger keeps its bad day.
 
 Re-verify everything yourself (signature via the proven-path verifier if
 built, STH pinning, freshness):

llms.txt

@@ -19,8 +19,8 @@
 
 ## Live evidence
 
-- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs. Thirteen leaves: three replay generations over four Ed25519 forks, plus entry 13 attesting the Lean mechanization of the log's own accumulator model. The mirror ships a fail-closed offline verifier (verify.py --all covers every leaf, signed head, and receipt) with an adversarial self-test.
+- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs. Nineteen leaves: three replay generations over four Ed25519 forks (newest at 44/44 certificates, leaves 13-16), the Lean mechanization of the log's own accumulator model (leaves 12 and 17), and the first post-quantum leaf - the SLH-DSA (FIPS 205) verify path (leaf 18); heads dual-signed (Ed25519 + SLH-DSA) since size 14. The mirror ships a fail-closed offline verifier (verify.py --all covers every leaf, signed head, and receipt) with an adversarial self-test.
-- The paper: https://ltl.zkdefi.org/paper — "Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log" (23 pages: trust decomposition, scheme-level accountability games with explicit reductions, live deployment, and the measured model/deployment divergence reported as a result). Earlier versions archived at /paper/v0.2 (19 pages) and /paper/v0.1 (4 pages).
+- The paper: https://ltl.zkdefi.org/paper — "Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log" (25 pages, v0.11, revised August 2026: trust decomposition, scheme-level accountability games with explicit reductions, live deployment, and the measured model/deployment divergence reported as a result). Superseded drafts remain retrievable from the repository git history.
 
 ## For agents
 

paper/.gitignore

@@ -2,3 +2,4 @@
 *.log
 *.out
 *.toc
+rendered-pages/

paper/README.md

@@ -1,10 +1,12 @@
 # Which file is current?
 
-**`ltl.pdf` / `ltl.tex` — the current paper (v0.10, revised August 2026).**
+**`ltl.pdf` / `ltl.tex` — the current paper (v0.11, revised August 2026).**
-The review process concluded in August 2026; this revision folds in the
+The review process concluded in August 2026. v0.10 folded in the
-corrections queued during the freeze (certificate-count update, the
+corrections queued during the freeze (the closed consistency-verifier
-closed consistency-verifier divergence with its `sn = 0` root cause, a
+divergence with its `sn = 0` root cause, replay-harness-integrity
-replay-harness-integrity limitation, and an added claim-matrix row). The
+limitation, claim-matrix row); v0.11 brings the paper up to the live
+system: the nineteen-leaf dual-signed deployment, the SLH-DSA (FIPS 205)
+verify-path instantiation, and its certificate appendix. The
 version submitted for review (July 17, 2026, sha256 `7f140356…`) is
 preserved unchanged in this repository's git history. The live copy at
 <https://ltl.zkdefi.org/paper> serves the current revision.
@@ -14,5 +16,5 @@ on 2026-08-15; like every prior state of this folder, they remain
 retrievable from this repository's git history.
 
 Revisions v0.3–v0.9 were successive overwrites of `ltl.tex`; they live in
-this repository's git history. v0.9 is the submitted version — the
+this repository's git history. v0.9 is the version that was submitted
-current `ltl.pdf` above.
+for review; v0.10 and v0.11 supersede it.

paper/check-paper.sh

@@ -0,0 +1,84 @@
+#!/usr/bin/env bash
+# check-paper.sh — the paper's form gate.
+#
+# Ports the book's check-book.sh lesson to the paper: the 2026-08-16
+# socratic round found a ghost page (a fossil \clearpage) and a solid-set
+# claim matrix whose badness-10000 warnings had printed in EVERY build,
+# unread. This gate makes both classes of defect fail the build instead
+# of shipping silently. It cannot replace the render-and-look eye pass —
+# it renders the pages so the eye pass has no excuse.
+#
+# Usage:  ./check-paper.sh            build + all gates + render pages
+#         ./check-paper.sh --selftest exercise the gate parsers on
+#                                     known-bad and known-good log lines
+set -euo pipefail
+cd "$(dirname "$0")"
+
+OVERFULL_LIMIT_PT=10
+MIN_PAGE_CHARS=300     # calibrated 2026-08-16: real minimum was 922 (claim-matrix page)
+PAGES_DIR=rendered-pages
+
+fail() { echo "FAIL: $*" >&2; exit 1; }
+
+# --- gate parsers (pure text -> verdict; selftestable) -------------------
+overfull_violations() {  # stdin: build log -> lines exceeding the limit
+  grep -i 'Overfull \\hbox' | grep -oP '\(\K[0-9.]+(?=pt too wide)' \
+    | awk -v lim="$OVERFULL_LIMIT_PT" '$1 > lim' || true
+}
+badness_violations() {   # stdin: build log -> badness-10000 underfull lines
+  grep -i 'Underfull \\hbox (badness 10000)' || true
+}
+
+if [[ "${1:-}" == "--selftest" ]]; then
+  n=0
+  t() { n=$((n+1)); [[ "$2" == "$3" ]] && echo "selftest $n ok: $1" || fail "selftest $n: $1 (got '$3', want '$2')"; }
+  t "80pt overfull trips" "80.05" \
+    "$(echo 'warning: x.tex:1: Overfull \hbox (80.05pt too wide) in paragraph' | overfull_violations)"
+  t "3.4pt overfull passes" "" \
+    "$(echo 'warning: x.tex:1: Overfull \hbox (3.374pt too wide) in paragraph' | overfull_violations)"
+  t "badness 10000 trips" "1" \
+    "$(echo 'warning: x.tex:1: Underfull \hbox (badness 10000) in paragraph' | badness_violations | wc -l)"
+  t "badness 2913 passes" "0" \
+    "$(echo 'warning: x.tex:1: Underfull \hbox (badness 2913) in paragraph' | badness_violations | wc -l)"
+  echo "selftest: $n/$n ok"; exit 0
+fi
+
+# --- 1. build ------------------------------------------------------------
+LOG=$(mktemp); trap 'rm -f "$LOG"' EXIT
+tectonic ltl.tex 2>&1 | tee "$LOG" >/dev/null
+grep -qi '^error' "$LOG" && fail "TeX errors in build log"
+
+# --- 2. overfull gate ----------------------------------------------------
+OV=$(overfull_violations <"$LOG")
+[[ -z "$OV" ]] || fail "overfull hbox beyond ${OVERFULL_LIMIT_PT}pt: $OV"
+
+# --- 3. loose-typesetting gate (the ignored-warnings class) --------------
+BAD=$(badness_violations <"$LOG" | wc -l)
+[[ "$BAD" -eq 0 ]] || fail "$BAD underfull badness-10000 lines (gappy table/paragraph)"
+
+# --- 4. ghost-page gate (the fossil-clearpage class) ---------------------
+NPAGES=$(pdfinfo ltl.pdf | awk '/^Pages:/{print $2}')
+for p in $(seq 1 $((NPAGES-1))); do
+  chars=$(pdftotext -f "$p" -l "$p" ltl.pdf - 2>/dev/null | tr -d '[:space:]' | wc -c)
+  [[ "$chars" -ge "$MIN_PAGE_CHARS" ]] || fail "page $p is mostly blank ($chars chars) — ghost page"
+done
+
+# --- 5. content probes ---------------------------------------------------
+VERSION=$(grep -oP '\\date\{[^}]*---\s*\Kv[0-9.]+' ltl.tex || true)
+[[ -n "$VERSION" ]] || fail "cannot extract version from \\date{...} in ltl.tex"
+pdftotext -f 1 -l 1 ltl.pdf - | grep -q "$VERSION" || fail "title page does not carry $VERSION"
+! pdftotext ltl.pdf - | grep -q '??' || fail "unresolved ?? reference in PDF"
+
+# --- 5b. site claim binding: the webdocs paper card's page count ---------
+WEBDOCS=../provider/src/pacta_provider/webdocs.py
+if [[ -f "$WEBDOCS" ]]; then
+  STATED=$(grep -oP '\(PDF, \K[0-9]+(?= pages)' "$WEBDOCS" || true)
+  [[ -n "$STATED" ]] || fail "webdocs paper card lost its '(PDF, N pages' claim"
+  [[ "$STATED" -eq "$NPAGES" ]] || fail "webdocs says $STATED pages, PDF has $NPAGES"
+fi
+
+# --- 6. render for the mandatory eye pass --------------------------------
+rm -rf "$PAGES_DIR"; mkdir -p "$PAGES_DIR"
+pdftoppm -png -r 110 ltl.pdf "$PAGES_DIR/p"
+echo "OK: $VERSION, $NPAGES pages, no overfull>${OVERFULL_LIMIT_PT}pt, no badness-10000, no ghost pages, no ?? refs."
+echo "NOW LOOK: the render-and-look law is not automated. Flip every page in $PAGES_DIR/."

paper/ltl.tex

@@ -12,7 +12,7 @@
 \usepackage{tikz}
 \usetikzlibrary{arrows.meta,positioning,fit,decorations.pathreplacing,calc}
 \usepackage[colorlinks=true,linkcolor=blue!55!black,citecolor=blue!55!black,urlcolor=blue!55!black]{hyperref}
-\hypersetup{pdftitle={Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log},pdfauthor={Olaf Horvath},pdfsubject={Transparency distribution of formal-verification replay evidence},pdfkeywords={formal verification, transparency log, Lean, Ed25519, Merkle tree, attestation}}
+\hypersetup{pdftitle={Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log},pdfauthor={Olaf Horvath},pdfsubject={Transparency distribution of formal-verification replay evidence},pdfkeywords={formal verification, transparency log, Lean, Ed25519, SLH-DSA, FIPS 205, Merkle tree, attestation}}
 \lefthyphenmin=2 \righthyphenmin=3
 
 \newtheorem{definition}{Definition}
@@ -26,6 +26,7 @@
 \newcommand{\Hh}{\mathsf{H}}
 \newcommand{\hleaf}{\mathsf{h}_{\rm leaf}}
 \newcommand{\hnode}{\mathsf{h}_{\rm node}}
+\hyphenation{time-stamp time-stamps}
 \newcommand{\MTH}{\mathsf{MTH}}
 \newcommand{\Root}{\mathsf{Root}}
 \newcommand{\Path}{\mathsf{Path}}
@@ -47,7 +48,7 @@ showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em}
 \large A Transparency Model and the Lean Transparency Log}
 \author{Olaf Horvath\\
 \small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805}
-\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.10}}
+\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.11}}
 
 \begin{document}
 \maketitle
@@ -73,10 +74,15 @@ We instantiate the model as the Lean Transparency Log (LTL), using Lean~4 replay
 attestations and an RFC~9162 Merkle tree. We give explicit
 collision-extracting arguments for inclusion and consistency, lift them to
 scheme-level accountability games with a composition theorem, and evaluate a
-live deployment over four production Ed25519 codebases. The public log
+live deployment over four production Ed25519 codebases and the verification
-contains thirteen leaves; the thirteenth attests a Lean mechanization of the
+path of SLH-DSA (FIPS~205), the hash-based post-quantum signature standard.
+The public log contains nineteen leaves, including a Lean mechanization of the
 accumulator's own security arguments (61 human-reviewed certificates with one
-project-specific uninterpreted SHA-256 boundary axiom). The mechanization effort also exposed,
+project-specific uninterpreted SHA-256 boundary axiom) and, as its newest
+entry, eleven certificates over the SLH-DSA-SHA2-128s verifier. Since tree
+size 14 every signed head additionally carries a deterministic SLH-DSA
+co-signature --- produced with the parameter set whose verification path the
+log itself attests. The mechanization effort also exposed,
 via differential testing, a nontrivial implementation boundary --- the
 deployed iterative consistency verifier is not extensionally equal to the
 recursive model on malformed size claims --- and the leaf records this
@@ -130,7 +136,7 @@ The contribution is not a new Merkle tree and not a new theorem prover. It is a
 trust decomposition for distributing machine-checked correctness evidence:
 
 \begin{center}
-\fbox{\parbox{0.91\linewidth}{
+\fbox{\parbox{0.91\linewidth}{\raggedright\hyphenpenalty=10000\exhyphenpenalty=10000
 \textbf{Expensive deterministic verification produces an observation.
 Transparency makes that observation accountable. Consumer-local policy decides
 whether the observation is acceptable.}}}
@@ -163,11 +169,14 @@ those observations with their own policy; operator labels can veto but cannot
 grant acceptance. We state clearly that axiom-name equality is not semantic
 identity of theorem statements.
 \item \textbf{A deployed cryptographic case study.}
-The log contains twelve historical replay leaves for four verified Ed25519
+The log contains nineteen leaves: three four-fork replay generations for the
-codebases and a thirteenth leaf for the accumulator's own Lean corpus. The
+Ed25519 codebases (the newest at 44 certificates per fork), two attestations
-entry-13 corpus carries an environment-derived audit inventory of 222 compiled
+of the accumulator's own Lean corpus (entry 13 carries an environment-derived
-constants, 61 human-reviewed certificate cones, and a single uninterpreted
+audit inventory of 222 compiled constants, 61 human-reviewed certificate
-SHA-256 axiom.
+cones, and a single uninterpreted SHA-256 axiom; leaf 17 re-attests the
+hardened state), and --- as leaf 18 --- the log's first post-quantum subject:
+eleven certificates over the SLH-DSA-SHA2-128s verification path
+(Appendix~\ref{app:slhtiers}).
 \item \textbf{A negative deployment result.}
 Differential testing found that the deployed iterative RFC-style consistency
 verifier and the recursive model proved in Lean are not extensionally equal:
@@ -287,7 +296,7 @@ observed axiom-name set. The deployed schema additionally carries diagnostics,
 resource controls, scope, and exclusions.
 
 \begin{definition}[Attestation-transparency scheme]
-An attestation-transparency scheme is a tuple
+An attestation-transparency scheme is a~\mbox{tuple}
 \[
 \Pi=(\mathsf{KeyGen},\mathsf{Append},\mathsf{ProveIncl},
 \mathsf{VerifyIncl},\mathsf{ProveCons},\mathsf{VerifyCons},\mathsf{Verdict})
@@ -452,6 +461,19 @@ size, root hash, timestamp, and hash-algorithm identifier. The canonical JSON se
 those fields is signed with Ed25519. The log identifier and version tag prevent
 cross-log and cross-protocol replay.
 
+Since tree size 14, every head additionally carries a \emph{deterministic}
+SLH-DSA-SHA2-128s (FIPS~205) signature over the same payload. The
+co-signature is additive: the Ed25519 signature remains the one every
+consumer must verify, and heads published before size 14 carry no
+post-quantum signature --- the standalone verifier reports them as absent
+rather than failing them, because an append-only log keeps the history of
+its own signature scheme. Determinism is chosen as an audit primitive: a
+deterministic re-sign of the same payload is byte-comparable, so ``same
+input, same signature'' becomes a diff rather than an assurance. The
+co-signature closes a further loop: its parameter set is exactly the one
+whose verification path is attested at leaf 18
+(\S\ref{sec:slhdsa}, Appendix~\ref{app:slhtiers}).
+
 The current implementation records signing-backend provenance alongside the
 signature, but that provenance is not execution attestation: an Ed25519
 signature does not identify the program that produced it. The public system
@@ -1040,7 +1062,7 @@ verifier inherits the refinement boundary of the previous subsection
 unchanged.
 \end{remark}
 
-\section{Lean and Ed25519 instantiation}\label{sec:instantiation}
+\section{Lean instantiation: Ed25519 and SLH-DSA}\label{sec:instantiation}
 
 \subsection{Proof corpus}
 
@@ -1083,6 +1105,38 @@ The separation keeps residual assumptions visible. SHA-512 and selected
 wire-format interfaces are opaque boundaries at the apex; lower arithmetic and
 group certificates use the foundational Lean axioms observed in the corpus.
 
+\subsection{The SLH-DSA verify path: the method on second terrain}\label{sec:slhdsa}
+
+The second campaign extracts the verification path of SLH-DSA (FIPS~205,
+parameter set SHA2-128s) from a pinned pure-Rust implementation through the
+same Charon/Aeneas route, starting from one monomorphic entry point with the
+five hash primitives marked opaque at the extraction boundary. The corpus is
+eleven certificates: ten loop-fidelity theorems (chain walking, WOTS
+recomputation and checksum, XMSS and FORS Merkle ascent, hypertree layering,
+digit/byte plumbing) and an acceptance characterization,
+\code{slh_verify_128s_accepts_iff}: for every message digest, signature, and
+public key at these parameters, the extracted verifier accepts exactly when
+the recomputed hypertree root byte-equals the public key's root --- no other
+acceptance path exists.
+
+The terrain differs from Ed25519 in one structural way, and the leaf says so.
+The Ed25519 bridges land in an independent second semantics
+($\mathbb{Z}/p\mathbb{Z}$, which the proof library understands without ever
+seeing the extracted code); SLH-DSA verification is hash chains and Merkle
+nodes all the way down, so the reference folds are built from the same five
+uninterpreted hash oracles (\code{h_msg}, \code{f}, \code{h},
+\code{t_l}, \code{t_len}, modeling the SHA-256 instantiations) that the
+extracted loops call. Each loop certificate therefore makes the extracted
+control flow \emph{visible} --- small, sequential, checkable against the
+standard's algorithms --- while the reading of fold against FIPS~205 remains
+a declared human step. The audit enforces every certificate's axiom set
+exactly in both directions, and the cone \emph{grows} up the pyramid ---
+pure bit arithmetic rests on the kernel alone; the apex carries all five
+oracles (Appendix~\ref{app:slhtiers}). Scope, stated in the leaf: the proved
+subject is a monomorphic facade whose bridge to the deployed generic verifier
+is a 137-case differential test; one inner digit-extraction loop carries no
+certificate; signing and key generation were never extracted.
+
 \subsection{Replay attestation}
 
 For every certificate the operator records:
@@ -1119,18 +1173,23 @@ deployed verifier?
 
 \subsection{Public state}
 
-As of 16 July 2026, the public log contains thirteen leaves and current root
+As of 15 August 2026, the public log contains nineteen leaves and current root
 \begin{center}
-\path{3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d}.
+\path{7ee239406890cf4ad59cc83ac3faa3d5cc48b29202159ee8c25bffd9737d32d8}.
 \end{center}
-Every signed head issued since public mirroring began is retained --- six
+Every signed head issued since public mirroring began is retained --- twelve
-heads, at tree sizes 8 through 13 --- together with every leaf and receipt, in
+heads, at tree sizes 8 through 19, dual-signed from size 14 on --- together
-an append-only Git mirror; a clone re-verifies the entire log offline with the
+with every leaf and receipt, in an append-only Git mirror; a clone
-repository's standalone verifier.
+re-verifies the entire log offline with the repository's standalone verifier.
 The first twelve leaves are three four-fork replay generations. Leaves 0--3
 record a failed audit run and remain permanently visible. Leaves 4--7 record a
 clean replay. Leaves 8--11 re-attest rewritten repository histories rather
-than replacing the old leaves. A leaf whose pinned commit ceases to be
+than replacing the old leaves. Leaf 12 attests the accumulator's own Lean
+corpus (\S\ref{sec:deployment}, E3); leaves 13--16 re-attest the four
+Ed25519 corpora at 44 certificates each; leaf 17 re-attests the accumulator
+corpus at its hardened state; and leaf 18 attests the SLH-DSA-SHA2-128s
+verification path --- the log's first post-quantum subject, and the scheme
+that has co-signed every head since size 14. A leaf whose pinned commit ceases to be
 distributed decays from a replayable claim to a historical record; consumers
 act only on attestations whose subjects they can retrieve.
 
@@ -1149,32 +1208,42 @@ boundary axiom, \code{LTLAcc.sha256}.
 \centering
 \begin{tikzpicture}[
   >=Latex,
-  box/.style={draw,rounded corners=2pt,minimum width=1.03cm,minimum height=.52cm,font=\scriptsize,align=center},
+  box/.style={draw,rounded corners=2pt,minimum width=.78cm,minimum height=.5cm,font=\tiny,align=center,inner sep=1.5pt},
   fail/.style={box,fill=black!6,draw=black!45,text=black!60},
+  pq/.style={box,fill=violet!8,draw=violet!60!black,text=violet!55!black},
   ok/.style={box,fill=green!7!white,draw=deepgreen,text=deepgreen!80!black},
   acc/.style={box,fill=blue!7!white,draw=deepblue,text=deepblue},
   arrow/.style={->,draw=black!55}
 ]
-\foreach \i in {0,...,3} {\node[fail] (l\i) at (1.08*\i,0) {\i\\failed};}
+\foreach \i in {0,...,3} {\node[fail] (l\i) at (0.82*\i,0) {\i\\failed};}
-\foreach \i in {4,...,7} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
+\foreach \i in {4,...,7} {\node[ok] (l\i) at (0.82*\i,0) {\i\\clean};}
-\foreach \i in {8,...,11} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
+\foreach \i in {8,...,11} {\node[ok] (l\i) at (0.82*\i,0) {\i\\clean};}
-\node[acc] (l12) at (1.08*12,0) {12\\accum.};
+\node[acc] (l12) at (0.82*12,0) {12\\accum.};
+\foreach \i in {13,...,16} {\node[ok] (l\i) at (0.82*\i,0) {\i\\re-att.};}
+\node[acc] (l17) at (0.82*17,0) {17\\accum.};
+\node[pq] (l18) at (0.82*18,0) {18\\slh-dsa};
 \draw[decorate,decoration={brace,mirror,raise=5pt},black!45]
-  ($(l0.south west)+(-.05,0)$)--($(l3.south east)+(.05,0)$)
+  ($(l0.south west)+(.05,0)$)--($(l3.south east)+(-.05,0)$)
   node[midway,below=11pt,font=\scriptsize]{run 1};
 \draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
-  ($(l4.south west)+(-.05,0)$)--($(l7.south east)+(.05,0)$)
+  ($(l4.south west)+(.05,0)$)--($(l7.south east)+(-.05,0)$)
   node[midway,below=11pt,font=\scriptsize]{run 2};
 \draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
-  ($(l8.south west)+(-.05,0)$)--($(l11.south east)+(.05,0)$)
+  ($(l8.south west)+(.05,0)$)--($(l11.south east)+(-.05,0)$)
   node[midway,below=11pt,font=\scriptsize]{run 3};
-\node[draw,rounded corners,fill=softgray,minimum width=4.3cm,minimum height=.7cm,font=\small] (sth) at (6.7,1.65)
+\draw[decorate,decoration={brace,mirror,raise=5pt},deepblue]
-  {signed head: size 13, root \code{3488a2d0...}};
+  ($(l13.south west)+(.05,0)$)--($(l18.south east)+(-.05,0)$)
-\draw[arrow] (l12.north) -- (sth.south east);
+  node[midway,below=11pt,font=\scriptsize]{August 2026};
+\node[draw,rounded corners,fill=softgray,minimum width=5.9cm,minimum height=.85cm,align=center,font=\small] (sth) at (7.4,1.75)
+  {signed head: size 19, root \code{7ee23940...}\\dual-signed: Ed25519 $+$ SLH-DSA};
 \draw[arrow] (l6.north) -- (sth.south west);
+\draw[arrow] (l18.north) -- (sth.south east);
 \end{tikzpicture}
-\caption{The public 13-leaf deployment. Failure leaves are retained; entry 13
+\caption{The public nineteen-leaf deployment. Failure leaves are retained; leaf
-attests the accumulator corpus itself, scoped to the recursive model.}
+12 (the thirteenth entry) attests the accumulator corpus itself, scoped to the
+recursive model; leaves 13--16 re-attest the four forks at 44 certificates
+each; leaf 17 the hardened accumulator corpus; leaf 18 the SLH-DSA verify
+path. Heads are dual-signed from size 14 on.}
 \label{fig:deployment}
 \end{figure}
 
@@ -1191,11 +1260,11 @@ refinement from the deployed iterative consistency verifier remain outside the
 corpus.
 
 \begin{center}\small
-\begin{tabularx}{\textwidth}{@{}lXX@{}}
+\begin{tabularx}{\textwidth}{@{}l>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X@{}}
 \toprule
 Layer & Mechanized evidence & Explicit boundary \\
 \midrule
-Merkle definitions & MTH, Root, Path, recursive ConsRec & single SHA-256 boundary axiom \\
+Merkle definitions & $\MTH$, $\Root$, $\Path$, recursive $\ConsRec$ & single SHA-256 boundary axiom \\
 Inclusion & completeness and named collision extractor & collision resistance interpreted externally \\
 Consistency & recursive-model soundness and extractor & no general consistency-completeness theorem \\
 Pinning & per-step monotonicity and prefix correctness & signature layer and multi-step closure external \\
@@ -1274,7 +1343,7 @@ structure actually differs.
 
 \paragraph{Transparency.}
 Certificate Transparency introduced publicly auditable append-only logs for
-certificate issuance~\cite{ct1,ct2}; Crosby and Wallach developed efficient
+certificate issuance~\cite{ct1,ct2}; Crosby and Wallach built efficient
 tamper-evident history trees~\cite{crosby}; Dowling et al. formalized security
 notions for secure logging and CT~\cite{dghs} --- the games of
 \S\ref{sec:games} adapt that two-transcript style to replay attestation, with
@@ -1499,24 +1568,38 @@ Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
 
 \end{thebibliography}
 
+% Appendix policy (declared 2026-08-16): the appendix block starts on a
+% fresh page and then flows continuously -- no page breaks between
+% individual appendices. The claim matrix is one unbreakable tabularx.
+\clearpage
 \appendix
 
 \section{End-to-end claim matrix}\label{app:matrix}
 \begin{center}\small
-\begin{tabularx}{\textwidth}{@{}XXX@{}}
+\begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X@{}}
 \toprule
 Consumer conclusion & Established by & Remaining assumption \\
 \midrule
-Leaf has an authentic opening with a position-bound leaf value at index $m$ under head $h$ & inclusion proof and signed head & SHA-256 collision resistance; correct public key; EUF-CMA of the head signature \\
+Leaf has an authentic opening with a position-bound leaf value at index $m$ under head $h$ & inclusion proof and signed head & \mbox{SHA-256} collision resistance; correct public key; \mbox{EUF-CMA} of the head signature \\
+\addlinespace[3pt]
 Head root commits the published numbered leaf list & full-mirror recomputation (\code{verify.py --all}) & mirror availability and retention \\
-Head was authorized by the log identity & Ed25519 verification & correct key acquisition; EUF-CMA \\
+\addlinespace[3pt]
-New pinned head extends old pinned head & consistency proof & SHA-256 collision resistance; recursive-model soundness; authentic size/root pairing for deployment \\
+Head was authorized by the log identity & Ed25519 verification & correct key acquisition; \mbox{EUF-CMA} \\
-Equal-size unequal roots in one log context conflict & two valid signatures & correct public key; EUF-CMA; operationally, a retaining observer must compare the heads \\
+\addlinespace[3pt]
+New pinned head extends old pinned head & consistency proof & \mbox{SHA-256} collision resistance; recursive-model soundness; authentic size/root pairing for deployment \\
+\addlinespace[3pt]
+Equal-size unequal roots in one log context conflict & two valid signatures & correct public key; \mbox{EUF-CMA}; operationally, a retaining observer must compare the heads \\
+\addlinespace[3pt]
 Observed cone matches local boundary policy & exact set equality & semantic identity of named declarations \\
-Operator claims the kernel produced the observation & attestation signature and leaf inclusion & correct provider key; EUF-CMA \\
+\addlinespace[3pt]
+Operator claims the kernel produced the observation & attestation signature and leaf inclusion & correct provider key; \mbox{EUF-CMA} \\
+\addlinespace[3pt]
 Kernel actually produced the recorded observation & not cryptographically established; independently checkable by replay & operator and replay-pipeline honesty, or faithful independent replay \\
+\addlinespace[3pt]
 Recorded cone was produced by an audit that performed its checks & not established --- the audit driver is itself part of the replay pipeline & audit-gate integrity; adversarial gate self-tests reduce this exposure, they do not eliminate it \\
+\addlinespace[3pt]
 Source corresponds to deployed binary & not established & reproducible build and compiler assurance \\
+\addlinespace[3pt]
 Claimed signer implementation produced STH & not established & execution provenance \\
 \bottomrule
 \end{tabularx}
@@ -1537,7 +1620,6 @@ additionally relies on an unmechanized authentic-size/root invariant
 Its exclusions name SHA-256 collision resistance, deployed-verifier extensional
 equality, the signature/STH layer, and asymptotic cost claims.
 
-\clearpage
 \section{Compact receipt-verification core}\label{app:verifier}
 The following code is only the Merkle inclusion core. A complete receipt
 verifier must additionally validate the signed tree head, log identifier,
@@ -1600,4 +1682,43 @@ T4 & constructive decompression lift & \code{verify_accepts_iff_decompress} \\
 \end{tabular}
 \end{center}
 
+\section{SLH-DSA verification certificates and their cones}\label{app:slhtiers}
+
+Eleven certificates over the extracted SLH-DSA-SHA2-128s verify path
+(leaf 18). Beyond Lean's three foundational axioms, each certificate's
+exact axiom set consists of the uninterpreted hash oracles listed ---
+enforced by the audit as set equality in both directions, so the table is
+machine-checked, not documentation. The cone grows with the layer: pure
+digit/byte arithmetic rests on the kernel alone; the apex carries all
+five oracles.
+
+\begin{center}\small
+\begin{tabular}{@{}lll@{}}
+\toprule
+Layer & Lean declaration(s) & Oracles in the cone \\
+\midrule
+Digit/byte plumbing & \code{to_int_loop_eq}, \code{to_byte_loop_eq} & --- \\
+ & \code{wots_csum_loop_eq}, \code{base2b_outer_loop_eq} & \\
+Chain walk & \code{chain_free_loop_eq} & \code{f} \\
+WOTS pk recomputation & \code{wots_loop1_eq} & \code{f} \\
+XMSS Merkle ascent & \code{xmss_loop_eq} & \code{h} \\
+FORS inner ascent & \code{fors_inner_loop_eq} & \code{h} \\
+FORS outer loop & \code{fors_outer_loop_eq} & \code{f}, \code{h} \\
+Hypertree walk & \code{ht_loop_eq} & \code{f}, \code{h}, \code{t_l} \\
+Acceptance characterization & \code{slh_verify_128s_accepts_iff} & all five \\
+\bottomrule
+\end{tabular}
+\end{center}
+
+The oracles model the parameter set's SHA-256 hash-suite instantiations:
+\code{h_msg} (message digest), \code{f} (chain step and FORS leaf),
+\code{h} (Merkle node), \code{t_l} and \code{t_len} (the WOTS and FORS
+compressors --- two axioms over what is one Rust primitive, deliberately
+conservative, with the source's naming inversion against the standard's
+$T_\ell$/$T_k$ documented at the declarations). The acceptance
+characterization is a structural factorization, not a composition of the
+loop theorems: it would remain provable if any of the ten were deleted,
+and each loop certificate is meaningful exactly to the extent its
+reference fold has been read against FIPS~205.
+
 \end{document}

provider/README.md

@@ -2,7 +2,7 @@
 
 This nested project is a prototype third-party proof-checking service. It reuses host Lean/Aeneas infrastructure, runs portable PACTA replay/audit checks, and emits signed attestation certificates.
 
-It does not modify anything outside this repository. It may read configured toolchains such as `/Users/oho/GitClone/ClaudeCodeProjects/your-lean-project/aeneas-toolchain/env.sh`.
+It does not modify anything outside this repository. It may read configured toolchains such as `~/aeneas-toolchain/env.sh`.
 
 It can also maintain a local transparency log. The log is an RFC 9162-style Merkle accumulator over signed attestations. It emits Signed Tree Heads with Ed25519 today; heads are dual-sign capable with an additive SLH-DSA-SHA2-128s slot (proven verify path), and the ML-DSA/FIPS 204 slot stays honestly `not_configured`/`unavailable` — never silently filled. Agents that require both signatures must reject such receipts.
 

provider/src/pacta_provider/published_assets.py

@@ -498,7 +498,7 @@ This repository is the **git-published face** of a transparency log of
 formal-verification attestations: signed statements that the Lean 4 proofs
 of specific software, at specific git commits, re-check with exactly their
 documented assumptions. Its first twelve leaves attest four cryptographic
-Rust libraries (Ed25519 implementations); as of **entry 13 (2026-07-16)**
+Rust libraries (Ed25519 implementations); as of **its thirteenth entry (leaf index 12, 2026-07-16)**
 the log also attests **its own accumulator machinery** — a kernel-checked
 mechanization of the log's security analysis, so the log carries
 kernel-checked proofs *about the accumulator model* underlying its own
@@ -506,7 +506,7 @@ inclusion and consistency reasoning, as one of its own entries (subject
 [`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified);
 scoped to the mechanized model — it does not prove operator honesty,
 signing, or execution provenance). As of **2026-08** the log also attests
-the **SLH-DSA (FIPS 205) verify-path proofs**
+the **SLH-DSA (FIPS 205) verify-path proofs** (leaf 18)
 ([`fips205-slhdsa-verified`](https://github.com/saymrwulf/fips205-slhdsa-verified))
 and its heads carry an **additive post-quantum SLH-DSA-SHA2-128s signature**
 beside the required Ed25519 one. The current head is `latest-sth.json` —

provider/src/pacta_provider/web.py

@@ -46,7 +46,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
             if route in ("/", "/docs"):
                 self._send_html(docs_html)
             elif route in ("/paper", "/paper/ltl.pdf"):
-                # /paper serves the current paper only (v0.10, revised
+                # /paper serves the current paper only (v0.11, revised
                 # August 2026). Superseded drafts were retired from the
                 # site 2026-08-15; git history retains them.
                 body = paper_pdfs.get("current")
@@ -229,7 +229,7 @@ def serve(
         docs_html = render_docs(log, base_path)
     paper_dir = Path(__file__).resolve().parents[3] / "paper"
     variants = {
-        "current": paper_dir / "ltl.pdf",       # v0.10, revised August 2026
+        "current": paper_dir / "ltl.pdf",       # v0.11, revised August 2026
     }
     paper_pdfs = {name: p.read_bytes() for name, p in variants.items() if p.is_file()}
     handler = make_handler(log, base_path, docs_html, paper_pdfs)

provider/src/pacta_provider/webdocs.py

@@ -95,7 +95,7 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head
     root_x, root_y = positions[(len(levels) - 1, 0)]
     out.append(f'<rect x="{root_x-190}" y="{root_y-72}" width="380" height="34" rx="6" fill="#e2f2e9" stroke="#1e7f4f" stroke-width="1.6"/>')
     out.append(f'<text x="{root_x}" y="{root_y-58}" text-anchor="middle" fill="#1e7f4f" font-weight="bold">Signed Tree Head — {escape(head_label)}({root_hex[:12]}…)</text>')
-    out.append(f'<text x="{root_x}" y="{root_y-46}" text-anchor="middle" fill="#1e7f4f" font-size="9">signed by: {escape(signing_backend)} (the proof-attested library itself)</text>')
+    out.append(f'<text x="{root_x}" y="{root_y-46}" text-anchor="middle" fill="#1e7f4f" font-size="9">signed by: {escape(signing_backend)} (verify path attested; signing itself not proven)</text>')
     out.append(f'<line x1="{root_x}" y1="{root_y-38}" x2="{root_x}" y2="{root_y-15}" stroke="#1e7f4f" stroke-width="1.4"/>')
     out.append("</svg>")
     return "".join(out)
@@ -138,16 +138,16 @@ proof subject of leaf&nbsp;18.</p>
         slh_block = ""
     return f"""<div class="card">
 <p style="margin-top:0">This key is the <strong>sole cryptographic identity anchor</strong>: it
-authenticates that these statements were made by the operator. It does not, by itself, make
+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. Every tree head and attestation is
+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, and compare this copy byte-for-byte with the independently hosted
+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
-<a href="{mirror}/blob/main/provider.ed25519.pub">mirror copy</a>; they must be identical.</p>
+<a href="{mirror}/blob/main/provider.ed25519.pub">mirror copy</a>; they must be identical. The first fetch is trust-on-first-use; the two-host byte-comparison is what bounds it.</p>
 <pre style="margin-bottom:.4rem">{pem}</pre>
 <p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{escape(fingerprint)}</code>
 &nbsp;·&nbsp; raw: <a href="{base}/log-public-key"><code>{base or ''}/log-public-key</code></a>
-&nbsp;·&nbsp; <code>curl -s ltl.zkdefi.org/log-public-key</code></p>
+&nbsp;·&nbsp; <code>curl -s https://ltl.zkdefi.org/log-public-key</code></p>
 {slh_block}</div>"""
 
 
@@ -197,11 +197,10 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
 · <a href="https://zkdefi.com/">cv</a></p>
 <h1>LTL — the Lean Transparency Log</h1>
 <p class="tagline"><strong>One sentence:</strong> a public, append-only Merkle
-accumulator of <em>signed statements that the Lean&nbsp;4 formal proofs of specific
+accumulator (a hash tree that only ever grows) of <em>signed statements that the <a href="https://lean-lang.org">Lean&nbsp;4</a> formal proofs of specific
-cryptographic Rust libraries, at specific git commits, machine-re-check with exactly
+cryptographic Rust libraries, at specific git commits, re-check by machine with exactly
 their documented assumptions</em> — so that you can trust a proof result by checking
-<strong>one required signature (Ed25519; heads from tree&nbsp;14 add an additive post-quantum
+<strong>one required signature (Ed25519) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in
-SLH-DSA signature) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in
 milliseconds</strong>, instead of running a theorem prover for hours.</p>
 
 <h2>The trust anchor — pin this key</h2>
@@ -211,10 +210,10 @@ milliseconds</strong>, instead of running a theorem prover for hours.</p>
 {tree_svg}
 <p class="legend">
 <span><span class="sw" style="background:#e2f2e9;border:1px solid #1e7f4f"></span>verified attestation (all certificates proven, axiom cones boundary-exact)</span>
-<span><span class="sw" style="background:#f4f4f6;border:1px solid #8a93a0"></span>historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day</span>
+<span><span class="sw" style="background:#f4f4f6;border:1px solid #8a93a0"></span>historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves&nbsp;0–3: an early audit round that failed; leaves&nbsp;4–7 re-attest the same four libraries cleanly)</span>
 </p>
 <p class="muted">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
+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 <em>verify</em> 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','?')))})
@@ -237,12 +236,12 @@ identical.</td>
 <td><a href="{base}/log-public-key">this site</a> · <a href="{mirror}/blob/main/provider.ed25519.pub">mirror</a></td></tr>
 <tr><td><b>2</b></td><td><code>&lt;library&gt;.attestation.json</code></td>
 <td><strong>The claim.</strong> Which repo, which exact git commit, which theorems,
-which observed axiom cones, what machine protection — signed by the provider.</td>
+which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider.</td>
-<td>table above, or <a href="{mirror}">mirror</a> <code>entries/</code></td></tr>
+<td>table below, or <a href="{mirror}">mirror</a> <code>entries/</code></td></tr>
 <tr><td><b>3</b></td><td><code>&lt;library&gt;.receipt.json</code></td>
 <td><strong>The proof of inclusion.</strong> Binds artifact&nbsp;2 into the signed tree:
-leaf index, sibling hashes, the Signed Tree Head. ~25 lines of Python verify it (stdlib hashing; signature checks shell out to the <code>openssl</code> binary).</td>
+leaf index, sibling hashes, the Signed Tree Head (STH). A one-page Python core verifies it — printed as Appendix&nbsp;C of the paper; the shipped <code>verify.py</code> wraps that core with full fail-closed binding checks (stdlib hashing; signature checks shell out to the <code>openssl</code> binary).</td>
-<td>table above, or <a href="{mirror}">mirror</a> <code>receipts/</code></td></tr>
+<td>table below, or <a href="{mirror}">mirror</a> <code>receipts/</code></td></tr>
 <tr><td>+</td><td>the full mirror clone</td>
 <td><strong>Maximal benefit: become a witness.</strong> Every leaf + every signed head
 ever issued + <code>verify.py</code> (Python stdlib + the <code>openssl</code> binary for
@@ -257,17 +256,19 @@ consumers.)</td>
 <h2>Attested libraries</h2>
 <table><tr><th>component</th><th>artifact 2</th><th>artifact 3</th><th>status</th></tr>{rows}</table>
 
+<p class="muted">One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone).</p>
+
 <h2>Three ways to use it</h2>
 <div class="steps">
 <div class="card"><strong>Quick check</strong> (any machine, milliseconds): download
 artifacts 1–3, then<br>
 <code>pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub</code>
-<br><span class="muted">No Lean, no Rust, no account. Add <code>--sth-store pins.json</code> for split-view defense.</span></div>
+<br><span class="muted">No Lean, no Rust, no account. The <code>pacta</code> CLI ships in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a> (<code>pip install .</code> from a clone). Add <code>--sth-store pins.json</code> to remember every Signed Tree Head (STH) you accept — your defense against a split view (the operator showing different histories to different consumers).</span></div>
-<div class="card"><strong>Zero-install audit</strong>: <code>git clone {mirror} &amp;&amp; python3 verify.py --all</code>
+<div class="card"><strong>Zero-install audit</strong>: <code>git clone {mirror} &amp;&amp; cd lean-transparency-log &amp;&amp; python3 verify.py --all</code>
-<br><span class="muted">Standard-library Python only. You become a witness of the whole history.</span></div>
+<br><span class="muted">Standard-library Python plus the system <code>openssl</code> binary (signature checks fail closed without it). You become a witness of the whole history.</span></div>
 <div class="card"><strong>Autonomous agent</strong>: the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta</a>
 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
+(R0–R5, six named residual-risk classes) with policy-gated consequences, and optionally verifies every signature through
 the proof-attested Ed25519 code path itself (<code>--require-verified-verifier</code>).</div>
 </div>
 
@@ -290,19 +291,19 @@ view.</div>
 <div class="card"><span class="pill warn">does not mean</span> A verified binary. The
 proofs cover Rust <em>source</em>; 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
+build it yourself — compiler and build are declared trusted base (assumed, not proven)
-until the reproducible-builds program (R5) lands. Every attestation carries its full
+until the reproducible-builds program lands and retires risk class R5. Every attestation carries its full
-residual-risk list. Honesty about the boundary is the product.</div>
+residual-risk list — the enumerated assumptions inside its <code>attestation.json</code>. Honesty about the boundary is the product.</div>
 
 <h2>You hold the ruler</h2>
 <div class="card">The list of assumptions a certificate is <em>allowed</em> to rest on
 is not something this site hands you at verification time — it is a
 <strong>requirements card</strong> that lives in <em>your</em> tooling, on
 <em>your</em> 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 —
+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 <em>observed</em> axiom list against <em>your</em> card, name by name.
+attestation's <em>observed</em> axiom list (its cone) against <em>your</em> card, name by name.
 The operator is trusted to copy down what the proof kernel printed — never to
 interpret it.</div>
 <div class="card">A card you write yourself will match this log's supply
@@ -312,13 +313,13 @@ shrunk until every remaining axiom justifies its existence. If your card is
 negotiate — the gap is itemized, never blurred, and you have three honest options:
 accept a <em>named</em> line item, walk away, or prove the missing piece and enter it
 into this same log. <strong>If your ruler is stricter than our supply, your ruler is
-our roadmap.</strong> (The full walk-through is lecture&nbsp;11 in the
+our roadmap.</strong> (The full walk-through is lecture&nbsp;11 of the Jupyter course in the
-<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">course</a>.)</div>
+<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repo</a>.)</div>
 
 <h2>The paper</h2>
 <div class="card"><a href="{base}/paper"><strong>Accountable Distribution of Machine-Checked
 Correctness Evidence: A Transparency Model and the Lean Transparency Log</strong></a>
-(PDF, 23 pages, <strong>v0.10 — revised August&nbsp;2026</strong>; the version is printed on the
+(PDF, 25 pages, <strong>v0.11 — revised August&nbsp;2026</strong>; 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
@@ -328,16 +329,18 @@ 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&nbsp;9162 conjunct (Step&nbsp;7's <code>sn&nbsp;=&nbsp;0</code>),
-zero divergences after the one-line restoration, confirmed by a three-way regression.</div>
+zero divergences after the one-line restoration, confirmed by a three-way regression.
+New in v0.11: the deployment evaluated to its current nineteen-leaf, dual-signed state, an
+instantiation section for the SLH-DSA (FIPS&nbsp;205) verify path — eleven certificates,
+five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the
+Ed25519 tiers.</div>
 
-<div class="card"><strong>The paper's snapshot vs. today's log.</strong> The paper analyses
+<div class="card"><strong>Paper and log, one story.</strong> Since v0.11 the paper
-the log's 16&nbsp;July&nbsp;2026 snapshot — thirteen leaves, still leaves&nbsp;0–12 today,
+describes this deployment as it runs — nineteen leaves, dual-signed heads, the
-byte-identical, its pinned head still head&nbsp;#5 of <code>sth-history.jsonl</code>. Everything
+post-quantum verify path as leaf&nbsp;18 with its own certificate appendix. The log is
-since is additive: the four Ed25519 corpora re-attested at 44 certificates each
+append-only and keeps growing past any paper revision; every number the paper states
-(leaves&nbsp;13–16), the accumulator's hardened model (leaf&nbsp;17), the first post-quantum
+stays checkable against the retained history: <code>python3 verify.py --all</code>
-subject (leaf&nbsp;18), and dual-signed heads from tree&nbsp;14 on.
+re-verifies all of it, paper-era and after, from a clone of the mirror.</div>
-<code>python3 verify.py --all</code> re-verifies the paper-era prefix together with everything
-after it.</div>
 
 <p class="muted">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 <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.</p>

tests/test_web_and_witness.py

@@ -159,3 +159,25 @@ def test_standalone_verify_py_runs(tmp_path):
     assert result.returncode == 0, result.stdout + result.stderr
     # hardened verifier: full mode (signatures verified) must report exactly this
     assert "RESULT: OK [full]" in result.stdout
+
+
+def test_webdocs_source_carries_no_stale_paper_claims():
+    # Regression for the 2026-08-16 operator finding: the paper card said
+    # "23 pages" and the July-snapshot card survived a silently failed
+    # replace (an invisible NBSP defeated the pattern). Guard the shipped
+    # STRINGS, not just version markers.
+    from pathlib import Path
+
+    source = Path(__file__).resolve().parents[1] / "provider" / "src" / "pacta_provider" / "webdocs.py"
+    text = source.read_text(encoding="utf-8")
+    for stale in ("snapshot", "thirteen leaves", "16 July", "16 July",
+                  "16\xa0July", "v0.9", "v0.10", "23 pages"):
+        assert stale not in text, f"stale marker {stale!r} in webdocs"
+    # printed commands must work as printed: curl needs the scheme
+    # (http->https redirect yields empty output), the clone one-liner
+    # needs the cd into the cloned directory
+    assert "curl -s ltl.zkdefi.org" not in text
+    assert "cd lean-transparency-log" in text
+    # first-use glosses the page promised: STH and axiom cones
+    assert "Signed Tree Head (STH)" in text
+    assert "axiom cones (the exact set of assumptions" in text