site: the homepage tells the truth about tree 19 — dual anchors, honest tooling, and a note to the paper's readers

The estate doc audit scoped itself to *.md and missed the text a site visitor
actually reads: the string constants in webdocs.py. Fixed here, verified by
RENDERING the page from the live 19-leaf state and checking each block:

- The SVG head label reads "Ed25519 + SLH-DSA" when the live head is
  dual-signed, "Ed25519" when it is not — computed, not asserted.
- The trust-anchor card now carries BOTH keys the same way: full PEM,
  SHA-256 fingerprint, raw endpoint (/v1/log-slhdsa-public-key), mirror
  comparison link. The Ed25519 key stays the required anchor; the SLH-DSA
  key is the additive post-quantum one, and the card says whose proof
  subject its verify path is (leaf 18).
- The registered homepage overclaim (register: homepage-stdlib-claim) is
  closed: "stdlib-only" wording replaced with the truth — stdlib hashing,
  signature checks shell out to the openssl binary, fails closed without.
- "one signature and ~N hashes" became "one REQUIRED signature (Ed25519;
  heads from tree 14 add an additive post-quantum SLH-DSA signature)".
- The paper card is reframed (frozen under review, describes the 16 July
  snapshot, "then-thirteen-leaf") and followed by a new reader-guidance
  card (operator-ordered): the paper-era prefix is unchanged inside the
  live history — leaves 0-12 byte-identical, the paper's head still
  head #5 of sth-history — verify.py --all checks both eras at once; the
  advances are additive (44-cert re-attestations, leaf 18, dual-signed
  heads, ABSENT on older heads by design); and the 3,867 divergence the
  paper honestly reports has since been CLOSED (sn==0 fix, 2026-07-23,
  pinned count now 0) — both the divergence and the fix are part of the
  retained record.

Layout fact the render surfaced: the served log dir must contain the .pub
files (that is what /v1/log-public-key reads); the SLH-DSA pub joins the
Ed25519 one there. Suite 152/0/0.

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

.gitignore

@@ -23,3 +23,6 @@ dogfood/quorum/*/Cargo.lock
 dogfood/quorum/*/target/
 dogfood/state/quorum/
 paper/eprint-submission.md
+dogfood/quorum/.build-slhdsa/
+dogfood/quorum/verify-slhdsa/Cargo.toml
+dogfood/quorum/verify-slhdsa/Cargo.lock

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.

dogfood/quorum/build-verify-slhdsa.sh

@@ -0,0 +1,102 @@
+#!/usr/bin/env bash
+# Build pacta-verify-slhdsa from the PINNED proven source.
+#
+# The pinned checkout is never modified. This script exports the pinned commit
+# into a scratch tree, applies expose-mono.patch there, builds against that, and
+# records exactly what went in. If the pinned checkout is dirty, or is not at
+# the commit the attestation names, it refuses: a quorum member built from a
+# tree nobody can identify is a quorum member that proves nothing.
+set -euo pipefail
+
+HERE="$(cd "$(dirname "$0")" && pwd)"
+SRC="${FIPS205_SOURCE:-$HOME/GitClone/FormalVerification/sources/fips205-source}"
+PIN="${FIPS205_PIN:-a3ce8e8}"
+BUILD="${BUILD_DIR:-$HERE/.build-slhdsa}"
+OUT="$HERE/verify-slhdsa/target/release/pacta-verify-slhdsa"
+
+echo "=== pacta-verify-slhdsa: build from the proven source ==="
+
+[ -d "$SRC/.git" ] || { echo "FATAL: '$SRC' is not a git checkout of fips205-source."; exit 2; }
+HEAD_SHA="$(git -C "$SRC" rev-parse HEAD)"
+case "$HEAD_SHA" in
+  "$PIN"*) ;;
+  *) echo "FATAL: pinned source is at ${HEAD_SHA:0:8}, expected $PIN."
+     echo "  The certificates cover $PIN. Building a 'proven' verifier from any"
+     echo "  other tree would be a claim nobody can check."; exit 1;;
+esac
+if [ -n "$(git -C "$SRC" status --porcelain)" ]; then
+  echo "FATAL: the pinned source has uncommitted changes:"
+  git -C "$SRC" status --porcelain | sed 's/^/    /'
+  echo "  Refusing: the binary must correspond to a nameable tree."; exit 1
+fi
+echo "  pinned source  $SRC @ ${HEAD_SHA:0:8} (clean)"
+
+# Export the pinned commit, never a working copy.
+rm -rf "$BUILD"; mkdir -p "$BUILD"
+git -C "$SRC" archive --format=tar "$HEAD_SHA" | tar -x -C "$BUILD"
+echo "  exported       $(find "$BUILD" -type f | wc -l) files from $PIN"
+
+# --- the two changes, applied verbatim and then VERIFIED to be present -------
+LIB="$BUILD/src/lib.rs"; VM="$BUILD/src/verify_mono.rs"
+grep -q '^mod verify_mono;' "$LIB" || { echo "FATAL: 'mod verify_mono;' not found in lib.rs — the source moved."; exit 1; }
+# The crate is `#![deny(missing_docs)]`, so a module cannot become public
+# without a doc comment. The comment is part of the visibility change, not an
+# extra edit: `pub mod` alone does not compile here.
+sed -i 's|^mod verify_mono;|/// Aeneas-compat monomorphic verify path: the extraction root the eleven\n/// certificates cover (apex `fips205.slh_verify_128s_accepts_iff`). Public only\n/// so a quorum binary can call the proven function; see expose-mono.patch.\npub mod verify_mono;|' "$LIB"
+
+cat >> "$VM" <<'RUST'
+
+/// Byte-level entry to the PROVEN root, for out-of-crate callers.
+///
+/// Assembles arguments only; the body is the crate's own test helper
+/// `internal_inputs` followed by the call. `mprime` is FIPS 205's M' and is
+/// built by the CALLER — its construction is outside every certificate
+/// (TRUSTED-BASE item 10), which is why it is a parameter and not computed
+/// here.
+pub fn verify_mono_bytes(mprime: &[u8], sig_bytes: &[u8; 7856], pk_bytes: &[u8; 32]) -> bool {
+    let mut pk_seed = [0u8; 16];
+    let mut pk_root = [0u8; 16];
+    pk_seed.copy_from_slice(&pk_bytes[0..16]);
+    pk_root.copy_from_slice(&pk_bytes[16..32]);
+    let pk = SlhPublicKey { pk_seed, pk_root };
+    let sig = SlhDsaSig::<12, 7, 9, 14, 35, 16>::deserialize(sig_bytes);
+    slh_verify_128s(mprime, &sig, &pk)
+}
+RUST
+
+# The extraction root must be untouched. Compare it against the pinned tree.
+if ! diff <(git -C "$SRC" show "$HEAD_SHA:src/verify_mono.rs") \
+          <(head -n "$(git -C "$SRC" show "$HEAD_SHA:src/verify_mono.rs" | wc -l)" "$VM") > /dev/null; then
+  echo "FATAL: the patch altered existing lines of verify_mono.rs, not just appended."
+  exit 1
+fi
+echo "  patched        lib.rs visibility + verify_mono_bytes appended (existing lines unchanged)"
+
+# --- render Cargo.toml from the template ------------------------------------
+sed "s|{{SOURCE}}|$BUILD|g" "$HERE/verify-slhdsa/Cargo.toml.template" > "$HERE/verify-slhdsa/Cargo.toml"
+
+echo "  building..."
+( cd "$HERE/verify-slhdsa" && cargo build --release 2>&1 | tail -5 | sed 's/^/    /' )
+
+[ -x "$OUT" ] || { echo "FATAL: build produced no binary at $OUT"; exit 1; }
+
+cat > "$HERE/verify-slhdsa/target/release/pacta-verify-slhdsa.provenance.json" <<JSON
+{
+  "binary_sha256": "$(sha256sum "$OUT" | cut -d' ' -f1)",
+  "source_repo": "fips205-source",
+  "source_commit": "$HEAD_SHA",
+  "patch": "expose-mono.patch",
+  "patch_sha256": "$(sha256sum "$HERE/verify-slhdsa/expose-mono.patch" | cut -d' ' -f1)",
+  "main_sha256": "$(sha256sum "$HERE/verify-slhdsa/src/main.rs" | cut -d' ' -f1)",
+  "proven_root": "slh_verify_128s",
+  "parameter_set": "SLH-DSA-SHA2-128s",
+  "certificates": 11,
+  "apex": "fips205.slh_verify_128s_accepts_iff",
+  "not_covered": "M-prime assembly (domain separator, context length), hex/file IO, and the compiler. Signing and keygen are out of scope entirely.",
+  "rustc": "$(rustc --version)"
+}
+JSON
+
+echo "  binary         $OUT"
+echo "                 sha256 $(sha256sum "$OUT" | cut -c1-16)…"
+echo "  provenance     written beside the binary"

dogfood/quorum/verify-slhdsa/Cargo.toml.template

@@ -0,0 +1,13 @@
+# Rendered by build-verify-slhdsa.sh — {{SOURCE}} is replaced with the exported
+# copy of the PINNED proven source plus expose-mono.patch. Committed as a
+# template so the repo never hardcodes a machine path.
+[package]
+name = "pacta-verify-slhdsa"
+version = "0.1.0"
+edition = "2021"
+publish = false
+
+[dependencies]
+fips205 = { path = "{{SOURCE}}", default-features = false, features = ["slh_dsa_sha2_128s"] }
+
+[workspace]

dogfood/quorum/verify-slhdsa/expose-mono.patch

@@ -0,0 +1,49 @@
+Expose the proven verify root so a quorum binary can call it.
+
+APPLIED TO A COPY of fips205-source at the pinned commit, never to the pinned
+checkout itself. Two hunks, and the reason each is the smallest possible:
+
+  1. `mod verify_mono;` -> `pub mod verify_mono;`
+     A visibility keyword. Rust's `src/bin/` and `examples/` targets are
+     SEPARATE crates, so neither can reach a `pub(crate)` item; the module has
+     to be public for any binary to call into it at all.
+
+  2. A new `verify_mono_bytes` function, appended.
+     It only assembles arguments: split the 32-byte public key into pk_seed and
+     pk_root, deserialize the 7856-byte signature, call `slh_verify_128s`. The
+     body is copied from the crate's OWN test helper `internal_inputs`, so the
+     conversion is the one the crate already trusts rather than one invented
+     here. Exposing the argument types and their fields instead would have
+     meant four more visibility changes across two files.
+
+WHAT THIS DOES NOT CHANGE. No existing line's semantics. The extraction root
+`slh_verify_128s` is untouched -- same body, same callees. Module visibility and
+an added sibling function do not alter the MIR of an existing function, so the
+code the certificates cover compiles to what it compiled to before. What IS
+true and must be said: the binary is built from `pinned commit + this patch`,
+not from the pinned commit alone, and the diff below is the whole of the
+difference.
+
+--- a/src/lib.rs
++++ b/src/lib.rs
+@@
+-mod verify_mono; // Aeneas-compat monomorphic verify path (formal-verification campaign; additive)
++pub mod verify_mono; // Aeneas-compat monomorphic verify path (formal-verification campaign; additive)
+
+--- a/src/verify_mono.rs
++++ b/src/verify_mono.rs
+@@ (appended after slh_verify_128s)
++/// Byte-level entry to the PROVEN root, for out-of-crate callers.
++///
++/// Assembles arguments only. `mprime` is FIPS 205's M' and is built by the
++/// CALLER -- its construction is outside every certificate (TRUSTED-BASE item
++/// 10), which is exactly why it is a parameter here and not computed inside.
++pub fn verify_mono_bytes(mprime: &[u8], sig_bytes: &[u8; 7856], pk_bytes: &[u8; 32]) -> bool {
++    let mut pk_seed = [0u8; 16];
++    let mut pk_root = [0u8; 16];
++    pk_seed.copy_from_slice(&pk_bytes[0..16]);
++    pk_root.copy_from_slice(&pk_bytes[16..32]);
++    let pk = SlhPublicKey { pk_seed, pk_root };
++    let sig = SlhDsaSig::<12, 7, 9, 14, 35, 16>::deserialize(sig_bytes);
++    slh_verify_128s(mprime, &sig, &pk)
++}

dogfood/quorum/verify-slhdsa/src/main.rs

@@ -0,0 +1,101 @@
+//! warden quorum member: SLH-DSA-SHA2-128s, the Lean-proven verify path.
+//!
+//! Built against a copy of the PINNED proven source (`fips205-source` at the
+//! commit named in the build provenance sidecar) plus `expose-mono.patch`,
+//! which adds a visibility keyword and an argument-assembly function and
+//! changes no existing line's semantics.
+//!
+//! The function this calls, `slh_verify_128s`, is the extraction root the
+//! eleven certificates cover, apex `fips205.slh_verify_128s_accepts_iff`.
+//! Verify-only on purpose: quorum members judge, they never sign.
+//!
+//! TWO THINGS THIS BINARY DOES THAT NO CERTIFICATE COVERS, stated here because
+//! a reader of the output cannot see them:
+//!
+//!   * It assembles M'. FIPS 205 hashes M' = toByte(0,1) ‖ toByte(|ctx|,1) ‖
+//!     ctx ‖ M, and Algorithm 20's input is already M'. Everything above the
+//!     extraction root -- including that leading domain-separator byte, the one
+//!     thing distinguishing the pure variant from prehash -- is outside every
+//!     proof (TRUSTED-BASE item 10). This binary implements the PURE variant
+//!     with EMPTY context, i.e. M' = 0x00 ‖ 0x00 ‖ payload, and refuses to
+//!     guess at anything else.
+//!   * It parses hex and reads a file.
+//!
+//! Usage: <pubkey-hex-32B> <sig-hex-7856B> <payload-file>
+//! stdout OK / INVALID; exit 0 = accept, 1 = reject, 2 = input error.
+
+use std::process::ExitCode;
+
+const SIG_LEN: usize = 7856;
+const PK_LEN: usize = 32;
+
+fn hex_decode(s: &str) -> Result<Vec<u8>, String> {
+    if s.len() % 2 != 0 {
+        return Err("odd-length hex".into());
+    }
+    (0..s.len() / 2)
+        .map(|i| u8::from_str_radix(&s[2 * i..2 * i + 2], 16).map_err(|e| e.to_string()))
+        .collect()
+}
+
+fn main() -> ExitCode {
+    let args: Vec<String> = std::env::args().collect();
+    if args.len() != 4 {
+        eprintln!("usage: {} <pubkey-hex-32B> <sig-hex-7856B> <payload-file>", args[0]);
+        return ExitCode::from(2);
+    }
+
+    let pk_bytes = match hex_decode(&args[1]) {
+        Ok(b) if b.len() == PK_LEN => b,
+        Ok(b) => {
+            eprintln!("error: public key must be {PK_LEN} bytes, got {}", b.len());
+            return ExitCode::from(2);
+        }
+        Err(e) => {
+            eprintln!("error: public key hex: {e}");
+            return ExitCode::from(2);
+        }
+    };
+    let sig_bytes = match hex_decode(&args[2]) {
+        Ok(b) if b.len() == SIG_LEN => b,
+        Ok(b) => {
+            // Size is part of the parameter set. A 7856-byte signature is
+            // SLH-DSA-SHA2-128s; anything else is a DIFFERENT parameter set and
+            // outside every certificate this binary exists to exercise. Refuse
+            // rather than attempt it.
+            eprintln!("error: signature must be {SIG_LEN} bytes (SLH-DSA-SHA2-128s), got {}", b.len());
+            return ExitCode::from(2);
+        }
+        Err(e) => {
+            eprintln!("error: signature hex: {e}");
+            return ExitCode::from(2);
+        }
+    };
+    let payload = match std::fs::read(&args[3]) {
+        Ok(p) => p,
+        Err(e) => {
+            eprintln!("error: cannot read payload file {}: {e}", args[3]);
+            return ExitCode::from(2);
+        }
+    };
+
+    // M' for the PURE variant with empty context: two length/domain bytes then
+    // the message. Built here, not proven anywhere.
+    let mut mprime = Vec::with_capacity(payload.len() + 2);
+    mprime.push(0u8); // domain separator: 0 = pure, 1 = prehash
+    mprime.push(0u8); // |ctx| = 0
+    mprime.extend_from_slice(&payload);
+
+    let mut sig_arr = [0u8; SIG_LEN];
+    sig_arr.copy_from_slice(&sig_bytes);
+    let mut pk_arr = [0u8; PK_LEN];
+    pk_arr.copy_from_slice(&pk_bytes);
+
+    if fips205::verify_mono::verify_mono_bytes(&mprime, &sig_arr, &pk_arr) {
+        println!("OK");
+        ExitCode::from(0)
+    } else {
+        println!("INVALID");
+        ExitCode::from(1)
+    }
+}

examples/repos.yaml

@@ -16,6 +16,86 @@ repos:
       - compiler correctness
       - SIMD/AVX/accelerator paths
 
+    # certificates + imports MEASURED from the two buttons (CERTS arrays;
+    # apex recovered the way Phase 3c itself recovers it). replay_exclude:
+    # the button-owned audit instruments the replay does not compile —
+    # disclosed per-leaf in replay.instruments_excluded.
+    certificates:
+      - CurveFieldProofs.fieldImplementation
+      - CurveFieldProofs.edwardsImplementation
+      - CurveFieldProofs.naf_table_spec
+      - CurveFieldProofs.naf_select_spec
+      - CurveFieldProofs.proj_double_law
+      - CurveFieldProofs.compl_as_projective_law
+      - CurveFieldProofs.dsm_step_p_law
+      - CurveFieldProofs.dsm_step_b_law
+      - CurveFieldProofs.dsm_loop_spec
+      - CurveFieldProofs.naf_load_spec
+      - CurveFieldProofs.naf_exit
+      - CurveFieldProofs.naf_digit_loop_spec
+      - CurveFieldProofs.non_adjacent_form_spec
+      - CurveFieldProofs.run_basepoint
+      - CurveFieldProofs.vartime_double_base_mul_spec
+      - CurveFieldProofs.verify_loop_full
+      - CurveFieldProofs.to_bytes_spec
+      - CurveFieldProofs.ed_compress_spec
+      - ScalarProofs.from_bytes_mod_order_wide_spec
+      - CurveFieldProofs.vartime_dsm_basepoint_spec
+      - CurveFieldProofs.enc_point_inj
+      - CurveFieldProofs.pow_p58_spec
+      - CurveFieldProofs.fe_ct_eq_spec
+      - CurveFieldProofs.sqrt_core
+      - CurveFieldProofs.sqrt_ratio_i_sq_spec
+      - CurveFieldProofs.from_bytes_spec
+      - CurveFieldProofs.decompress_of_canonical
+      - CurveFieldProofs.verify_accepts_iff
+      - CurveFieldProofs.verify_accepts_iff_decompress
+      - CurveFieldProofs.verify_accepts_iff_point
+      - CurveFieldProofs.verify_accepts_iff_point_eq
+      - ScalarProofs.L_val
+      - ScalarProofs.sub_loop_spec
+      - ScalarProofs.cond_add_l_one_spec
+      - ScalarProofs.sub_val_spec
+      - ScalarProofs.add_val_spec
+      - ScalarProofs.mul_internal_spec
+      - ScalarProofs.part1_spec
+      - ScalarProofs.montgomery_reduce_spec
+      - ScalarProofs.mul_spec
+      - ScalarProofs.scalarImplementation
+      - ScalarProofs.montgomery_mul_spec
+      - ScalarProofs.bytes_unpack_spec
+      - ScalarProofs.from_bytes_wide_spec
+    axiom_imports:
+      - Proofs.FieldMain
+      - Proofs.EdMain
+      - Proofs.ScalarMain
+      - Proofs.ToBytesSpec
+      - Proofs.CompressSpec
+      - Proofs.ScalarPackSpec
+      - Proofs.DsmMulSpec
+      - Proofs.SigApexSpec
+      - Proofs.PointLiftSpec
+      - Proofs.PointEqSpec
+      - Proofs.DecompressSpec
+      - Proofs.FromBytesSpec
+      - Proofs.DecompressMain
+      - Proofs.ScalarDenote
+      - Proofs.ScalarLoop
+      - Proofs.ScalarSubSpec
+      - Proofs.ScalarAddSpec
+      - Proofs.ScalarMulSpec
+      - Proofs.ScalarMontSpec
+      - Proofs.ScalarReduceSpec
+      - Proofs.ScalarFullMulSpec
+      - Proofs.ScalarWideSpec
+      - Proofs.ScalarBytesSpec
+      - Proofs.ScalarUnpackSpec
+      - Proofs.ScalarFromBytesSpec
+    replay_exclude:
+      - "Proofs/Audit.lean"
+      - "Proofs/ScalarAudit.lean"
+      - "Proofs/AxiomCheck.lean"
+      - "Proofs/Inventory*.lean"
   - name: anza-ed25519-verified
     url: https://github.com/saymrwulf/anza-ed25519-verified.git
     kind: ed25519
@@ -32,6 +112,86 @@ repos:
       - the default HEEA/Zebra verify() path
       - accelerator paths
 
+    # certificates + imports MEASURED from the two buttons (CERTS arrays;
+    # apex recovered the way Phase 3c itself recovers it). replay_exclude:
+    # the button-owned audit instruments the replay does not compile —
+    # disclosed per-leaf in replay.instruments_excluded.
+    certificates:
+      - CurveFieldProofs.fieldImplementation
+      - CurveFieldProofs.edwardsImplementation
+      - CurveFieldProofs.naf_table_spec
+      - CurveFieldProofs.naf_select_spec
+      - CurveFieldProofs.proj_double_law
+      - CurveFieldProofs.compl_as_projective_law
+      - CurveFieldProofs.dsm_step_p_law
+      - CurveFieldProofs.dsm_step_b_law
+      - CurveFieldProofs.dsm_loop_spec
+      - CurveFieldProofs.naf_load_spec
+      - CurveFieldProofs.naf_exit
+      - CurveFieldProofs.naf_digit_loop_spec
+      - CurveFieldProofs.non_adjacent_form_spec
+      - CurveFieldProofs.run_basepoint
+      - CurveFieldProofs.vartime_double_base_mul_spec
+      - CurveFieldProofs.verify_loop_full
+      - CurveFieldProofs.to_bytes_spec
+      - CurveFieldProofs.ed_compress_spec
+      - ScalarProofs.from_bytes_mod_order_wide_spec
+      - CurveFieldProofs.vartime_dsm_basepoint_spec
+      - CurveFieldProofs.enc_point_inj
+      - CurveFieldProofs.pow_p58_spec
+      - CurveFieldProofs.fe_ct_eq_spec
+      - CurveFieldProofs.sqrt_core
+      - CurveFieldProofs.sqrt_ratio_i_sq_spec
+      - CurveFieldProofs.from_bytes_spec
+      - CurveFieldProofs.decompress_of_canonical
+      - CurveFieldProofs.verify_accepts_iff
+      - CurveFieldProofs.verify_accepts_iff_decompress
+      - CurveFieldProofs.verify_accepts_iff_point
+      - CurveFieldProofs.verify_accepts_iff_point_eq
+      - ScalarProofs.L_val
+      - ScalarProofs.sub_loop_spec
+      - ScalarProofs.cond_add_l_one_spec
+      - ScalarProofs.sub_val_spec
+      - ScalarProofs.add_val_spec
+      - ScalarProofs.mul_internal_spec
+      - ScalarProofs.part1_spec
+      - ScalarProofs.montgomery_reduce_spec
+      - ScalarProofs.mul_spec
+      - ScalarProofs.scalarImplementation
+      - ScalarProofs.montgomery_mul_spec
+      - ScalarProofs.bytes_unpack_spec
+      - ScalarProofs.from_bytes_wide_spec
+    axiom_imports:
+      - Proofs.FieldMain
+      - Proofs.EdMain
+      - Proofs.ScalarMain
+      - Proofs.ToBytesSpec
+      - Proofs.CompressSpec
+      - Proofs.ScalarPackSpec
+      - Proofs.DsmMulSpec
+      - Proofs.SigApexSpec
+      - Proofs.PointLiftSpec
+      - Proofs.PointEqSpec
+      - Proofs.DecompressSpec
+      - Proofs.FromBytesSpec
+      - Proofs.DecompressMain
+      - Proofs.ScalarDenote
+      - Proofs.ScalarLoop
+      - Proofs.ScalarSubSpec
+      - Proofs.ScalarAddSpec
+      - Proofs.ScalarMulSpec
+      - Proofs.ScalarMontSpec
+      - Proofs.ScalarReduceSpec
+      - Proofs.ScalarFullMulSpec
+      - Proofs.ScalarWideSpec
+      - Proofs.ScalarBytesSpec
+      - Proofs.ScalarUnpackSpec
+      - Proofs.ScalarFromBytesSpec
+    replay_exclude:
+      - "Proofs/Audit.lean"
+      - "Proofs/ScalarAudit.lean"
+      - "Proofs/AxiomCheck.lean"
+      - "Proofs/Inventory*.lean"
   - name: risc0-ed25519-verified
     url: https://github.com/saymrwulf/risc0-ed25519-verified.git
     kind: ed25519
@@ -43,6 +203,86 @@ repos:
     lean_guard: verification/lean-guard
     backend_warning: pure Rust path only; do not treat zkVM accelerator/syscall path as verified
 
+    # certificates + imports MEASURED from the two buttons (CERTS arrays;
+    # apex recovered the way Phase 3c itself recovers it). replay_exclude:
+    # the button-owned audit instruments the replay does not compile —
+    # disclosed per-leaf in replay.instruments_excluded.
+    certificates:
+      - CurveFieldProofs.fieldImplementation
+      - CurveFieldProofs.edwardsImplementation
+      - CurveFieldProofs.naf_table_spec
+      - CurveFieldProofs.naf_select_spec
+      - CurveFieldProofs.proj_double_law
+      - CurveFieldProofs.compl_as_projective_law
+      - CurveFieldProofs.dsm_step_p_law
+      - CurveFieldProofs.dsm_step_b_law
+      - CurveFieldProofs.dsm_loop_spec
+      - CurveFieldProofs.naf_load_spec
+      - CurveFieldProofs.naf_exit
+      - CurveFieldProofs.naf_digit_loop_spec
+      - CurveFieldProofs.non_adjacent_form_spec
+      - CurveFieldProofs.run_basepoint
+      - CurveFieldProofs.vartime_double_base_mul_spec
+      - CurveFieldProofs.verify_loop_full
+      - CurveFieldProofs.to_bytes_spec
+      - CurveFieldProofs.ed_compress_spec
+      - ScalarProofs.from_bytes_mod_order_wide_spec
+      - CurveFieldProofs.vartime_dsm_basepoint_spec
+      - CurveFieldProofs.enc_point_inj
+      - CurveFieldProofs.pow_p58_spec
+      - CurveFieldProofs.fe_ct_eq_spec
+      - CurveFieldProofs.sqrt_core
+      - CurveFieldProofs.sqrt_ratio_i_sq_spec
+      - CurveFieldProofs.from_bytes_spec
+      - CurveFieldProofs.decompress_of_canonical
+      - CurveFieldProofs.verify_accepts_iff
+      - CurveFieldProofs.verify_accepts_iff_decompress
+      - CurveFieldProofs.verify_accepts_iff_point
+      - CurveFieldProofs.verify_accepts_iff_point_eq
+      - ScalarProofs.L_val
+      - ScalarProofs.sub_loop_spec
+      - ScalarProofs.sub_loop1_one_spec
+      - ScalarProofs.sub_val_spec
+      - ScalarProofs.add_val_spec
+      - ScalarProofs.mul_internal_spec
+      - ScalarProofs.part1_spec
+      - ScalarProofs.montgomery_reduce_spec
+      - ScalarProofs.mul_spec
+      - ScalarProofs.scalarImplementation
+      - ScalarProofs.montgomery_mul_spec
+      - ScalarProofs.bytes_unpack_spec
+      - ScalarProofs.from_bytes_wide_spec
+    axiom_imports:
+      - Proofs.FieldMain
+      - Proofs.EdMain
+      - Proofs.ScalarMain
+      - Proofs.ToBytesSpec
+      - Proofs.CompressSpec
+      - Proofs.ScalarPackSpec
+      - Proofs.DsmMulSpec
+      - Proofs.SigApexSpec
+      - Proofs.PointLiftSpec
+      - Proofs.PointEqSpec
+      - Proofs.DecompressSpec
+      - Proofs.FromBytesSpec
+      - Proofs.DecompressMain
+      - Proofs.ScalarDenote
+      - Proofs.ScalarLoop
+      - Proofs.ScalarSubSpec
+      - Proofs.ScalarAddSpec
+      - Proofs.ScalarMulSpec
+      - Proofs.ScalarMontSpec
+      - Proofs.ScalarReduceSpec
+      - Proofs.ScalarFullMulSpec
+      - Proofs.ScalarWideSpec
+      - Proofs.ScalarBytesSpec
+      - Proofs.ScalarUnpackSpec
+      - Proofs.ScalarFromBytesSpec
+    replay_exclude:
+      - "Proofs/Audit.lean"
+      - "Proofs/ScalarAudit.lean"
+      - "Proofs/AxiomCheck.lean"
+      - "Proofs/Inventory*.lean"
   - name: betrusted-ed25519-verified
     url: https://github.com/saymrwulf/betrusted-ed25519-verified.git
     kind: ed25519
@@ -54,6 +294,86 @@ repos:
     lean_guard: verification/lean-guard
     backend_warning: pure Rust path only; do not treat Engine25519/hardware accelerator as verified
 
+    # certificates + imports MEASURED from the two buttons (CERTS arrays;
+    # apex recovered the way Phase 3c itself recovers it). replay_exclude:
+    # the button-owned audit instruments the replay does not compile —
+    # disclosed per-leaf in replay.instruments_excluded.
+    certificates:
+      - CurveFieldProofs.fieldImplementation
+      - CurveFieldProofs.edwardsImplementation
+      - CurveFieldProofs.naf_table_spec
+      - CurveFieldProofs.naf_select_spec
+      - CurveFieldProofs.proj_double_law
+      - CurveFieldProofs.compl_as_projective_law
+      - CurveFieldProofs.dsm_step_p_law
+      - CurveFieldProofs.dsm_step_b_law
+      - CurveFieldProofs.dsm_loop_spec
+      - CurveFieldProofs.naf_load_spec
+      - CurveFieldProofs.naf_exit
+      - CurveFieldProofs.naf_digit_loop_spec
+      - CurveFieldProofs.non_adjacent_form_spec
+      - CurveFieldProofs.run_basepoint
+      - CurveFieldProofs.vartime_double_base_mul_spec
+      - CurveFieldProofs.verify_loop_full
+      - CurveFieldProofs.to_bytes_spec
+      - CurveFieldProofs.ed_compress_spec
+      - ScalarProofs.from_bytes_mod_order_wide_spec
+      - CurveFieldProofs.vartime_dsm_basepoint_spec
+      - CurveFieldProofs.enc_point_inj
+      - CurveFieldProofs.pow_p58_spec
+      - CurveFieldProofs.fe_ct_eq_spec
+      - CurveFieldProofs.sqrt_core
+      - CurveFieldProofs.sqrt_ratio_i_sq_spec
+      - CurveFieldProofs.from_bytes_spec
+      - CurveFieldProofs.decompress_of_canonical
+      - CurveFieldProofs.verify_accepts_iff
+      - CurveFieldProofs.verify_accepts_iff_decompress
+      - CurveFieldProofs.verify_accepts_iff_point
+      - CurveFieldProofs.verify_accepts_iff_point_eq
+      - ScalarProofs.L_val
+      - ScalarProofs.sub_loop_spec
+      - ScalarProofs.sub_loop1_one_spec
+      - ScalarProofs.sub_val_spec
+      - ScalarProofs.add_val_spec
+      - ScalarProofs.mul_internal_spec
+      - ScalarProofs.part1_spec
+      - ScalarProofs.montgomery_reduce_spec
+      - ScalarProofs.mul_spec
+      - ScalarProofs.scalarImplementation
+      - ScalarProofs.montgomery_mul_spec
+      - ScalarProofs.bytes_unpack_spec
+      - ScalarProofs.from_bytes_wide_spec
+    axiom_imports:
+      - Proofs.FieldMain
+      - Proofs.EdMain
+      - Proofs.ScalarMain
+      - Proofs.ToBytesSpec
+      - Proofs.CompressSpec
+      - Proofs.ScalarPackSpec
+      - Proofs.DsmMulSpec
+      - Proofs.SigApexSpec
+      - Proofs.PointLiftSpec
+      - Proofs.PointEqSpec
+      - Proofs.DecompressSpec
+      - Proofs.FromBytesSpec
+      - Proofs.DecompressMain
+      - Proofs.ScalarDenote
+      - Proofs.ScalarLoop
+      - Proofs.ScalarSubSpec
+      - Proofs.ScalarAddSpec
+      - Proofs.ScalarMulSpec
+      - Proofs.ScalarMontSpec
+      - Proofs.ScalarReduceSpec
+      - Proofs.ScalarFullMulSpec
+      - Proofs.ScalarWideSpec
+      - Proofs.ScalarBytesSpec
+      - Proofs.ScalarUnpackSpec
+      - Proofs.ScalarFromBytesSpec
+    replay_exclude:
+      - "Proofs/Audit.lean"
+      - "Proofs/ScalarAudit.lean"
+      - "Proofs/AxiomCheck.lean"
+      - "Proofs/Inventory*.lean"
   - name: pasta-pallas-verified
     url: https://github.com/saymrwulf/pasta-pallas-verified.git
     kind: pasta_pallas
@@ -221,3 +541,56 @@ repos:
       LTLAcc.take_append_drop: []
       LTLAcc.take_drop_prefix: ["propext", "Classical.choice", "Quot.sound"]
       LTLAcc.take_take_le: ["propext", "Quot.sound"]
+
+  - name: fips205-slhdsa-verified
+    url: https://github.com/saymrwulf/fips205-slhdsa-verified.git
+    kind: slh_dsa
+    verification_dir: verification
+    verified_backend: verify-mono/sha2-128s
+    env_script: ~/aeneas-toolchain/env.sh
+    lean_project_dir: $AENEAS_HOME/backends/lean
+    lean_guard: verification/lean-guard
+    backend_warning: >-
+      proved subject is the private verify_mono facade; the bridge to the
+      deployed generic pk.verify() is a 137-case differential test, not a
+      machine-checked refinement (TRUSTED-BASE item 9)
+    known_exclusions:
+      - the five verify-path hash oracles h_msg/f/h/t_l/t_len (assumed, not proven against FIPS 180-4)
+      - signing and key generation (out of extraction scope entirely)
+      - "everything above the extraction root: M' assembly, the pure/prehash domain-separator byte, ctx length bound, deserialization (TRUSTED-BASE item 10)"
+      - the base_2b inner loop (threaded opaquely, no certificate)
+      - parameter sets other than SLH-DSA-SHA2-128s
+      - compiler correctness and side channels
+    axiom_imports:
+      - Proofs.ApexSpec
+      - Proofs.ChainSpec
+      - Proofs.ForsInnerSpec
+      - Proofs.ForsOuterSpec
+      - Proofs.HtSpec
+      - Proofs.InputPrepSpec
+      - Proofs.WotsSpec
+      - Proofs.XmssSpec
+    certificates:
+      - fips205.base2b_outer_loop_eq
+      - fips205.chain_free_loop_eq
+      - fips205.fors_inner_loop_eq
+      - fips205.fors_outer_loop_eq
+      - fips205.ht_loop_eq
+      - fips205.slh_verify_128s_accepts_iff
+      - fips205.to_byte_loop_eq
+      - fips205.to_int_loop_eq
+      - fips205.wots_csum_loop_eq
+      - fips205.wots_loop1_eq
+      - fips205.xmss_loop_eq
+    certificate_axioms:
+      fips205.base2b_outer_loop_eq: ["Classical.choice", "Quot.sound", "propext"]
+      fips205.chain_free_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f"]
+      fips205.fors_inner_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.h"]
+      fips205.fors_outer_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f", "verify_mono.oracle.h"]
+      fips205.ht_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f", "verify_mono.oracle.h", "verify_mono.oracle.t_l"]
+      fips205.slh_verify_128s_accepts_iff: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f", "verify_mono.oracle.h", "verify_mono.oracle.h_msg", "verify_mono.oracle.t_l", "verify_mono.oracle.t_len"]
+      fips205.to_byte_loop_eq: ["Classical.choice", "Quot.sound", "propext"]
+      fips205.to_int_loop_eq: ["Classical.choice", "Quot.sound", "propext"]
+      fips205.wots_csum_loop_eq: ["Classical.choice", "Quot.sound", "propext"]
+      fips205.wots_loop1_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f"]
+      fips205.xmss_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.h"]

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
 

provider/src/pacta_provider/published_assets.py

@@ -22,7 +22,11 @@ files in this repository alone:
   1. every entry's leaf hash,
   2. every historical Signed Tree Head against the recomputed prefix root
      (a split view or tampered entry fails here),
-  3. every STH Ed25519 signature,
+  3. every STH Ed25519 signature — and, where a head carries the ADDITIVE
+     SLH-DSA-SHA2-128s signature (FIPS 205, heads from 2026-08 on), that
+     too: a present-but-wrong post-quantum signature FAILS the run, a head
+     without one is allowed, and an OpenSSL too old to check it (pre-3.5)
+     is reported loudly as a degradation, never counted as verified,
   4. every published receipt under receipts/ (with --all), and any receipt
      supplied via --receipt FILE, as a FULL transparency receipt: type tag,
      STH signature, REQUIRED key fingerprint, log id, presence of its STH
@@ -140,6 +144,57 @@ def check_sth_signature(head) -> str:
     return "VALID" if result.returncode == 0 else "INVALID"
 
 
+def check_slh_dsa_signature(head):
+    """ADDITIVE post-quantum check (SLH-DSA-SHA2-128s, FIPS 205).
+
+    Returns (status, hard_failure). Ed25519 remains the REQUIRED signature;
+    this one is verified when the head carries it and the local OpenSSL
+    (>= 3.5) can check it. The distinctions matter:
+      ABSENT    - head predates the second signature. Allowed: additive.
+      VALID     - verified against provider.slhdsa.pub.
+      INVALID   - present and WRONG. Hard failure - a bad signature is never
+                  a degradation.
+      WRONG-KEY - the head names a different key than the mirror ships.
+                  Hard failure.
+      NO-PUBKEY - the head claims the signature but the mirror ships no
+                  provider.slhdsa.pub. Broken publication: hard failure.
+      TOOLING   - this OpenSSL cannot read SLH-DSA keys (pre-3.5). Honest
+                  degradation: reported loudly, never counted as verified,
+                  never failed - the required Ed25519 check still gates.
+    """
+    slh = (head.get("signatures") or {}).get("slh_dsa") or {}
+    if slh.get("status") != "signed":
+        return "ABSENT", False
+    key = HERE / "provider.slhdsa.pub"
+    openssl = shutil.which("openssl")
+    if not openssl:
+        return "TOOLING", False
+    if not key.exists():
+        return "NO-PUBKEY", True
+    fp = slh.get("public_key_fingerprint_sha256")
+    if fp and fp != hashlib.sha256(key.read_bytes()).hexdigest():
+        return "WRONG-KEY", True
+    probe = subprocess.run([openssl, "pkey", "-pubin", "-in", str(key), "-noout"],
+                           capture_output=True)
+    if probe.returncode != 0:
+        return "TOOLING", False
+    payload = canonical_json({k: v for k, v in head.items() if k != "signatures"})
+    with tempfile.TemporaryDirectory() as tmp:
+        payload_path = Path(tmp) / "p"
+        signature_path = Path(tmp) / "s"
+        payload_path.write_bytes(payload)
+        try:
+            signature_path.write_bytes(base64.b64decode(slh.get("signature_base64", "")))
+        except Exception:
+            return "INVALID", True
+        result = subprocess.run(
+            [openssl, "pkeyutl", "-verify", "-pubin", "-inkey", str(key), "-rawin",
+             "-in", str(payload_path), "-sigfile", str(signature_path)],
+            capture_output=True,
+        )
+    return ("VALID", False) if result.returncode == 0 else ("INVALID", True)
+
+
 RECEIPT_TYPE = "pacta.transparency.receipt.v1"
 
 
@@ -245,6 +300,7 @@ def main() -> int:
         # published latest-sth.json is exactly the final history head.
         previous = -1
         log_id = None
+        slh_tooling_seen = False
         for position, head in enumerate(heads):
             size = int(head["tree_size"])
             if size > len(leaves):
@@ -260,8 +316,20 @@ def main() -> int:
             signature = check_sth_signature(head)
             if signature == "INVALID" or (signature == "UNAVAILABLE" and not args.structural_only):
                 failures.append(f"STH #{position} signature {signature}")
-            print(f"STH #{position} size={size} root={head['root_hash'][:16]}… prefix-root:{structural} signature:{signature}")
+            if args.structural_only:
+                slh = "SKIPPED"
+            else:
+                slh, slh_hard = check_slh_dsa_signature(head)
+                if slh_hard:
+                    failures.append(f"STH #{position} slh_dsa {slh}")
+                if slh == "TOOLING":
+                    slh_tooling_seen = True
+            print(f"STH #{position} size={size} root={head['root_hash'][:16]}… prefix-root:{structural} signature:{signature} slh_dsa:{slh}")
             previous = max(previous, size)
+        if slh_tooling_seen:
+            print("NOTE: this log carries an ADDITIVE SLH-DSA (FIPS 205) signature that "
+                  "your OpenSSL cannot check (needs >= 3.5). The required Ed25519 checks "
+                  "above still gate this result; the post-quantum signature was NOT verified.")
         latest_path = HERE / "latest-sth.json"
         if latest_path.exists() and heads:
             latest = json.loads(latest_path.read_text())
@@ -371,6 +439,40 @@ def main() -> int:
     cases.append(("--structural-only is explicit, never claims full",
                   code == 0 and "REDUCED" in out and "[full]" not in out))
 
+    # The ADDITIVE post-quantum signature must fail closed when tampered.
+    # Applicable only to mirrors whose heads carry it; older mirrors record
+    # the case as not-applicable rather than silently passing.
+    latest = json.loads((HERE / "latest-sth.json").read_text())
+    slh = (latest.get("signatures") or {}).get("slh_dsa") or {}
+    if slh.get("status") == "signed":
+        import base64 as _b64
+        import shutil as _sh
+        with tempfile.TemporaryDirectory() as tmp:
+            mirror = Path(tmp) / "mirror"
+            _sh.copytree(HERE, mirror)
+            raw = bytearray(_b64.b64decode(slh["signature_base64"])); raw[0] ^= 1
+            bad = _b64.b64encode(bytes(raw)).decode()
+            for name in ("latest-sth.json", "sth-history.jsonl"):
+                path = mirror / name
+                text = path.read_text().replace(slh["signature_base64"], bad)
+                path.write_text(text)
+            result = subprocess.run([sys.executable, str(mirror / "verify.py"), "--all"],
+                                    capture_output=True, text=True)
+            cases.append(("corrupted slh_dsa signature REJECTED",
+                          result.returncode == 1 and "slh_dsa:INVALID" in result.stdout))
+            # and the missing-pubkey path: a mirror claiming the signature but
+            # shipping no key is a broken publication, not a degradation.
+            (mirror / "provider.slhdsa.pub").unlink()
+            for name in ("latest-sth.json", "sth-history.jsonl"):
+                path = mirror / name
+                path.write_text(path.read_text().replace(bad, slh["signature_base64"]))
+            result = subprocess.run([sys.executable, str(mirror / "verify.py"), "--all"],
+                                    capture_output=True, text=True)
+            cases.append(("signed slh_dsa without published key REJECTED",
+                          result.returncode == 1 and "NO-PUBKEY" in result.stdout))
+    else:
+        cases.append(("slh_dsa cases n/a (no signed slh_dsa block in this mirror)", True))
+
     with tempfile.TemporaryDirectory() as tmp:
         os.symlink(sys.executable, Path(tmp) / Path(sys.executable).name)
         code, out = run("--all", env={"PATH": tmp})
@@ -403,8 +505,12 @@ kernel-checked proofs *about the accumulator model* underlying its own
 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). Current head: tree size 13, root
-`3488a2d0…`.
+signing, or execution provenance). As of **2026-08** the log also attests
+the **SLH-DSA (FIPS 205) verify-path proofs**
+([`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` —
+this README deliberately names no tree size, so it cannot go stale.
 
 Layout:
 
@@ -415,7 +521,8 @@ Layout:
 | `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 |
-| `provider.ed25519.pub` | the provider's public key — the sole cryptographic identity anchor; each statement's truth additionally rests on the assumptions stated in its leaf |
+| `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` | 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 |
 
@@ -439,5 +546,12 @@ declared trusted base). The log deliberately
 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
-provider's own Merkle self-check of that library's leaf.
+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:
+additive, so Ed25519 remains the signature a consumer must check, and honest
+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.
 '''

provider/src/pacta_provider/service.py

@@ -30,8 +30,26 @@ def build_attestation(
     profile = get_profile(repo.kind, repo)
     layout = discover_layout(path, repo.verification_dir)
     lean_guard = resolve_lean_guard(repo.lean_guard, path)
+    # The replay compiles the certificate corpus, not the button's audit
+    # instruments (see RepoConfig.replay_exclude). Filter by the path relative
+    # to the verification dir; record what was actually excluded so the LEAF
+    # says it — a silent exclusion here would be the exact defect class the
+    # estate keeps finding.
+    import fnmatch as _fnmatch
+    verification_root = path / repo.verification_dir
+    compile_order = layout.compile_order
+    instruments_excluded: list[str] = []
+    if repo.replay_exclude:
+        kept = []
+        for f in compile_order:
+            rel = str(Path(f).resolve().relative_to(verification_root.resolve()))
+            if any(_fnmatch.fnmatch(rel, g) for g in repo.replay_exclude):
+                instruments_excluded.append(rel)
+            else:
+                kept.append(f)
+        compile_order = kept
     check = lean_check_files(
-        layout.compile_order,
+        compile_order,
         layout.verification_dir,
         timeout=timeout,
         log_dir=log_dir,
@@ -103,6 +121,10 @@ def build_attestation(
             "check_log_path": check.log_path,
             "checked_files": len(check.checked_files),
             "failed_files": check.failed_files,
+            # The button's audit instruments this replay did NOT compile —
+            # disclosed in the leaf rather than silently absent. Empty for
+            # repositories without a replay_exclude list.
+            "instruments_excluded": sorted(instruments_excluded),
             "diagnostics": check.diagnostics,
             "axiom_attempted": axiom.attempted if axiom else False,
             "axiom_ok": axiom.ok if axiom else False,

provider/src/pacta_provider/transparency_log.py

@@ -96,6 +96,8 @@ class TransparencyLog:
         private_key_path: str | Path,
         public_key_path: str | Path,
         timestamp: str | None = None,
+        slhdsa_private_key_path: str | Path | None = None,
+        slhdsa_public_key_path: str | Path | None = None,
     ) -> dict[str, Any]:
         metadata = self.metadata()
         entries = self.entries()
@@ -108,6 +110,8 @@ class TransparencyLog:
             private_key_path,
             public_key_path,
             signing_provenance=self.signing_provenance(entries),
+            slhdsa_private_key_path=slhdsa_private_key_path,
+            slhdsa_public_key_path=slhdsa_public_key_path,
         )
         dump_data(sth, self.sth_path)
         self._record_sth(sth)
@@ -119,6 +123,8 @@ class TransparencyLog:
         private_key_path: str | Path,
         public_key_path: str | Path,
         receipt_out: str | Path | None = None,
+        slhdsa_private_key_path: str | Path | None = None,
+        slhdsa_public_key_path: str | Path | None = None,
     ) -> dict[str, Any]:
         metadata = self.metadata()
         attestation = load_data(attestation_path)
@@ -151,6 +157,8 @@ class TransparencyLog:
             private_key_path,
             public_key_path,
             signing_provenance=self.signing_provenance(entries),
+            slhdsa_private_key_path=slhdsa_private_key_path,
+            slhdsa_public_key_path=slhdsa_public_key_path,
         )
         dump_data(sth, self.sth_path)
         self._record_sth(sth)
@@ -302,6 +310,12 @@ class TransparencyLog:
         (out / "README.md").write_text(README_MD, encoding="utf-8")
         if public_key_path is not None:
             (out / "provider.ed25519.pub").write_bytes(Path(public_key_path).read_bytes())
+            # The SLH-DSA verification key travels beside the Ed25519 one the
+            # moment it exists (operator decision 2026-08-06: additive second
+            # signature). Public key only — nothing secret lives near this path.
+            slh_pub = Path(public_key_path).parent / "provider.slhdsa.pub"
+            if slh_pub.exists():
+                (out / "provider.slhdsa.pub").write_bytes(slh_pub.read_bytes())
         return {"entries": len(entries), "components": sorted(components), "out": str(out)}
 
     def consistency_from(self, old_tree_size: int) -> dict[str, Any]:

provider/src/pacta_provider/web.py

@@ -65,11 +65,16 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
                 self.send_header("Content-Length", str(len(body)))
                 self.end_headers()
                 self.wfile.write(body)
-            elif route == "/log-public-key":
+            elif route in ("/log-public-key", "/log-slhdsa-public-key"):
                 # TOFU mitigation depends on the key being published in two
                 # independent locations; this is the site's copy (the mirror
                 # carries the other). Serving only a fingerprint would not do.
-                key_path = Path(log.log_dir) / "provider.ed25519.pub"
+                # The SLH-DSA key (additive post-quantum signature, 2026-08)
+                # is published THE SAME WAY as the Ed25519 one — same route
+                # shape, same two-location rule.
+                fname = ("provider.ed25519.pub" if route == "/log-public-key"
+                         else "provider.slhdsa.pub")
+                key_path = Path(log.log_dir) / fname
                 if not key_path.is_file():
                     self._send(404, {"error": "log public key not present in this log directory"})
                     return
@@ -152,6 +157,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
                         f"{base}/docs",
                         f"{base}/paper",
                         f"{base}/log-public-key",
+                        f"{base}/log-slhdsa-public-key",
                         f"{base}/healthz",
                         f"{base}/{API_VERSION}/metadata",
                         f"{base}/{API_VERSION}/sth",

provider/src/pacta_provider/webdocs.py

@@ -50,7 +50,7 @@ def _leaf_ok(entry: LogEntry) -> bool:
     )
 
 
-def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str) -> str:
+def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head_label: str = "Ed25519") -> str:
     """The accumulator, drawn from its real leaves."""
     if not entries:
         return "<p class='muted'>(log is empty)</p>"
@@ -94,7 +94,7 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str) -> s
                         out.append(f'<line x1="{x}" y1="{y+15}" x2="{cx}" y2="{cy-22 if level_index==1 else cy-15}" stroke="#ccc"/>')
     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 — Ed25519({root_hex[:12]}…)</text>')
+    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'<line x1="{root_x}" y1="{root_y-38}" x2="{root_x}" y2="{root_y-15}" stroke="#1e7f4f" stroke-width="1.4"/>')
     out.append("</svg>")
@@ -114,6 +114,28 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str
             f'<a href="{mirror}/blob/main/provider.ed25519.pub">mirror</a> instead.</div>'
         )
     pem = escape(key_path.read_text(encoding="utf-8").strip())
+    # The SLH-DSA verification key (additive post-quantum head signature,
+    # 2026-08) is published THE SAME WAY: full PEM on the page, raw endpoint,
+    # mirror comparison. Heads before tree 14 carry no SLH-DSA signature and
+    # verify.py reports them ABSENT — allowed; an append-only log keeps its
+    # history.
+    slh_path = log.log_dir / "provider.slhdsa.pub"
+    if slh_path.is_file():
+        import hashlib as _h
+        slh_pem = escape(slh_path.read_text(encoding="utf-8").strip())
+        slh_fp = _h.sha256(slh_path.read_bytes()).hexdigest()
+        slh_block = f"""<hr style="border:none;border-top:1px solid #ddd;margin:.8rem 0">
+<p style="margin-top:0"><strong>Second, additive anchor — post-quantum.</strong> Heads from
+tree&nbsp;14 on additionally carry a deterministic <strong>SLH-DSA-SHA2-128s</strong> (FIPS&nbsp;205)
+signature over the same payload. The Ed25519 signature above remains the one every consumer must
+check; this one is checked where tooling allows (OpenSSL&nbsp;≥&nbsp;3.5). Its verify path is the
+proof subject of leaf&nbsp;18.</p>
+<pre style="margin-bottom:.4rem">{slh_pem}</pre>
+<p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{slh_fp}</code>
+&nbsp;·&nbsp; raw: <a href="{base}/log-slhdsa-public-key"><code>{base or ''}/log-slhdsa-public-key</code></a>
+&nbsp;·&nbsp; mirror: <a href="{mirror}/blob/main/provider.slhdsa.pub">provider.slhdsa.pub</a></p>"""
+    else:
+        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
@@ -126,7 +148,7 @@ Pin it, and compare this copy byte-for-byte with the independently hosted
 <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>
-</div>"""
+{slh_block}</div>"""
 
 
 def render_docs(log: TransparencyLog, base_path: str) -> str:
@@ -161,7 +183,9 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
         f"<td><span class='pill ok'>{escape(_counts(newest[c]))}</span></td></tr>"
         for c in components
     )
-    tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend)
+    slh_signed = ((latest.get("signatures") or {}).get("slh_dsa") or {}).get("status") == "signed"
+    head_label = "Ed25519 + SLH-DSA" if slh_signed else "Ed25519"
+    tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend, head_label)
 
     return f"""<!doctype html><html lang="en"><head><meta charset="utf-8">
 <meta name="viewport" content="width=device-width,initial-scale=1">
@@ -176,7 +200,8 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
 accumulator of <em>signed statements that the Lean&nbsp;4 formal proofs of specific
 cryptographic Rust libraries, at specific git commits, machine-re-check with exactly
 their documented assumptions</em> — so that you can trust a proof result by checking
-<strong>one signature and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in
+<strong>one required signature (Ed25519; heads from tree&nbsp;14 add an additive post-quantum
+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>
@@ -216,11 +241,12 @@ which observed axiom cones, what machine protection — signed by the provider.<
 <td>table above, 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 stdlib Python verify it.</td>
+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>
 <td>table above, 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> (stdlib-only). <code>python3 verify.py --all</code>
+ever issued + <code>verify.py</code> (Python stdlib + the <code>openssl</code> binary for
+signatures; fails closed without them). <code>python3 verify.py --all</code>
 recomputes the entire tree and every historical head — you then hold a retained view that can
 later EXPOSE a conflicting head shown to someone else. (A single clone cannot by itself prove the
 log never split its view toward another consumer; that requires comparing heads across
@@ -292,19 +318,39 @@ our roadmap.</strong> (The full walk-through is lecture&nbsp;11 in the
 <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, v0.9) — the trust decomposition (expensive verification produces an
+(PDF, 23 pages, v0.9 — <strong>frozen while under journal review</strong>; it describes the
+log as of its 16&nbsp;July&nbsp;2026 snapshot) — 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
 accountability GAMES with an explicit composition theorem (head authenticity, position
 binding, history binding with a fully proved prefix-transport induction, context-scoped
 fork evidence — all discharged by named reductions), the policy boundary where
-operator labels can veto but never grant acceptance, the live thirteen-leaf deployment
+operator labels can veto but never grant acceptance, the then-thirteen-leaf deployment
 whose entry 13 attests the accumulator's own mechanized model, and the measured
 model/deployment divergence (3,867 lied-size cases, every one accepted only by the
 deployed verifier) reported as a result rather than hidden.
 <span class="muted">Previous versions: <a href="{base}/paper/v0.2">v0.2</a> (19 pages, the
 system report) · <a href="{base}/paper/v0.1">v0.1</a> (4 pages).</span></div>
 
+<div class="card"><strong>Reading the paper against today's log.</strong> The paper is frozen
+under review; the log is append-only and has kept moving. Nothing the paper describes was
+altered, so every number in it remains checkable against the live history: the thirteen leaves
+it analyses are still leaves 0–12, byte-identical, and the head it pins (tree&nbsp;13, root
+<code>3488a2d0…</code>) is still head&nbsp;#5 of <code>sth-history.jsonl</code> —
+<code>python3 verify.py --all</code> re-verifies the paper-era prefix together with everything
+after it. What has moved since the snapshot is additive: leaves&nbsp;13–16 re-attest the four
+Ed25519 libraries at 44 certificates each (the paper's sixteen-certificate corpora describe the
+leaf&nbsp;8–11 generation, which those leaves still record); leaf&nbsp;17 re-attests the
+accumulator's mechanized model at its hardened state; and leaf&nbsp;18 is the log's first
+post-quantum subject, the SLH-DSA-SHA2-128s verify path. Heads from tree&nbsp;14 on carry an
+additive SLH-DSA signature beside the Ed25519 signature the paper describes; earlier heads have
+none, by design, and the verifier reports them as <code>ABSENT</code> rather than failing them.
+One result has changed in the good direction: the 3,867-case model/deployment divergence the
+paper honestly reports was closed on 23&nbsp;July&nbsp;2026 (the <code>sn==0</code> fix); the
+current pinned divergence count is 0, and both the divergence and its fix are part of the
+retained record. Where the paper and the live log disagree on a number, the paper is describing
+its snapshot — and the log's history contains that snapshot, unchanged, inside 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 course (12 Jupyter
 lectures) live in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.</p>

src/pacta/config.py

@@ -28,6 +28,17 @@ class RepoConfig:
     env_script: str | None = None
     lean_project_dir: str | None = None
     lean_guard: str | None = None
+    # Files the provider REPLAY does not compile (globs relative to the
+    # verification dir). Exists because the hardened forks ship audit
+    # INSTRUMENTS — kernel-gate modules that read other modules' object files
+    # via readModuleData and only run inside the button's own environment
+    # (its cwd, LEAN_PATH and compile order). The replay's generic
+    # topological compile breaks on them (register:
+    # replay-pipeline-lags-hardened-forks). The replay checks the CERTIFICATES;
+    # the deeper self-auditing gates are the repository's own and run there.
+    # Every exclusion actually applied is recorded in the attestation's replay
+    # block, so the leaf discloses what its replay did not compile.
+    replay_exclude: list[str] = field(default_factory=list)
 
     @classmethod
     def from_dict(cls, raw: dict[str, Any]) -> "RepoConfig":
@@ -53,6 +64,7 @@ class RepoConfig:
             env_script=raw.get("env_script"),
             lean_project_dir=raw.get("lean_project_dir"),
             lean_guard=raw.get("lean_guard"),
+            replay_exclude=[str(g) for g in (raw.get("replay_exclude") or [])],
         )
 
 

src/pacta/dogfood.py

@@ -12,7 +12,27 @@ from pathlib import Path
 from typing import Any
 
 DOGFOOD_ENV = "PACTA_DOGFOOD_VERIFIER"
-DEFAULT_STATE_DIR = Path("dogfood") / "state"
+REQUIRE_VERIFIED_ENV = "PACTA_REQUIRE_VERIFIED_SIGNER"
+
+# Anchored to the PACKAGE, not to the caller's working directory.
+#
+# This was `Path("dogfood") / "state"` — a relative path, so it resolved against
+# whatever directory the process happened to start in. The consequence was not a
+# crash but something quieter and worse: run the provider from the repository
+# root and it signs with the attested dalek build; run it from anywhere else and
+# locate_verifier() finds nothing, signing falls back to OpenSSL, and the head
+# records `signing_backend: openssl`. WHICH IMPLEMENTATION SIGNS THE
+# TRANSPARENCY LOG WAS AN ACCIDENT OF THE CURRENT DIRECTORY.
+#
+# Found 2026-08-04 by re-signing the published head 13 as a reproducibility
+# check: the byte comparison passed, but the backend came back `openssl` while
+# the published head says `verified-dalek-serial`. Both produced identical bytes
+# — Ed25519 is deterministic, so that is expected and is itself useful evidence
+# — which is exactly why the substitution was invisible. A silent backend swap
+# that changes no output is one nobody notices until the outputs differ.
+#
+# __file__ is <repo>/src/pacta/dogfood.py, so parents[2] is the repo root.
+DEFAULT_STATE_DIR = Path(__file__).resolve().parents[2] / "dogfood" / "state"
 BACKEND_VERIFIED = "verified-dalek-serial"
 BACKEND_OPENSSL = "openssl"
 
@@ -112,6 +132,21 @@ def locate_verifier(state_dir: str | Path | None = None) -> Path | None:
     return path if path.exists() else None
 
 
+def require_verified_signer() -> bool:
+    """Whether a downgrade to OpenSSL is forbidden for this process.
+
+    Recording a downgrade truthfully, which this code already does, tells you
+    afterwards which implementation signed. It does not let you DECIDE which
+    one will. For an operation as consequential as signing a transparency-log
+    head, the choice should be stated up front and enforced, not discovered in
+    the provenance field once the head exists.
+
+    Off by default: every existing caller keeps the fall-back-and-record
+    behaviour. Set PACTA_REQUIRE_VERIFIED_SIGNER=1 and signing raises instead
+    of quietly substituting OpenSSL."""
+    return os.environ.get(REQUIRE_VERIFIED_ENV, "").strip().lower() in {"1", "true", "yes", "on"}
+
+
 def load_provenance(binary_path: str | Path) -> dict[str, Any]:
     sidecar = Path(binary_path).with_suffix(".provenance.json")
     if sidecar.exists():

src/pacta/signing.py

@@ -92,12 +92,20 @@ def sign_payload_ed25519_detailed(payload: bytes, private_key_path: str | Path)
     library) and falling back to OpenSSL. Returns (base64 signature, the
     backend that actually signed) - the backend is recorded next to every
     signature so the provenance is never silent."""
-    from .dogfood import BACKEND_OPENSSL, BACKEND_VERIFIED, locate_verifier, sign_payload_dogfood
+    from .dogfood import (BACKEND_OPENSSL, BACKEND_VERIFIED, REQUIRE_VERIFIED_ENV,
+                          default_binary_path, locate_verifier, require_verified_signer,
+                          sign_payload_dogfood)
 
     binary = locate_verifier()
     if binary is not None:
         signature_bytes = sign_payload_dogfood(payload, private_key_path, binary)
         return base64.b64encode(signature_bytes).decode("ascii"), BACKEND_VERIFIED
+    if require_verified_signer():
+        raise SignatureError(
+            f"{REQUIRE_VERIFIED_ENV} is set, so falling back to OpenSSL is refused, but the "
+            f"attested signer was not found at {default_binary_path()}. "
+            f"Build it, or point {'PACTA_DOGFOOD_VERIFIER'} at it, or unset "
+            f"{REQUIRE_VERIFIED_ENV} to accept the recorded downgrade.")
     return _sign_payload_openssl(payload, private_key_path), BACKEND_OPENSSL
 
 

src/pacta/slhdsa.py

@@ -0,0 +1,232 @@
+"""SLH-DSA-SHA2-128s signing and verification for transparency-log heads.
+
+This module is the post-quantum signing path that did NOT exist before
+2026-08-06 (register: pq-slot-names-unproven-algorithm). Scope discipline,
+stated up front because the estate has measured what silence costs:
+
+  * The parameter set is LOCKED to SLH-DSA-SHA2-128s — the only set the
+    eleven fips205 certificates cover. Every entry point asserts the key's
+    algorithm and refuses anything else rather than producing a signature
+    outside every proof the estate holds.
+  * Signing is DETERMINISTIC (operator decision 2026-08-06): FIPS 205's
+    optional deterministic variant, selected via OpenSSL's
+    `-pkeyopt deterministic:1`. Chosen so the byte-level reproducibility
+    check that caught a real defect on the Ed25519 side survives for this
+    algorithm too. The trade is documented: fault-attack hardening from
+    hedged signing is forgone, for a key that signs a public log.
+  * NOTHING here is Lean-proven. The certificates cover the VERIFY path of
+    the extracted model; signing and key generation are outside every proof
+    (fips205 TRUSTED-BASE item 2). Verification below can be cross-checked
+    against the proven-source binary (pacta-verify-slhdsa); signing cannot
+    be cross-checked against anything proven, and no field this module
+    emits claims otherwise.
+"""
+from __future__ import annotations
+
+import base64
+import hashlib
+import os
+import subprocess
+import tempfile
+from pathlib import Path
+from typing import Any
+
+SLH_SCHEME = "openssl-slh-dsa-sha2-128s"
+SLH_STANDARD = "FIPS 205"
+SLH_PARAMETER_SET = "SLH-DSA-SHA2-128s"
+SLH_SIGNATURE_BYTES = 7856
+SLH_PUBLIC_KEY_BYTES = 32
+
+# Package-anchored, NOT cwd-relative. The Ed25519 twin of this constant was a
+# relative path and which implementation signed the log became an accident of
+# the launch directory (register: signer-backend-depends-on-cwd). parents[2]
+# of src/pacta/slhdsa.py is the repository root.
+_REPO_ROOT = Path(__file__).resolve().parents[2]
+PROVEN_VERIFIER = (_REPO_ROOT / "dogfood" / "quorum" / "verify-slhdsa"
+                   / "target" / "release" / "pacta-verify-slhdsa")
+SLHDSA_VERIFIER_ENV = "PACTA_SLHDSA_VERIFIER"
+
+
+class SlhDsaError(RuntimeError):
+    pass
+
+
+def _openssl() -> str:
+    import shutil
+    exe = shutil.which("openssl")
+    if not exe:
+        raise SlhDsaError("openssl binary not found; SLH-DSA operations unavailable")
+    return exe
+
+
+def _assert_128s_key(key_path: str | Path, public: bool) -> None:
+    """Refuse any key that is not SLH-DSA-SHA2-128s.
+
+    The check is on the PROPERTY (the algorithm OpenSSL reports for the key),
+    not on a filename. A signature under any other parameter set would sit
+    outside all eleven certificates while looking exactly like dogfood.
+    """
+    args = [_openssl(), "pkey", "-in", str(key_path), "-noout", "-text"]
+    if public:
+        args.insert(2, "-pubin")
+    result = subprocess.run(args, capture_output=True, text=True, timeout=30)
+    if result.returncode != 0:
+        raise SlhDsaError(f"cannot read key {key_path}: {(result.stderr or '').strip()[:120]}")
+    if SLH_PARAMETER_SET not in result.stdout:
+        first = (result.stdout.strip().splitlines() or ["<empty>"])[0]
+        raise SlhDsaError(
+            f"key {key_path} is not {SLH_PARAMETER_SET} (openssl reports: {first!r}). "
+            f"The certificates cover {SLH_PARAMETER_SET} only; refusing.")
+
+
+def generate_slhdsa_keypair(private_key_path: str | Path, public_key_path: str | Path) -> None:
+    """Generate an SLH-DSA-SHA2-128s key pair. Private key mode 0600.
+
+    Key generation is NOT covered by any certificate; this is OpenSSL's
+    generator, trusted base, and recorded as such wherever the key is used.
+    """
+    openssl = _openssl()
+    private_path = Path(private_key_path)
+    public_path = Path(public_key_path)
+    private_path.parent.mkdir(parents=True, exist_ok=True)
+    subprocess.run([openssl, "genpkey", "-algorithm", SLH_PARAMETER_SET,
+                    "-out", str(private_path)], check=True, timeout=60)
+    os.chmod(private_path, 0o600)
+    subprocess.run([openssl, "pkey", "-in", str(private_path), "-pubout",
+                    "-out", str(public_path)], check=True, timeout=30)
+    _assert_128s_key(private_path, public=False)
+    _assert_128s_key(public_path, public=True)
+
+
+def sign_payload_slhdsa(payload: bytes, private_key_path: str | Path) -> str:
+    """Deterministically sign; returns base64. Same payload + key => same bytes."""
+    _assert_128s_key(private_key_path, public=False)
+    openssl = _openssl()
+    with tempfile.TemporaryDirectory(prefix="pacta-slhdsa-sign-") as tmp:
+        payload_path = Path(tmp) / "payload.bin"
+        signature_path = Path(tmp) / "payload.sig"
+        payload_path.write_bytes(payload)
+        completed = subprocess.run(
+            [openssl, "pkeyutl", "-sign", "-inkey", str(private_key_path), "-rawin",
+             "-pkeyopt", "deterministic:1",
+             "-in", str(payload_path), "-out", str(signature_path)],
+            check=False, capture_output=True, text=True, timeout=120)
+        if completed.returncode != 0:
+            raise SlhDsaError((completed.stderr or "slh-dsa signing failed").strip())
+        signature = signature_path.read_bytes()
+    if len(signature) != SLH_SIGNATURE_BYTES:
+        raise SlhDsaError(
+            f"signature is {len(signature)} bytes, expected {SLH_SIGNATURE_BYTES} "
+            f"for {SLH_PARAMETER_SET} — wrong parameter set slipped through?")
+    return base64.b64encode(signature).decode("ascii")
+
+
+def verify_payload_slhdsa(payload: bytes, signature_base64: str,
+                          public_key_path: str | Path) -> tuple[bool, str | None]:
+    """Verify with OpenSSL. For the proven-source cross-check, see
+    verify_payload_slhdsa_proven — callers wanting both run both."""
+    _assert_128s_key(public_key_path, public=True)
+    try:
+        signature = base64.b64decode(signature_base64)
+    except Exception as exc:
+        return False, f"signature_base64 undecodable: {exc}"
+    if len(signature) != SLH_SIGNATURE_BYTES:
+        return False, f"signature is {len(signature)} bytes, expected {SLH_SIGNATURE_BYTES}"
+    openssl = _openssl()
+    with tempfile.TemporaryDirectory(prefix="pacta-slhdsa-verify-") as tmp:
+        payload_path = Path(tmp) / "payload.bin"
+        signature_path = Path(tmp) / "payload.sig"
+        payload_path.write_bytes(payload)
+        signature_path.write_bytes(signature)
+        completed = subprocess.run(
+            [openssl, "pkeyutl", "-verify", "-pubin", "-inkey", str(public_key_path),
+             "-rawin", "-in", str(payload_path), "-sigfile", str(signature_path)],
+            capture_output=True, timeout=120)
+    if completed.returncode == 0:
+        return True, None
+    return False, "OpenSSL rejected the SLH-DSA signature"
+
+
+def locate_proven_verifier() -> Path | None:
+    env = os.environ.get(SLHDSA_VERIFIER_ENV)
+    if env:
+        path = Path(env)
+        return path if path.exists() else None
+    return PROVEN_VERIFIER if PROVEN_VERIFIER.exists() else None
+
+
+def raw_public_key(public_key_path: str | Path) -> bytes:
+    der = subprocess.run([_openssl(), "pkey", "-pubin", "-in", str(public_key_path),
+                          "-outform", "DER"], capture_output=True, timeout=30).stdout
+    if len(der) < SLH_PUBLIC_KEY_BYTES:
+        raise SlhDsaError(f"cannot extract raw public key from {public_key_path}")
+    return der[-SLH_PUBLIC_KEY_BYTES:]
+
+
+def verify_payload_slhdsa_proven(payload: bytes, signature_base64: str,
+                                 public_key_path: str | Path) -> tuple[bool, str | None]:
+    """Verify with pacta-verify-slhdsa, built from the PINNED proven source.
+
+    This is the one place in the estate where a log signature is checked by
+    the implementation whose verify path the certificates actually cover.
+    Honest residue: the binary also assembles M' and does IO, which no
+    certificate reaches; and it is a compiled binary, while the proofs are
+    about the extracted model (the estate's standing R5 gap).
+    """
+    binary = locate_proven_verifier()
+    if binary is None:
+        return False, ("proven verifier not built (dogfood/quorum/build-verify-slhdsa.sh); "
+                       "refusing to report a proven-path verdict without it")
+    try:
+        signature = base64.b64decode(signature_base64)
+    except Exception as exc:
+        return False, f"signature_base64 undecodable: {exc}"
+    if len(signature) != SLH_SIGNATURE_BYTES:
+        return False, f"signature is {len(signature)} bytes, expected {SLH_SIGNATURE_BYTES}"
+    with tempfile.TemporaryDirectory(prefix="pacta-slhdsa-proven-") as tmp:
+        payload_path = Path(tmp) / "payload.bin"
+        payload_path.write_bytes(payload)
+        completed = subprocess.run(
+            [str(binary), raw_public_key(public_key_path).hex(), signature.hex(),
+             str(payload_path)], capture_output=True, text=True, timeout=120)
+    if completed.returncode == 0:
+        return True, None
+    if completed.returncode == 1:
+        return False, "proven verifier rejected the signature"
+    return False, f"proven verifier input error: {(completed.stderr or '').strip()[:120]}"
+
+
+def public_key_fingerprint(public_key_path: str | Path) -> str:
+    return hashlib.sha256(Path(public_key_path).read_bytes()).hexdigest()
+
+
+def slh_dsa_signature_block(payload: bytes, private_key_path: str | Path,
+                            public_key_path: str | Path) -> dict[str, Any]:
+    """The `signatures.slh_dsa` block for a signed tree head.
+
+    A SEPARATE block by operator decision 2026-08-06: the ml_dsa slot keeps
+    saying, truthfully, that ML-DSA was never configured; no algorithm is
+    swapped inside a field that names a different one.
+    """
+    signature_base64 = sign_payload_slhdsa(payload, private_key_path)
+    return {
+        "scheme": SLH_SCHEME,
+        "standard": SLH_STANDARD,
+        "parameter_set": SLH_PARAMETER_SET,
+        "mode": "deterministic",
+        "status": "signed",
+        "signing_backend": "openssl",  # honest: no proven signer exists, for any algorithm
+        "payload_digest_sha256": hashlib.sha256(payload).hexdigest(),
+        "signature_base64": signature_base64,
+        "public_key_fingerprint_sha256": public_key_fingerprint(public_key_path),
+    }
+
+
+def slh_dsa_not_configured_block() -> dict[str, Any]:
+    return {
+        "scheme": SLH_SCHEME,
+        "standard": SLH_STANDARD,
+        "parameter_set": SLH_PARAMETER_SET,
+        "status": "not_configured",
+        "reason": "No SLH-DSA signing key was configured for this log.",
+    }

src/pacta/transparency.py

@@ -158,6 +158,8 @@ def make_signed_tree_head(
     private_key_path: str | Path,
     public_key_path: str | Path,
     signing_provenance: dict[str, Any] | None = None,
+    slhdsa_private_key_path: str | Path | None = None,
+    slhdsa_public_key_path: str | Path | None = None,
 ) -> dict[str, Any]:
     sth: dict[str, Any] = {
         "schema_version": 1,
@@ -170,6 +172,17 @@ def make_signed_tree_head(
     }
     payload = signed_tree_head_payload(sth)
     signature_base64, signing_backend = sign_payload_ed25519_detailed(payload, private_key_path)
+    # slh_dsa is a SEPARATE block (operator decision 2026-08-06): ml_dsa keeps
+    # its truthful not-configured disclosure; no algorithm is swapped inside a
+    # field that names a different one. ADDITIVE: ed25519 remains the signature
+    # consumers must check; a head without an SLH-DSA key carries the honest
+    # not-configured slot, exactly as ml_dsa always has.
+    from .slhdsa import slh_dsa_not_configured_block, slh_dsa_signature_block
+
+    if slhdsa_private_key_path and slhdsa_public_key_path:
+        slh_block = slh_dsa_signature_block(payload, slhdsa_private_key_path, slhdsa_public_key_path)
+    else:
+        slh_block = slh_dsa_not_configured_block()
     sth["signatures"] = {
         "ed25519": {
             "scheme": "openssl-ed25519",
@@ -181,6 +194,7 @@ def make_signed_tree_head(
             **({"signing_provenance": signing_provenance} if signing_provenance else {}),
         },
         "ml_dsa": detect_ml_dsa().to_signature_slot(),
+        "slh_dsa": slh_block,
     }
     return sth
 

tests/test_slhdsa.py

@@ -0,0 +1,126 @@
+"""SLH-DSA signing path: deterministic, parameter-locked, two-verifier checked.
+
+Every test uses THROWAWAY keys generated into tmp_path. No test touches the
+provider state directory or any long-lived key.
+"""
+from __future__ import annotations
+
+import base64
+import json
+
+
+def _keypair(tmp_path):
+    from pacta.slhdsa import generate_slhdsa_keypair
+    priv, pub = tmp_path / "t.key", tmp_path / "t.pub"
+    generate_slhdsa_keypair(priv, pub)
+    return priv, pub
+
+
+def test_keygen_shape_and_permissions(tmp_path):
+    priv, pub = _keypair(tmp_path)
+    assert priv.exists() and pub.exists()
+    assert (priv.stat().st_mode & 0o777) == 0o600
+
+
+def test_deterministic_signing_reproduces_bytes(tmp_path):
+    """Operator decision 2026-08-06: same payload + key => identical bytes.
+    This is the property the Ed25519 reproducibility check relies on, and the
+    reason the deterministic variant was chosen over the FIPS 205 default."""
+    from pacta.slhdsa import sign_payload_slhdsa
+    priv, _pub = _keypair(tmp_path)
+    payload = b"the same head payload"
+    assert sign_payload_slhdsa(payload, priv) == sign_payload_slhdsa(payload, priv)
+
+
+def test_sign_verify_roundtrip_both_verifiers(tmp_path):
+    from pacta.slhdsa import (locate_proven_verifier, sign_payload_slhdsa,
+                              verify_payload_slhdsa, verify_payload_slhdsa_proven)
+    priv, pub = _keypair(tmp_path)
+    payload = b"a transparency log head payload"
+    sig = sign_payload_slhdsa(payload, priv)
+    ok, err = verify_payload_slhdsa(payload, sig, pub)
+    assert ok, err
+    if locate_proven_verifier() is None:
+        import pytest
+        pytest.skip("pacta-verify-slhdsa not built on this host")
+    ok, err = verify_payload_slhdsa_proven(payload, sig, pub)
+    assert ok, f"proven-source verifier disagrees with OpenSSL: {err}"
+
+
+def test_corruption_rejected_by_both(tmp_path):
+    from pacta.slhdsa import (locate_proven_verifier, sign_payload_slhdsa,
+                              verify_payload_slhdsa, verify_payload_slhdsa_proven)
+    priv, pub = _keypair(tmp_path)
+    payload = b"payload"
+    raw = bytearray(base64.b64decode(sign_payload_slhdsa(payload, priv)))
+    raw[0] ^= 1
+    bad = base64.b64encode(bytes(raw)).decode()
+    ok, _ = verify_payload_slhdsa(payload, bad, pub)
+    assert not ok
+    if locate_proven_verifier() is not None:
+        ok, _ = verify_payload_slhdsa_proven(payload, bad, pub)
+        assert not ok
+
+
+def test_parameter_set_lock_refuses_foreign_key(tmp_path):
+    """An Ed25519 key must be refused outright — a signature under any other
+    algorithm would look like dogfood while sitting outside every proof."""
+    import pytest
+    from pacta.signing import generate_ed25519_keypair
+    from pacta.slhdsa import SlhDsaError, sign_payload_slhdsa
+    priv, pub = tmp_path / "ed.key", tmp_path / "ed.pub"
+    generate_ed25519_keypair(priv, pub)
+    with pytest.raises(SlhDsaError):
+        sign_payload_slhdsa(b"x", priv)
+
+
+def test_head_carries_separate_slh_dsa_block(tmp_path):
+    """make_signed_tree_head with an SLH-DSA key: both signatures verify, the
+    ml_dsa slot is UNTOUCHED, and without a key the slot degrades honestly."""
+    from pacta.signing import generate_ed25519_keypair, verify_payload_ed25519_detailed
+    from pacta.slhdsa import verify_payload_slhdsa
+    from pacta.transparency import make_signed_tree_head, signed_tree_head_payload
+
+    ed_priv, ed_pub = tmp_path / "ed.key", tmp_path / "ed.pub"
+    generate_ed25519_keypair(ed_priv, ed_pub)
+    slh_priv, slh_pub = _keypair(tmp_path)
+
+    sth = make_signed_tree_head("00" * 32, 19, "11" * 32, "2026-08-06T00:00:00Z",
+                                ed_priv, ed_pub,
+                                slhdsa_private_key_path=slh_priv,
+                                slhdsa_public_key_path=slh_pub)
+    payload = signed_tree_head_payload(sth)
+
+    ed = sth["signatures"]["ed25519"]
+    ok, err, _backend = verify_payload_ed25519_detailed(payload, ed["signature_base64"], ed_pub)
+    assert ok, err
+
+    slh = sth["signatures"]["slh_dsa"]
+    assert slh["status"] == "signed"
+    assert slh["parameter_set"] == "SLH-DSA-SHA2-128s"
+    assert slh["mode"] == "deterministic"
+    ok, err = verify_payload_slhdsa(payload, slh["signature_base64"], slh_pub)
+    assert ok, err
+
+    # ml_dsa stays exactly the honest disclosure it always was
+    assert sth["signatures"]["ml_dsa"]["status"] in {"not_configured", "unavailable"}
+    assert "signature_base64" not in sth["signatures"]["ml_dsa"]
+
+    # additive: no key => honest not-configured slot, never an error
+    bare = make_signed_tree_head("00" * 32, 19, "11" * 32, "2026-08-06T00:00:00Z",
+                                 ed_priv, ed_pub)
+    assert bare["signatures"]["slh_dsa"]["status"] == "not_configured"
+
+    # and the payload is unchanged by the slh_dsa presence: signatures are
+    # outside the signed bytes for BOTH algorithms
+    assert signed_tree_head_payload(bare) == payload
+
+
+def test_block_is_json_serialisable(tmp_path):
+    from pacta.slhdsa import slh_dsa_signature_block
+    priv, pub = _keypair(tmp_path)
+    block = slh_dsa_signature_block(b"payload", priv, pub)
+    json.dumps(block)
+    assert set(block) >= {"scheme", "standard", "parameter_set", "mode", "status",
+                          "payload_digest_sha256", "signature_base64",
+                          "public_key_fingerprint_sha256"}