docs: estate-wide consistency pass (workflow audit, 36 findings, all verified before fixing)

Nine parallel readers audited every doc against measured ground truth; every
finding was re-verified against the file before any edit, and the sweep fixed
by PROPERTY, not by flag — wording the readers caught in one repo was hunted
in all siblings (the two-button README sentence existed in all four forks,
not the three flagged; likewise the cone-overclaim in TRUSTED-BASE item 1).

This repo: see the diff. Records were not rewritten; clarifications are
dated. Doc-only except where noted in the estate summary; every gated doc
change was followed by a green button run.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

ESTATE.md

@@ -23,10 +23,10 @@ flowchart LR
     s6["fips205-source"]
   end
   subgraph V["VERIFIED SUBJECTS"]
-    d["dalek-ed25519-verified<br/>16 certs · leaf 8 · signer source"]
-    a["anza-ed25519-verified<br/>16 certs · leaf 9"]
-    r["risc0-ed25519-verified<br/>16 certs · leaf 10"]
-    b["betrusted-ed25519-verified<br/>16 certs · leaf 11"]
+    d["dalek-ed25519-verified<br/>44 certs today · attested at 16 (leaf 8 · signer source)"]
+    a["anza-ed25519-verified<br/>44 certs today · attested at 16 (leaf 9)"]
+    r["risc0-ed25519-verified<br/>44 certs today · attested at 16 (leaf 10)"]
+    b["betrusted-ed25519-verified<br/>44 certs today · attested at 16 (leaf 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"]
     c["ltl-accumulator-verified<br/>61 certs · entry-13 subject · frozen 172a1d0"]
@@ -119,8 +119,8 @@ deployed verifier; see the corpus KNOWN-GAPS ledger).
 | Repository | Lane | Role | Mutability |
 |---|---|---|---|
 | `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 `5dca0db` — single deviation: upstream CI workflows stripped, documented in-commit | pinned; moves only for transparent, individually-justified Aeneas-compat patches (nothing proposed upstream) |
-| `dalek-` / `anza-` / `risc0-` / `betrusted-ed25519-verified` | subject | Rust source + Lean proofs; 16 certs each; attested (leaves 8–11, generations at 0–7) | frozen at attested commits; branch moves only for docs |
+| `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 |
 | `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 |
 | `ltl-accumulator-verified` | subject | 61-cert corpus about the log's accumulator model; **entry-13 subject**, frozen `172a1d0` | frozen; doc-only commits allowed |

README.md

@@ -207,6 +207,7 @@ 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 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),
@@ -303,7 +304,7 @@ This is the intended trust transformation: local agents can avoid constructing t
 ## Real Evidence (shipped)
 
 `evidence/` contains signed, transparency-logged attestations from a REAL
-guarded replay of all four verified repositories: 16/16 certificates proven
+guarded replay of all four verified repositories at the 2026-07 attestation generation: 16/16 certificates proven
 per fork with boundary-exact axiom cones, pinned to exact repo commits,
 machine-protected by `lean-guard` throughout (~30 min of Lean kernel
 re-checking per fork, done ONCE - verifying the signature + inclusion
@@ -358,7 +359,7 @@ pacta dogfood-status
 pacta receipt-verify ... --require-verified-verifier   # fail closed unless the proven path ran
 ```
 
-The backend that actually verified each signature (`verified-dalek-serial` or the `openssl` fallback) is recorded in receipts' signature statuses and attestation evidence; the fallback is never silent. A provenance sidecar records the source commit, backend cfg, and the honest coverage note (the certificates cover the extraction image of this verify path; SHA-512 and the wire glue remain the documented trusted base). ML-DSA is deliberately NOT dogfooded: no proven implementation exists, so the slot stays fail-closed - the hybrid-PQC posture is one proven-classical signature plus one required-but-honest post-quantum slot.
+The backend that actually verified each signature (`verified-dalek-serial` or the `openssl` fallback) is recorded in receipts' signature statuses and attestation evidence; the fallback is never silent. A provenance sidecar records the source commit, backend cfg, and the honest coverage note (the certificates cover the extraction image of this verify path; SHA-512 and the wire glue remain the documented trusted base). ML-DSA is deliberately NOT dogfooded: no proven implementation exists, so the slot stays fail-closed - the ML-DSA slot stays required-but-honest, while SLH-DSA now provides a proven-verify post-quantum capability (signing itself remains trusted base, as for Ed25519).
 
 ## Truth Boundary
 

WALLET.md

@@ -46,7 +46,8 @@ into an alarm with a machine-checked guarantee behind it.
 | SHA-512 | opaque oracle inside the theorems |
 | wire parsers | outcomes are hypotheses |
 | reproducible builds, side channels | not claimed (that is R5) |
-| ML-DSA / PQC | fail-closed: no proven implementation exists |
+| ML-DSA | fail-closed: no proven implementation exists; slot stays `not_configured` |
+| SLH-DSA | verify path PROVEN (fips205-slhdsa-verified, 11 certs); signing deterministic + parameter-locked, trusted base |
 
 The asymmetry is the point: warden is strongest exactly where it matters
 most for custody — deciding whether an inbound authorization is real — and

docs/agent-native.md

@@ -47,7 +47,9 @@ cover the **verification** path. Signing is declared trusted base
 (mitigated by the firewall below), SHA-512 is an oracle, wire parsing
 is hypothesis, side channels and reproducible builds are the R5
 frontier. ML-DSA remains fail-closed: no proven implementation exists,
-so the PQC slot reports `unavailable` rather than pretending.
+so that slot reports `unavailable` rather than pretending. (Update
+2026-08: an SLH-DSA slot with a proven verify path now exists beside it —
+the PQC story is no longer a single unavailable slot.)
 
 ## The four semantic edges (why divergence needs a taxonomy)
 

docs/runbook-latch.md

@@ -35,7 +35,7 @@ hash at the moment of divergence. That table is your suspect list.
 
 1. **A corrupted/updated member binary.** Compare each member's current
    hash against the capsule:
-   `sha256sum dogfood/state/quorum/pacta-verify-*` vs
+   `shasum -a 256 dogfood/state/quorum/pacta-verify-*` (GNU: `sha256sum`) vs
    `capsule.json` → `members[].binary_sha256`. A mismatch on exactly the
    dissenting member is the common benign case (a rebuild happened);
    a mismatch you cannot explain is not benign.

llms.txt

@@ -26,7 +26,7 @@
 
 warden speaks MCP over stdio: `pacta wallet mcp --wallet <dir>`. Tools:
 `wallet_status`, `verify_inbound`, `request_signature`, `custody_card`,
-`posture_challenge`, `list_incidents`, `explain_refusal`. Errors are
+`posture_challenge`, `list_incidents`, `explain_refusal`, `airgap_pending`. Errors are
 structured objects (code / missing / remediation). The custody card at
 `.well-known/custody-card.json` is self-proving: it embeds transparency-log
 inclusion proofs a counterparty recomputes rather than trusts.
@@ -36,4 +36,4 @@ inclusion proofs a counterparty recomputes rather than trusts.
 Verification paths are certificate-covered; signing is trusted base (the
 attested artifact, fenced by the firewall). SHA-512 is an opaque oracle;
 wire parsers are hypotheses; reproducible builds and side channels are R5,
-not claimed; ML-DSA (PQC) fails closed — no proven implementation exists.
+not claimed; ML-DSA fails closed — no proven implementation exists; the SLH-DSA verify path IS proven (verify only; signing remains trusted base).

provider/README.md

@@ -4,7 +4,7 @@ This nested project is a prototype third-party proof-checking service. It reuses
 
 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 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 and records an ML-DSA/FIPS 204 signature slot as `unavailable` unless a real backend is present. Agents that require both signatures must reject such receipts.
+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.
 
 ## Commands