diff --git a/.github/hooks/validate-k9.sh b/.github/hooks/validate-k9.sh
index c83e2908..955c6c8d 100755
--- a/.github/hooks/validate-k9.sh
+++ b/.github/hooks/validate-k9.sh
@@ -2,356 +2,65 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# validate-k9.sh — K9 configuration file validation script
+# validate-k9.sh — pre-push K9 check, through the canonical validator.
 #
-# Scans for .k9 and .k9.ncl files and validates:
-#   1. K9! magic number on line 1
-#   2. Pedigree block presence with required fields (name, version)
-#   3. Security level is one of: kennel, yard, hunt (case-insensitive)
-#   4. Hunt-level files must have a signature or signature_required field
-#   5. SPDX-License-Identifier header presence
+# One validator per family (hyperpolymath/standards,
+# docs/CONTRACTILE-DESCRIPTILE-VALIDATION.adoc): the grep checks that used to
+# live here were a second validator, and they accepted files that contract
+# v1.0.0 (D173) rejects. This runs 1-formats/k9/tools/k9-validate.sh from a
+# standards checkout over the tracked K9 files, strict, layers L0–L2 (L0–L1
+# when nickel is not installed), as the k9-conformance lane does in CI (.github/workflows/dogfood-gate.yml). The lane
+# is the gate; this is the early warning.
 #
 # Environment variables:
-#   INPUT_PATH   — Directory to scan (default: .)
-#   INPUT_STRICT — Promote warnings to errors (default: false)
+#   INPUT_PATH     — Repository to check (default: .)
+#   STANDARDS_DIR  — A hyperpolymath/standards checkout
+#                    (default: ../standards beside the repository)
 #
 # Exit codes:
-#   0 — All files valid (or only warnings in non-strict mode)
-#   1 — Validation errors found
+#   0 — Every tracked K9 file passes, or no validator is available (skipped
+#       with a notice: CI still runs the lane)
+#   1 — A file failed
 
 set -euo pipefail
 
-# ---------------------------------------------------------------------------
-# Configuration
-# ---------------------------------------------------------------------------
+REPO="${INPUT_PATH:-.}"
+STANDARDS_DIR="${STANDARDS_DIR:-$(cd "$REPO/.." && pwd)/standards}"
+case "$STANDARDS_DIR" in
+    /*) ;;
+    *) STANDARDS_DIR="$PWD/$STANDARDS_DIR" ;;
+esac
+VALIDATOR="$STANDARDS_DIR/1-formats/k9/tools/k9-validate.sh"
 
-SCAN_PATH="${INPUT_PATH:-.}"
-STRICT="${INPUT_STRICT:-false}"
-PATHS_IGNORE_RAW="${INPUT_PATHS_IGNORE:-}"
-GITHUB_OUTPUT_FILE="${GITHUB_OUTPUT:-/dev/null}"
-
-# Parse paths-ignore: newline-separated fragments, blank lines and # comments
-# stripped. Each fragment is a substring match against the file path. Pattern
-# adopted from hyperpolymath/hypatia#243 — content-pattern validators must
-# distinguish a target from a vendored / fixture file that legitimately
-# contains the very pattern being checked.
-PATHS_IGNORE=()
-while IFS= read -r _frag; do
-    # Strip leading and trailing whitespace (canonical bash idiom).
-    _frag="${_frag#"${_frag%%[![:space:]]*}"}"
-    _frag="${_frag%"${_frag##*[![:space:]]}"}"
-    [[ -z "$_frag" || "$_frag" == \#* ]] && continue
-    PATHS_IGNORE+=("$_frag")
-done <<< "$PATHS_IGNORE_RAW"
-
-# Returns 0 if path should be skipped (matches any ignore fragment)
-path_ignored() {
-    local p="$1" frag
-    for frag in "${PATHS_IGNORE[@]}"; do
-        [[ "$p" == *"$frag"* ]] && return 0
-    done
-    return 1
-}
-
-# Counters
-FILES_SCANNED=0
-ERRORS=0
-WARNINGS=0
-
-# Valid security levels (the leash metaphor)
-VALID_LEVELS="kennel yard hunt"
-
-# ---------------------------------------------------------------------------
-# Helper: emit GitHub annotation
-# ---------------------------------------------------------------------------
-annotate() {
-    local level="$1" file="$2" line="$3" message="$4"
-    echo "::${level} file=${file},line=${line}::${message}"
-}
-
-# ---------------------------------------------------------------------------
-# Helper: report issue (respects strict mode)
-# ---------------------------------------------------------------------------
-report_issue() {
-    local severity="$1" file="$2" line="$3" message="$4"
-
-    if [[ "$severity" == "warning" && "$STRICT" == "true" ]]; then
-        severity="error"
-    fi
-
-    annotate "$severity" "$file" "$line" "$message"
-
-    if [[ "$severity" == "error" ]]; then
-        ERRORS=$((ERRORS + 1))
-    else
-        WARNINGS=$((WARNINGS + 1))
-    fi
-}
-
-# ---------------------------------------------------------------------------
-# Helper: normalise a security level string
-# ---------------------------------------------------------------------------
-# Strips quotes, leading/trailing whitespace, Nickel enum tick prefix
-normalise_level() {
-    local raw="$1"
-    # Remove surrounding quotes, tick prefix ('Kennel -> Kennel), whitespace
-    raw="${raw#*=}"              # Remove everything before =
-    raw="${raw//\"/}"            # Remove double quotes
-    raw="${raw//\'/}"            # Remove single quotes (Nickel tick)
-    raw="${raw//,/}"             # Remove trailing commas
-    raw="${raw## }"              # Trim leading space
-    raw="${raw%% }"              # Trim trailing space
-    raw="${raw%%#*}"             # Remove inline comments
-    raw="${raw## }"              # Trim again
-    raw="${raw%% }"
-    echo "${raw,,}"             # Lowercase
-}
-
-# ---------------------------------------------------------------------------
-# Validator: check a single K9 file
-# ---------------------------------------------------------------------------
-validate_k9() {
-    local file="$1"
-    FILES_SCANNED=$((FILES_SCANNED + 1))
-
-    # --- Check 1: K9! magic number on first non-empty line ---
-    local first_content_line=""
-    local first_content_line_num=0
-    local line_num=0
-
-    while IFS= read -r line; do
-        line_num=$((line_num + 1))
-        # Skip empty lines
-        if [[ -z "${line// /}" ]]; then
-            continue
-        fi
-        first_content_line="$line"
-        first_content_line_num=$line_num
-        break
-    done < "$file"
-
-    if [[ "$first_content_line" != "K9!" ]]; then
-        report_issue "error" "$file" "$first_content_line_num" \
-            "Missing K9! magic number. First non-empty line must be exactly 'K9!'"
-    fi
-
-    # --- Check 2: SPDX header ---
-    local has_spdx=false
-    line_num=0
-    while IFS= read -r line; do
-        line_num=$((line_num + 1))
-        if [[ $line_num -gt 10 ]]; then
-            break
-        fi
-        if [[ "$line" == *"SPDX-License-Identifier"* ]]; then
-            has_spdx=true
-            break
-        fi
-    done < "$file"
-
-    if [[ "$has_spdx" == "false" ]]; then
-        report_issue "warning" "$file" 1 \
-            "Missing SPDX-License-Identifier in first 10 lines"
-    fi
-
-    # --- Check 3: Pedigree block with required fields ---
-    local has_pedigree=false
-    local has_pedigree_name=false
-    local has_pedigree_version=false
-    local has_security_level=false
-    local security_level_value=""
-    local security_level_line=0
-    local has_signature_field=false
-    local in_pedigree=false
-    local pedigree_depth=0
-
-    line_num=0
-    while IFS= read -r line; do
-        line_num=$((line_num + 1))
-
-        # Detect pedigree block start. Note: do NOT `continue` here — the
-        # `pedigree = {` line itself contains the opening brace that
-        # establishes the block. Falling through to the brace counter
-        # below makes depth start at 1, so a subsequent `security = {…},`
-        # closing brace correctly takes depth to 1 (not 0), keeping us
-        # inside the pedigree block when later fields (name/version/leash)
-        # are checked. Previously the `continue` skipped this opening
-        # brace, depth started at 0, and the first nested block's close
-        # prematurely terminated the validator's view of the pedigree —
-        # making `pedigree.metadata.name` invisible.
-        if [[ "$line" =~ ^[[:space:]]*pedigree[[:space:]]*= ]]; then
-            has_pedigree=true
-            in_pedigree=true
-            pedigree_depth=0
-            # fall through
-        fi
-
-        if [[ "$in_pedigree" == "true" ]]; then
-            # Track brace depth to know when pedigree block ends
-            local opens closes
-            opens="${line//[^\{]/}"
-            closes="${line//[^\}]/}"
-            pedigree_depth=$(( pedigree_depth + ${#opens} - ${#closes} ))
-
-            if [[ $pedigree_depth -le 0 && "$has_pedigree" == "true" ]]; then
-                # Check this final line too before leaving
-                :
-            fi
-
-            # Check for name field within pedigree.metadata or pedigree directly.
-            # Two patterns cover both multi-line and single-line pedigrees:
-            #   1. ^[[:space:]]+name[[:space:]]*= — the normal multi-line case where
-            #      `name = "..."` appears on its own indented line.
-            #   2. [[:space:]]name[[:space:]]*= — inline within a single-line
-            #      pedigree assignment such as:
-            #        pedigree = component_pedigree & { name = "foo" }
-            #      (root cause: developer-ecosystem@baab1534 — single-line form
-            #      was missed entirely because the pedigree block opened and
-            #      closed in one line, never reaching the ^[[:space:]]+ check on
-            #      a subsequent iteration.)
-            if [[ "$line" =~ ^[[:space:]]+name[[:space:]]*= ]] || \
-               [[ "$line" =~ [[:space:]]name[[:space:]]*= ]]; then
-                has_pedigree_name=true
-            fi
-
-            # Check for version field
-            if [[ "$line" =~ ^[[:space:]]+(version|schema_version)[[:space:]]*= ]] || \
-               [[ "$line" =~ [[:space:]](version|schema_version)[[:space:]]*= ]]; then
-                has_pedigree_version=true
-            fi
-
-            # Check for security level (leash field)
-            if [[ "$line" =~ ^[[:space:]]+(leash|security_level)[[:space:]]*= ]]; then
-                has_security_level=true
-                security_level_value="$(normalise_level "$line")"
-                security_level_line=$line_num
-            fi
-
-            # Check for signature fields
-            if [[ "$line" =~ ^[[:space:]]+(signature|signature_required)[[:space:]]*= ]]; then
-                has_signature_field=true
-            fi
-
-            # End of pedigree block
-            if [[ $pedigree_depth -le 0 && "$has_pedigree" == "true" && "$line" == *"}"* ]]; then
-                in_pedigree=false
-            fi
-        fi
-
-        # Also check for signature fields outside pedigree (top-level)
-        if [[ "$line" =~ ^[[:space:]]*(signature)[[:space:]]*= ]]; then
-            has_signature_field=true
-        fi
-    done < "$file"
-
-    if [[ "$has_pedigree" == "false" ]]; then
-        report_issue "error" "$file" 1 \
-            "Missing pedigree block. K9 files must contain a 'pedigree = { ... }' section"
-    else
-        if [[ "$has_pedigree_name" == "false" ]]; then
-            report_issue "error" "$file" 1 \
-                "Pedigree block missing 'name' field (in pedigree.metadata.name or pedigree.name)"
-        fi
-
-        if [[ "$has_pedigree_version" == "false" ]]; then
-            report_issue "warning" "$file" 1 \
-                "Pedigree block missing 'version' or 'schema_version' field"
-        fi
-    fi
-
-    # --- Check 4: Security level validation ---
-    if [[ "$has_security_level" == "true" ]]; then
-        local level_valid=false
-        for valid in $VALID_LEVELS; do
-            if [[ "$security_level_value" == "$valid" ]]; then
-                level_valid=true
-                break
-            fi
-        done
-
-        if [[ "$level_valid" == "false" ]]; then
-            report_issue "error" "$file" "$security_level_line" \
-                "Invalid security level '${security_level_value}'. Must be one of: kennel, yard, hunt"
-        fi
-    else
-        if [[ "$has_pedigree" == "true" ]]; then
-            report_issue "warning" "$file" 1 \
-                "No security level (leash/security_level) found in pedigree block"
-        fi
-    fi
-
-    # --- Check 5: Hunt-level signature requirement ---
-    if [[ "$security_level_value" == "hunt" && "$has_signature_field" == "false" ]]; then
-        report_issue "error" "$file" "$security_level_line" \
-            "Hunt-level K9 file must include a 'signature' or 'signature_required' field"
-    fi
-}
-
-# ---------------------------------------------------------------------------
-# Main: discover and validate K9 files
-# ---------------------------------------------------------------------------
-
-echo "::group::K9 Configuration Validation"
-echo "Scanning ${SCAN_PATH} for K9 files (.k9, .k9.ncl)..."
-echo ""
-
-# Find all K9 files, excluding .git directory
-mapfile -t k9_candidates < <(find "$SCAN_PATH" \( -name '*.k9' -o -name '*.k9.ncl' \) -not -path '*/.git/*' -type f | sort)
-
-# Apply paths-ignore filter
-k9_files=()
-SKIPPED=0
-for _f in "${k9_candidates[@]}"; do
-    if path_ignored "$_f"; then
-        SKIPPED=$((SKIPPED + 1))
-        continue
-    fi
-    k9_files+=("$_f")
-done
+if [ ! -f "$VALIDATOR" ]; then
+    echo "::notice::K9: no standards checkout at $STANDARDS_DIR (set STANDARDS_DIR to run the validator locally); the k9-conformance lane validates in CI"
+    exit 0
+fi
 
-if [[ $SKIPPED -gt 0 ]]; then
-    echo "::notice::Skipped ${SKIPPED} file(s) matching paths-ignore"
+# L2 is the Nickel evaluation against the contract; without nickel the
+# validator reports those checks as SKIPPED and refuses to call that a pass,
+# so stop at L1 here and say so. The lane checks L2 in CI either way.
+LAYER=L2
+if ! command -v nickel >/dev/null 2>&1; then
+    echo "::notice::K9: nickel is not installed, so layer L2 (Nickel semantics) is left to the CI lane; checking L0–L1"
+    LAYER=L1
 fi
 
-if [[ ${#k9_files[@]} -eq 0 ]]; then
-    echo "::notice::No K9 files found in ${SCAN_PATH}"
-    echo "files_scanned=0" >> "$GITHUB_OUTPUT_FILE" 2>/dev/null || true
-    echo "errors=0" >> "$GITHUB_OUTPUT_FILE" 2>/dev/null || true
-    echo "warnings=0" >> "$GITHUB_OUTPUT_FILE" 2>/dev/null || true
-    echo "::endgroup::"
+cd "$REPO"
+mapfile -t files < <(git ls-files -- '*.k9.ncl' '*.k9' '*.k9.lock' | sort)
+if [ "${#files[@]}" -eq 0 ]; then
+    echo "::notice::K9: no tracked K9 file"
     exit 0
 fi
 
-echo "Found ${#k9_files[@]} K9 file(s)"
-echo ""
-
-for file in "${k9_files[@]}"; do
-    echo "  Validating: ${file}"
-    validate_k9 "$file"
+errors=0
+for f in "${files[@]}"; do
+    echo "  Validating: $f"
+    if ! bash "$VALIDATOR" --strict --layer "$LAYER" "$f"; then
+        errors=$((errors + 1))
+    fi
 done
 
-echo ""
-echo "────────────────────────────────────────"
-echo "Files scanned: ${FILES_SCANNED}"
-echo "Errors:        ${ERRORS}"
-echo "Warnings:      ${WARNINGS}"
-echo "Strict mode:   ${STRICT}"
-echo "────────────────────────────────────────"
-
-# Write outputs for GitHub Actions
-{
-    echo "files_scanned=${FILES_SCANNED}"
-    echo "errors=${ERRORS}"
-    echo "warnings=${WARNINGS}"
-} >> "$GITHUB_OUTPUT_FILE" 2>/dev/null || true
-
-echo "::endgroup::"
-
-# Exit with failure if errors were found
-if [[ $ERRORS -gt 0 ]]; then
-    echo "::error::K9 validation failed with ${ERRORS} error(s)"
-    exit 1
-fi
-
+echo "K9: ${#files[@]} file(s), ${errors} failing (validator: $VALIDATOR)"
+[ "$errors" -eq 0 ] || { echo "::error::K9 validation failed for ${errors} file(s)"; exit 1; }
 echo "K9 validation passed."
-exit 0
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 29bd304e..9c3470e7 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -83,51 +83,53 @@ jobs:
   k9-validate:
     name: Validate K9 contracts
     runs-on: ubuntu-latest
-    timeout-minutes: 10
+    timeout-minutes: 15
     outputs:
       validation: ${{ steps.validate.outcome }}
+    env:
+      NICKEL_VERSION: '1.18.0'
+      NICKEL_SHA256: '9cba4dd65ae9915ec61f73033aafcff307a377665a83fd8f530df086763318cb'
 
     steps:
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
 
-      - name: Check for K9 files
-        id: detect
+      - name: Checkout canonical K9 validator and contract
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: metadatastician/standards
+          ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
+          path: .standards-k9
+          sparse-checkout: 1-formats/k9
+          sparse-checkout-cone-mode: true
+          persist-credentials: false
+
+      - name: Install sha256-verified Nickel CLI
         run: |
-          COUNT=$(find . \( -name '*.k9' -o -name '*.k9.ncl' \) -not -path './.git/*' | wc -l)
-          CONFIG_COUNT=$(find . \( -name '*.toml' -o -name '*.yaml' -o -name '*.yml' -o -name '*.json' \) \
-            -not -path './.git/*' -not -path './node_modules/*' -not -path './.deno/*' \
-            -not -name 'package-lock.json' -not -name 'Cargo.lock' -not -name 'deno.lock' | wc -l)
-          echo "k9_count=$COUNT" >> "$GITHUB_OUTPUT"
-          echo "config_count=$CONFIG_COUNT" >> "$GITHUB_OUTPUT"
-          if [ "$COUNT" -eq 0 ] && [ "$CONFIG_COUNT" -gt 0 ]; then
-            echo "::warning::Found $CONFIG_COUNT config files but no K9 contracts. Run k9iser to generate contracts."
-          fi
+          set -euo pipefail
+          URL="https://github.com/tweag/nickel/releases/download/${NICKEL_VERSION}/nickel-x86_64-linux"
+          curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 --retry 3 -o "$RUNNER_TEMP/nickel" "$URL"
+          echo "${NICKEL_SHA256}  ${RUNNER_TEMP}/nickel" | sha256sum -c -
+          chmod +x "$RUNNER_TEMP/nickel"
+          echo "$RUNNER_TEMP" >> "$GITHUB_PATH"
 
-      - name: Validate K9 contracts
+      - name: Validate K9 contracts (L0–L2)
         id: validate
-        if: steps.detect.outputs.k9_count > 0
-        env:
-          INPUT_STRICT: "true"
-        run: bash .github/hooks/validate-k9.sh
-      - name: Write summary
         run: |
-          K9_COUNT="${{ steps.detect.outputs.k9_count }}"
-          CFG_COUNT="${{ steps.detect.outputs.config_count }}"
-          if [ "$K9_COUNT" -eq 0 ]; then
-            cat <<'EOF' >> "$GITHUB_STEP_SUMMARY"
-          ## K9 Contract Validation
-
-          :warning: **No K9 contracts found.** Structural K9 validation was not run.
-
-          Generate contracts with: `k9iser generate .`
-          EOF
-          else
-            echo "## K9 Contract Validation" >> "$GITHUB_STEP_SUMMARY"
-            echo "" >> "$GITHUB_STEP_SUMMARY"
-            echo "Checked structural fields in **${K9_COUNT}** K9 contract(s). The repository contains **${CFG_COUNT}** configuration file(s); this hook does not compare their contents with the contracts." >> "$GITHUB_STEP_SUMMARY"
-            echo "This is not Nickel evaluation, cryptographic signature verification or Hunt deployment authorization." >> "$GITHUB_STEP_SUMMARY"
+          set -euo pipefail
+          rm -rf "$RUNNER_TEMP/standards-k9"
+          mv "$PWD/.standards-k9" "$RUNNER_TEMP/standards-k9"
+          if [ ! -f "$RUNNER_TEMP/standards-k9/1-formats/k9/tools/k9-validate.sh" ]; then
+            echo "::error::K9 validator is missing from the standards checkout"
+            exit 1
+          fi
+          if ! command -v nickel >/dev/null 2>&1; then
+            echo "::error::nickel is required for K9 layer L2 validation"
+            exit 1
           fi
+          STANDARDS_DIR="$RUNNER_TEMP/standards-k9" bash .github/hooks/validate-k9.sh
 
   # ---------------------------------------------------------------------------
   # Job 3: Empty-linter — invisible character detection
diff --git a/.machine_readable/contractiles/README.adoc b/.machine_readable/contractiles/README.adoc
index 07d79151..5034d402 100644
--- a/.machine_readable/contractiles/README.adoc
+++ b/.machine_readable/contractiles/README.adoc
@@ -30,9 +30,10 @@ coherence manifest:
   actual invariants / trust actions / tolerances / intents).
 * `<verb>.ncl` — the paired Nickel *runner* (pedigree + schema + run
   policy). Imports `../_base.ncl`.
-* `<verb>.k9.ncl` — the *K9 trust-tier component* (execution surface,
-  evidence sinks, session-open/close negotiation). Imports the Hunt
-  base via `../k9/template-hunt.k9.ncl` and `../_base.ncl`.
+* `<verb>.k9.ncl` — the *K9 component* (K9 contract v1.0.0, D173): a
+  declaration evaluated at 'Yard. It records evidence sinks and
+  session-open/close negotiation; the paired runner is the execution
+  surface, so this record spawns nothing. Imports `../_base.ncl`.
 * `<verb>.manifest.a2ml` — the *trident coherence manifest* (file roles,
   cross-refs, signature, history).
 
@@ -125,14 +126,14 @@ no paired xfile is non-conformant.
 
 [NOTE]
 ====
-*Local k9-base status.* Echidna's three trust-tier templates currently
-live under `../svc/k9/` (`template-kennel.k9.ncl`, `template-yard.k9.ncl`,
-`template-hunt.k9.ncl`). The per-verb `<verb>.k9.ncl` components import the
-canonical `../k9/template-hunt.k9.ncl` base path used estate-wide; that
-shared Hunt base is a known estate-level gap (the same import is unresolved
-in `standards`) and is tracked by the machine-readable respec programme
-rather than patched per-repo here. The runner `.ncl` files (which import
-only `_base.ncl`) `nickel typecheck` clean.
+*Validation.* Every `<verb>.k9.ncl` passes the canonical validator
+(`metadatastician/standards` `1-formats/k9/tools/k9-validate.sh --strict`,
+layers L0–L2), run by the `k9-validate` job in `dogfood-gate.yml` through
+`.github/hooks/validate-k9.sh`. The former import of an estate-wide
+`../k9/template-hunt.k9.ncl` base never resolved and has been removed, as
+rsr-template-repo did. Echidna's templates for new components are
+`../svc/k9/template-{kennel,yard,hunt}.k9.ncl.in`: they carry unfilled
+placeholders, so they are not components and are not validated.
 ====
 
 == Fill-in / maintenance rules
diff --git a/.machine_readable/contractiles/adjust/adjust.k9.ncl b/.machine_readable/contractiles/adjust/adjust.k9.ncl
index 4974ba7f..f0b120bd 100644
--- a/.machine_readable/contractiles/adjust/adjust.k9.ncl
+++ b/.machine_readable/contractiles/adjust/adjust.k9.ncl
@@ -22,12 +22,24 @@ K9!
 # erosion causing gradual parameter drift). Where must flags "broken
 # now", adjust flags "drifting toward broken".
 
-let base_k9 = import "../k9/template-hunt.k9.ncl" in
+#
+# 2026-11-09 (K9 contract v1.0.0, D173, standards#1058): this record is a
+# DECLARATION evaluated at 'Yard. The probes it lists are run by the paired
+# runner (adjust.ncl and the scripts/run-*.sh runners), which is the execution
+# surface; this file spawns nothing. A 'Hunt record needs signature_required,
+# a signature block and a verified signature (K9-S008/S009/C001); no
+# contractile carries one, so 'Hunt here was a claim the gate could never honour.
+# Mirrors rsr-template-repo's contractiles (WO-9).
+
 let base    = import "../_base.ncl" in
 
 {
-  pedigree = base_k9.pedigree_schema & {
+  pedigree = base.pedigree_schema & {
     contractile_verb = "adjust",
+    schema_version   = "1.0.0",
+    component_type   = "contractile:adjust",
+    semantics        = "drift tolerances + corrective actions",
+    side_effects     = [],
     paired_xfile     = "../adjust/Adjustfile.a2ml",
     paired_runner    = "../adjust/adjust.ncl",
 
@@ -48,12 +60,13 @@ let base    = import "../_base.ncl" in
       trust_level = "tolerance measurement + declared auto-fix",
       allow_network = false,
       allow_filesystem_write_conditional = true,  # auto_fix_when_available may edit
-      allow_subprocess = true,
+      allow_subprocess = false,   # the paired runner spawns; this record does not
       probe_scope = 'measurement_plus_declared_fix,
     },
   },
 
-  variance_schema = {
+  # A record SHAPE (contract-only fields, no values): kept out of `nickel export`.
+  variance_schema | not_exported = {
     entry_id     | String,
     reason       | String,
     approved_by  | String,
diff --git a/.machine_readable/contractiles/bust/bust.k9.ncl b/.machine_readable/contractiles/bust/bust.k9.ncl
index 0740076b..ce5e6e93 100644
--- a/.machine_readable/contractiles/bust/bust.k9.ncl
+++ b/.machine_readable/contractiles/bust/bust.k9.ncl
@@ -23,16 +23,28 @@ K9!
 # (invariant) and trust (cleanliness) as the third blocking verb in the
 # (Hunt, blocking) triple.
 
-let base_k9 = import "../k9/template-hunt.k9.ncl" in
+#
+# 2026-11-09 (K9 contract v1.0.0, D173, standards#1058): this record is a
+# DECLARATION evaluated at 'Yard. The probes it lists are run by the paired
+# runner (bust.ncl and the scripts/run-*.sh runners), which is the execution
+# surface; this file spawns nothing. A 'Hunt record needs signature_required,
+# a signature block and a verified signature (K9-S008/S009/C001); no
+# contractile carries one, so 'Hunt here was a claim the gate could never honour.
+# Mirrors rsr-template-repo's contractiles (WO-9).
+
 let base    = import "../_base.ncl" in
 
 {
-  pedigree = base_k9.pedigree_schema & {
+  pedigree = base.pedigree_schema & {
     contractile_verb = "bust",
+    schema_version   = "1.0.0",
+    component_type   = "contractile:bust",
+    semantics        = "hard-stop / expiry / must-not-run declarations",
+    side_effects     = [],
     paired_xfile     = "../bust/Bustfile.a2ml",
     paired_runner    = "../bust/bust.ncl",
 
-    tier      = 'Hunt,
+    tier      = 'Yard,
     authority = 'blocking,
 
     metadata = {
@@ -45,20 +57,18 @@ let base    = import "../_base.ncl" in
     },
 
     security = {
-      leash = 'Hunt,
+      leash = 'Yard,
+      signature_required = false,
       trust_level = "controlled failure injection; scoped to system-under-test",
       allow_network = false,
-      allow_filesystem_write = true,      # drills may write transient state (tmp dirs, test DBs)
-      allow_subprocess = true,
+      allow_filesystem_write = false,     # the runner's drills write transient state (tmp dirs, test DBs); this record does not
+      allow_subprocess = false,   # the paired runner spawns; this record does not
       injection_scope = 'system_under_test_only,
-      # Hunt-tier files must declare whether a cryptographic signature
-      # is required. Bust trident runs in CI on every PR; signatures
-      # are enforced at the trident-runner layer, not in-band.
-      signature_required = true,
     },
   },
 
-  variance_schema = {
+  # A record SHAPE (contract-only fields, no values): kept out of `nickel export`.
+  variance_schema | not_exported = {
     entry_id           | String,
     reason             | String,
     approved_by        | String,
diff --git a/.machine_readable/contractiles/dust/dust.k9.ncl b/.machine_readable/contractiles/dust/dust.k9.ncl
index be922a49..c05f2402 100644
--- a/.machine_readable/contractiles/dust/dust.k9.ncl
+++ b/.machine_readable/contractiles/dust/dust.k9.ncl
@@ -30,12 +30,24 @@ K9!
 # previous existence — e.g. D040-D042 archive rather than delete; the
 # PR is the durable record for D001/D002; git history covers D050-D052).
 
-let base_k9 = import "../k9/template-hunt.k9.ncl" in
+#
+# 2026-11-09 (K9 contract v1.0.0, D173, standards#1058): this record is a
+# DECLARATION evaluated at 'Yard. The probes it lists are run by the paired
+# runner (dust.ncl and the scripts/run-*.sh runners), which is the execution
+# surface; this file spawns nothing. A 'Hunt record needs signature_required,
+# a signature block and a verified signature (K9-S008/S009/C001); no
+# contractile carries one, so 'Hunt here was a claim the gate could never honour.
+# Mirrors rsr-template-repo's contractiles (WO-9).
+
 let base    = import "../_base.ncl" in
 
 {
-  pedigree = base_k9.pedigree_schema & {
+  pedigree = base.pedigree_schema & {
     contractile_verb = "dust",
+    schema_version   = "1.0.0",
+    component_type   = "contractile:dust",
+    semantics        = "rollback / recovery / deprecation / audit-trail preservation",
+    side_effects     = [],
     paired_xfile     = "../dust/Dustfile.a2ml",
     paired_runner    = "../dust/dust.ncl",
 
@@ -60,7 +72,7 @@ let base    = import "../_base.ncl" in
       # orphan pids/caches, archive prior-run artefacts) — but only
       # behind explicit --apply flag + per-item approval. Default is dry-run.
       allow_filesystem_write_conditional = true,
-      allow_subprocess = true,
+      allow_subprocess = false,   # the paired runner spawns; this record does not
       destructive_action_gating = {
         default_mode = 'dry_run,
         requires_flag = "--apply",
@@ -80,7 +92,8 @@ let base    = import "../_base.ncl" in
     },
   },
 
-  variance_schema = {
+  # A record SHAPE (contract-only fields, no values): kept out of `nickel export`.
+  variance_schema | not_exported = {
     entry_id     | String,
     reason       | String,
     approved_by  | String,
diff --git a/.machine_readable/contractiles/intend/intend.k9.ncl b/.machine_readable/contractiles/intend/intend.k9.ncl
index 6c7d454a..f16a4192 100644
--- a/.machine_readable/contractiles/intend/intend.k9.ncl
+++ b/.machine_readable/contractiles/intend/intend.k9.ncl
@@ -33,12 +33,24 @@ K9!
 # * Evidence sinks: VeriSimDB (queryable) + descriptiles/DRIFT.a2ml (repo-local).
 # * Failure-mode defenses cross-referenced to the AI failure catalog.
 
-let base_k9 = import "../k9/template-hunt.k9.ncl" in
+#
+# 2026-11-09 (K9 contract v1.0.0, D173, standards#1058): this record is a
+# DECLARATION evaluated at 'Yard. The probes it lists are run by the paired
+# runner (intend.ncl and the scripts/run-*.sh runners), which is the execution
+# surface; this file spawns nothing. A 'Hunt record needs signature_required,
+# a signature block and a verified signature (K9-S008/S009/C001); no
+# contractile carries one, so 'Hunt here was a claim the gate could never honour.
+# Mirrors rsr-template-repo's contractiles (WO-9).
+
 let base    = import "../_base.ncl" in
 
 {
-  pedigree = base_k9.pedigree_schema & {
+  pedigree = base.pedigree_schema & {
     contractile_verb = "intend",
+    schema_version   = "1.0.0",
+    component_type   = "contractile:intend",
+    semantics        = "north-star (commitments + aspirations)",
+    side_effects     = [],
     paired_xfile     = "../intend/Intentfile.a2ml",
     paired_runner    = "../intend/intend.ncl",
 
@@ -48,7 +60,7 @@ let base    = import "../_base.ncl" in
     # adjust/dust declare (Yard, advisory). Splitting the axes
     # means "I'm Hunt-tier so I can override everything" is structurally
     # impossible — authority is a separate field.
-    tier      = 'Hunt,
+    tier      = 'Yard,
     authority = 'reporting,
 
     metadata = {
@@ -65,12 +77,12 @@ let base    = import "../_base.ncl" in
     },
 
     security = {
-      leash = 'Hunt,
-      signature_required = true,
+      leash = 'Yard,
+      signature_required = false,
       trust_level = "subprocess + filesystem-read",
       allow_network = false,
       allow_filesystem_write = false,   # evidence sinks are indirected
-      allow_subprocess = true,
+      allow_subprocess = false,   # the paired runner spawns; this record does not
     },
   },
 
@@ -83,7 +95,8 @@ let base    = import "../_base.ncl" in
   # Per user 2026-04-18: variances are structural, not magic-comment
   # markers — markers are gameable.
   # -------------------------------------------------------------------
-  variance_schema = {
+  # A record SHAPE (contract-only fields, no values): kept out of `nickel export`.
+  variance_schema | not_exported = {
     entry_id     | String,   # which intent/wish id the variance applies to
     reason       | String,
     approved_by  | String,
diff --git a/.machine_readable/contractiles/must/must.k9.ncl b/.machine_readable/contractiles/must/must.k9.ncl
index 05d9e06e..1a00b8a7 100644
--- a/.machine_readable/contractiles/must/must.k9.ncl
+++ b/.machine_readable/contractiles/must/must.k9.ncl
@@ -38,19 +38,31 @@ K9!
 # against marketing copy about prover counts) and D1 (lore fabrication
 # about what the repo contains).
 
-let base_k9 = import "../k9/template-hunt.k9.ncl" in
+#
+# 2026-11-09 (K9 contract v1.0.0, D173, standards#1058): this record is a
+# DECLARATION evaluated at 'Yard. The probes it lists are run by the paired
+# runner (must.ncl and the scripts/run-*.sh runners), which is the execution
+# surface; this file spawns nothing. A 'Hunt record needs signature_required,
+# a signature block and a verified signature (K9-S008/S009/C001); no
+# contractile carries one, so 'Hunt here was a claim the gate could never honour.
+# Mirrors rsr-template-repo's contractiles (WO-9).
+
 let base    = import "../_base.ncl" in
 
 {
-  pedigree = base_k9.pedigree_schema & {
+  pedigree = base.pedigree_schema & {
     contractile_verb = "must",
+    schema_version   = "1.0.0",
+    component_type   = "contractile:must",
+    semantics        = "invariant assertion — release-blocking",
+    side_effects     = [],
     paired_xfile     = "../must/Mustfile.a2ml",
     paired_runner    = "../must/must.ncl",
 
-    # α two-axis: Hunt tier (subprocess for grep/test/etc.) but
-    # restricted to read-only operations. Blocking authority because
+    # α two-axis: Yard tier (the runner shells out for grep/test/etc.;
+    # this record only declares) and read-only operations. Blocking authority because
     # must is the canonical gating verb.
-    tier      = 'Hunt,
+    tier      = 'Yard,
     authority = 'blocking,
 
     metadata = {
@@ -63,16 +75,13 @@ let base    = import "../_base.ncl" in
     },
 
     security = {
-      leash = 'Hunt,
+      leash = 'Yard,
+      signature_required = false,
       trust_level = "read-only invariant verification with subprocess",
       allow_network = false,
       allow_filesystem_write = false,
-      allow_subprocess = true,
+      allow_subprocess = false,   # the paired runner spawns; this record does not
       probe_scope = 'read_only,              # must probes NEVER mutate
-      # Hunt-tier files must declare whether a cryptographic signature
-      # is required. The must trident runs in CI on every PR; signatures
-      # are enforced at the trident-runner layer, not in-band.
-      signature_required = true,
       probe_kinds_allowed = [
         'file_existence,
         'pattern_presence,
@@ -95,7 +104,8 @@ let base    = import "../_base.ncl" in
   # Because must is BLOCKING, variances carry real weight. Critical-
   # severity invariants can only be varied by maintainer-or-above.
   # -------------------------------------------------------------------
-  variance_schema = {
+  # A record SHAPE (contract-only fields, no values): kept out of `nickel export`.
+  variance_schema | not_exported = {
     entry_id     | String,   # which invariant id the variance applies to
     reason       | String,
     approved_by  | String,   # maintainer or above for critical-severity
diff --git a/.machine_readable/contractiles/trust/trust.k9.ncl b/.machine_readable/contractiles/trust/trust.k9.ncl
index c253021a..5c1f02d6 100644
--- a/.machine_readable/contractiles/trust/trust.k9.ncl
+++ b/.machine_readable/contractiles/trust/trust.k9.ncl
@@ -36,12 +36,24 @@ K9!
 # Licence findings (T001) are FLAG-ONLY: never auto-edit — see
 # [[feedback_no_automated_licence_edits]].
 
-let base_k9 = import "../k9/template-hunt.k9.ncl" in
+#
+# 2026-11-09 (K9 contract v1.0.0, D173, standards#1058): this record is a
+# DECLARATION evaluated at 'Yard. The probes it lists are run by the paired
+# runner (trust.ncl and the scripts/run-*.sh runners), which is the execution
+# surface; this file spawns nothing. A 'Hunt record needs signature_required,
+# a signature block and a verified signature (K9-S008/S009/C001); no
+# contractile carries one, so 'Hunt here was a claim the gate could never honour.
+# Mirrors rsr-template-repo's contractiles (WO-9).
+
 let base    = import "../_base.ncl" in
 
 {
-  pedigree = base_k9.pedigree_schema & {
+  pedigree = base.pedigree_schema & {
     contractile_verb = "trust",
+    schema_version   = "1.0.0",
+    component_type   = "contractile:trust",
+    semantics        = "security + provenance + safe-hacking",
+    side_effects     = [],
     paired_xfile     = "../trust/Trustfile.a2ml",
     paired_runner    = "../trust/trust.ncl",
 
@@ -49,7 +61,7 @@ let base    = import "../_base.ncl" in
     # fuzz/injection/auth-bypass/sandbox-escape attempts scoped to the repo)
     # AND blocking-authority (failed verification = failed CI). Completes the
     # (Hunt, blocking) triple with must + bust.
-    tier      = 'Hunt,
+    tier      = 'Yard,
     authority = 'blocking,
 
     metadata = {
@@ -62,20 +74,17 @@ let base    = import "../_base.ncl" in
     },
 
     security = {
-      leash = 'Hunt,
+      leash = 'Yard,
+      signature_required = false,
       trust_level = "verification + authorised-probe + hard-gate",
       allow_network = false,            # verifications offline by default
       allow_filesystem_write = false,   # evidence sinks are indirected
-      allow_subprocess = true,
+      allow_subprocess = false,   # the paired runner spawns; this record does not
       authorised_probes_only = true,    # probe section explicitly lists allowed targets + probe classes
       probe_scope_enforcement = 'this_repo_only,  # probes NEVER hit external systems
       # echidna-bespoke: the dispatcher trust boundary trust enforces.
       dispatcher_trust_boundary = "no-proof-emits-without-axiom-track-integrity-sandbox",
       error_namespace = "T###",
-      # Hunt-tier files must declare whether a cryptographic signature is
-      # required. trust trident runs in CI on every PR; signatures are
-      # enforced at the trident-runner layer, not in-band.
-      signature_required = true,
     },
   },
 
@@ -86,7 +95,8 @@ let base    = import "../_base.ncl" in
   # entries — the variance approver MUST be the repo maintainer or above
   # for critical-severity entries (T001/T002/T010/T020/T030/T040/T050/T051).
   # -------------------------------------------------------------------
-  variance_schema = {
+  # A record SHAPE (contract-only fields, no values): kept out of `nickel export`.
+  variance_schema | not_exported = {
     entry_id     | String,   # which T### verification / probe id
     reason       | String,
     approved_by  | String,   # maintainer or above for critical entries
diff --git a/.machine_readable/setup-prover-env.k9.ncl b/.machine_readable/setup-prover-env.k9.ncl
index 4354ae8b..74877f4d 100644
--- a/.machine_readable/setup-prover-env.k9.ncl
+++ b/.machine_readable/setup-prover-env.k9.ncl
@@ -1,302 +1,126 @@
 K9!
 # SPDX-License-Identifier: MPL-2.0
-# ECHIDNA Theorem Prover Environment Setup
+# setup-prover-env.k9.ncl — ECHIDNA prover environment setup (Hunt level)
 #
-# This K9 component automates the installation and configuration of ECHIDNA's
-# 12 theorem prover backends, including Agda, Coq, Lean, Isabelle, Z3, CVC5,
-# Metamath, HOL Light, Mizar, PVS, ACL2, and HOL4.
-
-pedigree = {
-  name = "setup-prover-env",
-  version = "1.0.0",
-  leash = 'Hunt,
-  signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT",
-  schema_version = "1.0.0",
-  component_type = "prover-env-setup",
-  author = "Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>",
-  description = "Automated setup of 12 theorem prover environments for ECHIDNA",
-  created = "2026-01-30",
-  k9_spec_version = "1.0.0",
-}
-
-config = {
-  # Prover tier selection
-  install_tiers = {
-    tier1 | Bool = true,   # Agda, Coq, Lean, Isabelle, Z3, CVC5
-    tier2 | Bool = true,   # Metamath, HOL Light, Mizar
-    tier3 | Bool = false,  # PVS, ACL2 (heavier dependencies)
-    tier4 | Bool = false,  # HOL4 (legacy)
-  },
-
-  # Installation method preferences
-  install_methods = {
-    prefer_package_manager | Bool = true,  # Use system package manager when possible
-    use_containers | Bool = false,          # Isolate provers in containers
-    build_from_source | [| 'Never, 'IfNeeded, 'Always |] = 'IfNeeded,
-  },
-
-  # Container runtime (if use_containers = true)
-  container_runtime | [| 'Podman, 'Docker |] = 'Podman,
-
-  # Prover-specific configurations
-  provers = {
-    agda = { enabled | Bool = true, version | String = "2.6.4" },
-    coq = { enabled | Bool = true, version | String = "8.18" },
-    lean = { enabled | Bool = true, version | String = "4.4.0" },
-    isabelle = { enabled | Bool = true, version | String = "2023" },
-    z3 = { enabled | Bool = true, version | String = "4.12.5" },
-    cvc5 = { enabled | Bool = true, version | String = "1.1.1" },
-    metamath = { enabled | Bool = true, version | String = "0.198" },
-    hol_light = { enabled | Bool = true, version | String = "latest" },
-    mizar = { enabled | Bool = true, version | String = "8.1.11" },
-    pvs = { enabled | Bool = false, version | String = "7.1" },
-    acl2 = { enabled | Bool = false, version | String = "8.5" },
-    hol4 = { enabled | Bool = false, version | String = "latest" },
-  },
-
-  # Installation paths
-  paths = {
-    install_dir | String = "$HOME/.echidna/provers",
-    container_volumes | String = "$HOME/.echidna/volumes",
-    config_dir | String = "$HOME/.config/echidna",
-  },
-
-  # Testing
-  run_smoke_tests | Bool = true,
-  verify_integration | Bool = true,
-}
-
-# Prover installation recipes
-prover_recipes = {
-  agda = {
-    description = "Install Agda (dependent type theory)",
-    enabled = config.provers.agda.enabled && config.install_tiers.tier1,
-    commands = [
-      "echo 'Installing Agda %{config.provers.agda.version}...'",
-      "if command -v agda >/dev/null 2>&1; then echo 'Agda already installed'; else " ++
-        "if [ %{std.string.from config.install_methods.prefer_package_manager} = 'true' ]; then " ++
-          "if command -v dnf >/dev/null 2>&1; then sudo dnf install -y agda; " ++
-          "elif command -v apt-get >/dev/null 2>&1; then sudo apt-get install -y agda; " ++
-          "else echo 'Installing via cabal...'; cabal install Agda; fi; " ++
-        "else cabal install Agda; fi; " ++
-      "fi",
-      "agda --version",
-    ],
-  },
-
-  coq = {
-    description = "Install Coq/Rocq (interactive theorem prover)",
-    enabled = config.provers.coq.enabled && config.install_tiers.tier1,
-    commands = [
-      "echo 'Installing Coq %{config.provers.coq.version}...'",
-      "if command -v coqc >/dev/null 2>&1; then echo 'Coq already installed'; else " ++
-        "if [ %{std.string.from config.install_methods.prefer_package_manager} = 'true' ]; then " ++
-          "if command -v dnf >/dev/null 2>&1; then sudo dnf install -y coq; " ++
-          "elif command -v apt-get >/dev/null 2>&1; then sudo apt-get install -y coq; " ++
-          "else echo 'Installing via opam...'; opam install coq.%{config.provers.coq.version}; fi; " ++
-        "else opam install coq.%{config.provers.coq.version}; fi; " ++
-      "fi",
-      "coqc --version",
-    ],
-  },
-
-  lean = {
-    description = "Install Lean 4 (functional programming and proving)",
-    enabled = config.provers.lean.enabled && config.install_tiers.tier1,
-    commands = [
-      "echo 'Installing Lean %{config.provers.lean.version}...'",
-      "if command -v lean >/dev/null 2>&1; then echo 'Lean already installed'; else " ++
-        "curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y; " ++
-        "source $HOME/.elan/env; " ++
-        "elan default leanprover/lean4:%{config.provers.lean.version}; " ++
-      "fi",
-      "lean --version",
-    ],
-  },
-
-  isabelle = {
-    description = "Install Isabelle (higher-order logic)",
-    enabled = config.provers.isabelle.enabled && config.install_tiers.tier1,
-    commands = [
-      "echo 'Installing Isabelle %{config.provers.isabelle.version}...'",
-      "if [ ! -d %{config.paths.install_dir}/isabelle ]; then " ++
-        "mkdir -p %{config.paths.install_dir}; " ++
-        "cd %{config.paths.install_dir}; " ++
-        "wget https://isabelle.in.tum.de/website-Isabelle%{config.provers.isabelle.version}/dist/Isabelle%{config.provers.isabelle.version}_linux.tar.gz; " ++
-        "tar xzf Isabelle%{config.provers.isabelle.version}_linux.tar.gz; " ++
-        "ln -sf %{config.paths.install_dir}/Isabelle%{config.provers.isabelle.version}/bin/isabelle $HOME/.local/bin/isabelle; " ++
-      "fi",
-      "isabelle version",
-    ],
-  },
-
-  z3 = {
-    description = "Install Z3 (SMT solver)",
-    enabled = config.provers.z3.enabled && config.install_tiers.tier1,
-    commands = [
-      "echo 'Installing Z3 %{config.provers.z3.version}...'",
-      "if command -v z3 >/dev/null 2>&1; then echo 'Z3 already installed'; else " ++
-        "if [ %{std.string.from config.install_methods.prefer_package_manager} = 'true' ]; then " ++
-          "if command -v dnf >/dev/null 2>&1; then sudo dnf install -y z3; " ++
-          "elif command -v apt-get >/dev/null 2>&1; then sudo apt-get install -y z3; fi; " ++
-        "else " ++
-          "mkdir -p %{config.paths.install_dir}; " ++
-          "cd %{config.paths.install_dir}; " ++
-          "wget https://github.com/Z3Prover/z3/releases/download/z3-%{config.provers.z3.version}/z3-%{config.provers.z3.version}-x64-glibc-2.31.zip; " ++
-          "unzip z3-%{config.provers.z3.version}-x64-glibc-2.31.zip; " ++
-          "ln -sf %{config.paths.install_dir}/z3-%{config.provers.z3.version}-x64-glibc-2.31/bin/z3 $HOME/.local/bin/z3; " ++
-        "fi; " ++
-      "fi",
-      "z3 --version",
-    ],
-  },
-
-  cvc5 = {
-    description = "Install CVC5 (SMT solver)",
-    enabled = config.provers.cvc5.enabled && config.install_tiers.tier1,
-    commands = [
-      "echo 'Installing CVC5 %{config.provers.cvc5.version}...'",
-      "if command -v cvc5 >/dev/null 2>&1; then echo 'CVC5 already installed'; else " ++
-        "mkdir -p %{config.paths.install_dir}; " ++
-        "cd %{config.paths.install_dir}; " ++
-        "wget https://github.com/cvc5/cvc5/releases/download/cvc5-%{config.provers.cvc5.version}/cvc5-Linux; " ++
-        "chmod +x cvc5-Linux; " ++
-        "ln -sf %{config.paths.install_dir}/cvc5-Linux $HOME/.local/bin/cvc5; " ++
-      "fi",
-      "cvc5 --version",
-    ],
-  },
-
-  metamath = {
-    description = "Install Metamath (plain text verifier)",
-    enabled = config.provers.metamath.enabled && config.install_tiers.tier2,
-    commands = [
-      "echo 'Installing Metamath %{config.provers.metamath.version}...'",
-      "if command -v metamath >/dev/null 2>&1; then echo 'Metamath already installed'; else " ++
-        "mkdir -p %{config.paths.install_dir}; " ++
-        "cd %{config.paths.install_dir}; " ++
-        "git clone https://github.com/metamath/metamath-exe.git; " ++
-        "cd metamath-exe; " ++
-        "gcc *.c -o metamath; " ++
-        "ln -sf %{config.paths.install_dir}/metamath-exe/metamath $HOME/.local/bin/metamath; " ++
-      "fi",
-      "metamath --help | head -1",
-    ],
-  },
-}
-
-# Main installation recipes
-recipes = {
-  default = {
-    recipe = "install-all",
-    description = "Install all enabled theorem provers",
-  },
-
-  "check-prerequisites" = {
-    description = "Verify prerequisites for prover installation",
-    commands = [
-      "echo 'Checking prerequisites...'",
-
-      # Check basic tools
-      "command -v wget >/dev/null 2>&1 || { echo 'Error: wget not found'; exit 1; }",
-      "command -v git >/dev/null 2>&1 || { echo 'Error: git not found'; exit 1; }",
-
-      # Create installation directories
-      "mkdir -p %{config.paths.install_dir}",
-      "mkdir -p %{config.paths.config_dir}",
-      "mkdir -p $HOME/.local/bin",
-
-      # Check if .local/bin is in PATH
-      "if echo $PATH | grep -q '$HOME/.local/bin'; then echo '.local/bin already in PATH'; else echo 'Warning: Add $HOME/.local/bin to PATH'; fi",
-
-      "echo 'Prerequisites check complete!'",
+# K9 contract v1.0.0 (D173). This component provisions theorem provers
+# through the repository's two sanctioned paths only:
+#
+#   1. Guix (PRIMARY): manifests/live-provers.scm. That manifest records
+#      which provers Guix packages and which it does not; it is the
+#      authority, not this file.
+#   2. The sealed-container escape hatch for the not-in-Guix tail:
+#      .containerization/Containerfile.wave3, built by `just
+#      container-build-tier3`.
+#
+# It replaces an earlier version that was not valid Nickel (top-level
+# bindings without an enclosing record), named a fixed list of 12 provers
+# (docs/PROVER_COUNT.adoc is the only count), installed through sudo
+# apt/dnf, cabal and opam, piped an unpinned elan install script from
+# `master` into `sh`, and carried the string
+# "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT" where a signature belongs.
+#
+# WARNING: this component executes shell commands. It is 'Hunt, so a host
+# runs it only with all five Hunt preconditions met, a verified signature
+# among them. The signature block below is a claim until the owner signs this
+# file; until then the validator reports it 'Present_Unverified (K9-C001) and
+# Hunt stays unauthorised.
+#
+# Usage:
+#   k9-validate.sh --strict --layer L2 .machine_readable/setup-prover-env.k9.ncl
+#   k9-svc run .machine_readable/setup-prover-env.k9.ncl install-all
+
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "prover-env-setup",
+
+    metadata = {
+      name = "setup-prover-env",
+      version = "2.0.0",
+      description = "Provision ECHIDNA's live theorem provers through the Guix manifest and the Wave-3 sealed containers",
+      author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
+    },
+
+    security = {
+      leash = 'Hunt,
+      trust_level = "controlled-execution",
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = true,
+      # Default-deny: every flag above is paid for here (contract §8.4).
+      capabilities = [
+        "net.fetch",
+        "fs.write",
+        "process.spawn",
+        "container.run",
+      ],
+    },
+
+    warnings = [
+      "This is a Hunt-level component: it executes shell commands and changes the system.",
+      "Guix resolving a package does not show that the prover runs or that any proof passes.",
+      "A signature block being present is not a signature being verified.",
     ],
-  },
-
-  "install-tier1" = {
-    description = "Install Tier 1 provers (Agda, Coq, Lean, Isabelle, Z3, CVC5)",
-    dependencies = ["check-prerequisites"],
-    skip = !config.install_tiers.tier1,
-    commands =
-      prover_recipes.agda.commands @ prover_recipes.coq.commands @
-      prover_recipes.lean.commands @ prover_recipes.isabelle.commands @
-      prover_recipes.z3.commands @ prover_recipes.cvc5.commands,
-  },
-
-  "install-tier2" = {
-    description = "Install Tier 2 provers (Metamath, HOL Light, Mizar)",
-    dependencies = ["check-prerequisites"],
-    skip = !config.install_tiers.tier2,
-    commands = prover_recipes.metamath.commands,
-  },
 
-  "smoke-test-provers" = {
-    description = "Run smoke tests for installed provers",
-    skip = !config.run_smoke_tests,
-    commands = [
-      "echo 'Running smoke tests...'",
-      "if command -v agda >/dev/null 2>&1; then echo '✓ Agda'; else echo '✗ Agda'; fi",
-      "if command -v coqc >/dev/null 2>&1; then echo '✓ Coq'; else echo '✗ Coq'; fi",
-      "if command -v lean >/dev/null 2>&1; then echo '✓ Lean'; else echo '✗ Lean'; fi",
-      "if command -v isabelle >/dev/null 2>&1; then echo '✓ Isabelle'; else echo '✗ Isabelle'; fi",
-      "if command -v z3 >/dev/null 2>&1; then echo '✓ Z3'; else echo '✗ Z3'; fi",
-      "if command -v cvc5 >/dev/null 2>&1; then echo '✓ CVC5'; else echo '✗ CVC5'; fi",
-      "if command -v metamath >/dev/null 2>&1; then echo '✓ Metamath'; else echo '✗ Metamath'; fi",
-      "echo 'Smoke tests complete!'",
+    side_effects = [
+      "runs `guix package -m manifests/live-provers.scm`, which fetches substitutes or sources and writes the Guix store and the user's default profile",
+      "runs `just container-build-tier3`, which builds the Tier-3 prover images from .containerization/Containerfile.wave3 with podman and fetches their base images",
+      "runs `just doctor`, which only reads the toolchain",
     ],
-  },
 
-  "install-all" = {
-    description = "Install all enabled theorem provers (default)",
-    dependencies = [
-      "check-prerequisites",
-      "install-tier1",
-      "install-tier2",
-      "smoke-test-provers",
-    ],
-    commands = [
-      "echo ''",
-      "echo '╔══════════════════════════════════════════════════════════╗'",
-      "echo '║  ✅ ECHIDNA Prover Environment Setup Complete!         ║'",
-      "echo '╚══════════════════════════════════════════════════════════╝'",
-      "echo ''",
-      "echo 'Installed provers:'",
-      "command -v agda >/dev/null 2>&1 && echo '  - Agda (dependent type theory)'",
-      "command -v coqc >/dev/null 2>&1 && echo '  - Coq (interactive theorem prover)'",
-      "command -v lean >/dev/null 2>&1 && echo '  - Lean 4 (functional programming + proving)'",
-      "command -v isabelle >/dev/null 2>&1 && echo '  - Isabelle (higher-order logic)'",
-      "command -v z3 >/dev/null 2>&1 && echo '  - Z3 (SMT solver)'",
-      "command -v cvc5 >/dev/null 2>&1 && echo '  - CVC5 (SMT solver)'",
-      "command -v metamath >/dev/null 2>&1 && echo '  - Metamath (verifier)'",
-      "echo ''",
-      "echo 'Next steps:'",
-      "echo '  1. Build ECHIDNA:     just build'",
-      "echo '  2. Run tests:         just test'",
-      "echo '  3. Start ECHIDNA:     just run'",
-      "echo ''",
-    ],
+    # Ed25519, presence only (K9-S009). The signing step adds payload_hash
+    # and signature; verification is K9-C001 (L3).
+    signature = {
+      algorithm = "Ed25519",
+      key_id = "primary",
+    },
+  },
+
+  config = {
+    # Which sanctioned path(s) to run.
+    use_guix = true,
+    use_sealed_containers = false,   # heavier; builds every Tier-3 image
+    run_doctor = true,
+  },
+
+  # Recipes are an execution surface, which is why the leash is 'Hunt
+  # (K9-S011). Each delegates to a pinned, repository-owned surface; none
+  # downloads anything itself.
+  recipes = {
+    check-prerequisites = {
+      description = "Confirm the tools the sanctioned paths need are present",
+      # An enabled path whose tool is missing fails here, loudly; a disabled
+      # path is not checked. Nothing is skipped silently.
+      commands =
+        ["command -v just >/dev/null 2>&1 || { echo 'just not found'; exit 1; }"]
+        @ (if config.use_guix then ["command -v guix >/dev/null 2>&1 || { echo 'guix not found but config.use_guix is true'; exit 1; }"] else [])
+        @ (if config.use_sealed_containers then ["command -v podman >/dev/null 2>&1 || { echo 'podman not found but config.use_sealed_containers is true'; exit 1; }"] else []),
+    },
+    install-guix = {
+      description = "Install the Guix-packaged provers listed in manifests/live-provers.scm",
+      dependencies = ["check-prerequisites"],
+      commands = ["guix package -m manifests/live-provers.scm"],
+    },
+    install-containers = {
+      description = "Build the non-proprietary Tier-3 sealed prover containers",
+      dependencies = ["check-prerequisites"],
+      commands = ["just container-build-tier3"],
+    },
+    doctor = {
+      description = "Report which tools are present (read-only)",
+      commands = ["just doctor"],
+    },
+    # The dependency list is built from `config`, so a disabled path does not
+    # run and an enabled one does.
+    install-all = {
+      description = "Run every path enabled in config, then report",
+      dependencies =
+        ["check-prerequisites"]
+        @ (if config.use_guix then ["install-guix"] else [])
+        @ (if config.use_sealed_containers then ["install-containers"] else [])
+        @ (if config.run_doctor then ["doctor"] else []),
+      commands = ["echo 'install-all: every path enabled in config has run'"],
+    },
   },
 }
-
-validation = {
-  # At least one tier must be enabled
-  has_enabled_tier =
-    config.install_tiers.tier1
-    || config.install_tiers.tier2
-    || config.install_tiers.tier3
-    || config.install_tiers.tier4
-    | doc "At least one prover tier must be enabled",
-
-  # Ensure install methods are valid
-  valid_build_method =
-    config.install_methods.build_from_source == 'Never
-    || config.install_methods.build_from_source == 'IfNeeded
-    || config.install_methods.build_from_source == 'Always
-    | doc "build_from_source must be Never, IfNeeded, or Always",
-
-  # Container runtime must be valid
-  valid_container_runtime =
-    config.container_runtime == 'Podman
-    || config.container_runtime == 'Docker
-    | doc "container_runtime must be Podman or Docker",
-}
diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/k9/README.adoc
index 16107f14..ae11e68a 100644
--- a/.machine_readable/svc/k9/README.adoc
+++ b/.machine_readable/svc/k9/README.adoc
@@ -50,7 +50,7 @@ Configuration with Nickel contracts for runtime validation. Evaluated safely wit
 
 === Hunt Level (Full Execution)
 
-**File:** `examples/setup-repo.k9.ncl`
+**File:** `examples/setup-repo.k9.ncl.in` (a template: fill it, then validate it)
 
 Full execution with Just recipes. Can run shell commands and modify filesystem.
 
@@ -71,13 +71,13 @@ Choose the appropriate security level for your use case:
 [source,bash]
 ----
 # Kennel: Pure configuration
-cp contractiles/k9/examples/project-metadata.k9.ncl config/metadata.k9.ncl
+cp .machine_readable/svc/k9/examples/project-metadata.k9.ncl config/metadata.k9.ncl
 
 # Yard: Validated configuration
-cp contractiles/k9/examples/ci-config.k9.ncl .github/ci.k9.ncl
+cp .machine_readable/svc/k9/examples/ci-config.k9.ncl .github/ci.k9.ncl
 
 # Hunt: Full automation
-cp contractiles/k9/examples/setup-repo.k9.ncl scripts/setup.k9.ncl
+cp .machine_readable/svc/k9/examples/setup-repo.k9.ncl.in scripts/setup.k9.ncl  # then fill its placeholders
 ----
 
 === 2. Validate Components
@@ -136,9 +136,12 @@ K9 contractiles integrate with other RSR standards:
 
 Use these as starting points for your own K9 components:
 
-- `template-kennel.k9.ncl` - Pure data template
-- `template-yard.k9.ncl` - Validated config template
-- `template-hunt.k9.ncl` - Full execution template
+- `template-kennel.k9.ncl.in` - Pure data template
+- `template-yard.k9.ncl.in` - Validated config template
+- `template-hunt.k9.ncl.in` - Full execution template
+
+These end in `.in` because a template is not a component: they still carry
+unfilled placeholders. Copy one, fill it, drop the `.in`, and validate it.
 
 == Dependencies
 
diff --git a/.machine_readable/svc/k9/examples/ci-config.k9.ncl b/.machine_readable/svc/k9/examples/ci-config.k9.ncl
index 485a9173..9fe314e2 100644
--- a/.machine_readable/svc/k9/examples/ci-config.k9.ncl
+++ b/.machine_readable/svc/k9/examples/ci-config.k9.ncl
@@ -10,7 +10,7 @@ K9!
     component_type = "ci-configuration",
     security = {
       leash = 'Yard,
-      leash = "yard",
+      trust_level = "validated-config",
       allow_network = false,
       allow_filesystem_write = false,
       allow_subprocess = false,
diff --git a/.machine_readable/svc/k9/examples/project-metadata.k9.ncl b/.machine_readable/svc/k9/examples/project-metadata.k9.ncl
index f5bec22b..b2299b44 100644
--- a/.machine_readable/svc/k9/examples/project-metadata.k9.ncl
+++ b/.machine_readable/svc/k9/examples/project-metadata.k9.ncl
@@ -10,7 +10,7 @@ K9!
     component_type = "project-metadata",
     security = {
       leash = 'Kennel,
-      leash = "kennel",
+      trust_level = "data-only",
       allow_network = false,
       allow_filesystem_write = false,
       allow_subprocess = false,
diff --git a/.machine_readable/svc/k9/examples/setup-repo.k9.ncl b/.machine_readable/svc/k9/examples/setup-repo.k9.ncl.in
similarity index 100%
rename from .machine_readable/svc/k9/examples/setup-repo.k9.ncl
rename to .machine_readable/svc/k9/examples/setup-repo.k9.ncl.in
diff --git a/.machine_readable/svc/k9/template-hunt.k9.ncl b/.machine_readable/svc/k9/template-hunt.k9.ncl.in
similarity index 100%
rename from .machine_readable/svc/k9/template-hunt.k9.ncl
rename to .machine_readable/svc/k9/template-hunt.k9.ncl.in
diff --git a/.machine_readable/svc/k9/template-kennel.k9.ncl b/.machine_readable/svc/k9/template-kennel.k9.ncl.in
similarity index 100%
rename from .machine_readable/svc/k9/template-kennel.k9.ncl
rename to .machine_readable/svc/k9/template-kennel.k9.ncl.in
diff --git a/.machine_readable/svc/k9/template-yard.k9.ncl b/.machine_readable/svc/k9/template-yard.k9.ncl.in
similarity index 100%
rename from .machine_readable/svc/k9/template-yard.k9.ncl
rename to .machine_readable/svc/k9/template-yard.k9.ncl.in
diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl
index cce4d57a..8ea7cd93 100644
--- a/container/deploy.k9.ncl
+++ b/container/deploy.k9.ncl
@@ -1,98 +1,136 @@
 K9!
 # SPDX-License-Identifier: MPL-2.0
 # deploy.k9.ncl — ECHIDNA deployment component (Hunt level)
+#
+# k9-svc deployment component, K9 contract v1.0.0 (D173). The structure
+# follows rsr-template-repo build/container/stapeln/deploy.k9.ncl.in, with
+# ECHIDNA's own values filled in.
+#
+# WARNING: this component executes shell commands. It is 'Hunt, so a host
+# runs it only with all five Hunt preconditions met, a verified signature
+# among them. The signature block below is a claim until the owner signs this
+# file; until then the validator reports it 'Present_Unverified (K9-C001) and
+# Hunt stays unauthorised. (This replaces the earlier
+# "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT" string and "sha256:placeholder"
+# checksum, which looked like values but were not.)
+#
+# Usage:
+#   k9-validate.sh --strict --layer L2 container/deploy.k9.ncl
+#   k9-svc validate container/deploy.k9.ncl
+#   k9-svc deploy container/deploy.k9.ncl --env production
 
-let component_pedigree = {
-  # Top-level identity fields — duplicated from metadata so the K9
-  # validator (which inspects the literal `pedigree = { ... }` block
-  # at the toplevel of the file rather than the resolved Nickel value)
-  # can locate name / version / security_level without resolving the
-  # `component_pedigree` indirection.
-  name = "echidna-deploy",
-  version = "1.5.0",
-  schema_version = "1.0.0",
-  security_level = 'Hunt,
-  signature_required = true,
-  metadata = {
-    name = "echidna-deploy",
-    version = "1.5.0",
-    breed = "application/vnd.k9+nickel",
-    magic_number = "K9!",
-    description = "ECHIDNA deployment component (Hunt level)",
-  },
-  target = {
-    os = 'Linux,
-    is_edge = false,
-    requires_podman = true,
-    min_memory_mb = 512,
-  },
-  security = {
-    leash = 'Hunt,
-    allow_network = true,
-    allow_filesystem_write = true,
-    allow_subprocess = true,
-    signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT",
-  },
-  validation = {
-    checksum = "sha256:placeholder",
-    pedigree_version = "1.0.0",
-    hunt_authorized = false,
-  },
-  recipes = {
-    install = "just container-build",
-    validate = "just container-verify",
-    deploy = "just container-up",
-    migrate = "just container-build && just container-up",
-  },
-} in
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "deployment",
 
-let deployment = {
-  environments = {
-    dev = {
-      replicas = 1,
-      memory = "256Mi",
-      cpu = "100m",
-      image_tag = "dev",
+    metadata = {
+      name = "echidna-deploy",
+      version = "1.5.0",
+      description = "ECHIDNA deployment component (Hunt level)",
     },
-    staging = {
-      replicas = 2,
-      memory = "512Mi",
-      cpu = "250m",
-      image_tag = "staging",
+
+    # Target environment (extension field; contract §5.5).
+    target = {
+      os = 'Linux,
+      is_edge = false,
+      requires_podman = true,
+      min_memory_mb = 512,
     },
-    production = {
-      replicas = 3,
-      memory = "1Gi",
-      cpu = "500m",
-      image_tag = "latest",
+
+    security = {
+      leash = 'Hunt,
+      trust_level = "controlled-execution",
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = true,
+      # Default-deny: every flag above is paid for here (contract §8.4), plus
+      # the deploy and rollback actions the scripts below perform.
+      capabilities = [
+        "net.fetch",
+        "fs.write",
+        "process.spawn",
+        "container.run",
+        "deploy.apply",
+        "rollback.apply",
+      ],
+    },
+
+    warnings = [
+      "This is a Hunt-level component: it executes shell commands and changes the system.",
+      "Review the deployment scripts before running it.",
+      "A signature block being present is not a signature being verified.",
+      "Authorise Hunt explicitly: k9-svc authorize container/deploy.k9.ncl",
+    ],
+
+    side_effects = [
+      "spawns container/ct-build.sh, which builds the image",
+      "pulls and pushes ghcr.io/hyperpolymath/echidna images",
+      "starts, updates and stops the echidna stack with selur-compose, else podman compose over container/compose.toml",
+      "publishes the service on port 8081",
+    ],
+
+    # Ed25519, presence only (K9-S009). The signing step adds payload_hash
+    # and signature; verification is K9-C001 (L3).
+    signature = {
+      algorithm = "Ed25519",
+      key_id = "primary",
     },
   },
-  container = {
-    image = "ghcr.io/hyperpolymath/echidna",
-    port = 8081,
-    # Process-level readiness only: /api/health reports that this HTTP process
-    # responds. It does not check dispatcher, solver or dependent-service
-    # readiness. Consumers that gate traffic on those dependencies need their
-    # own checks; this probe cannot establish that stronger contract.
-    health_check = "/api/health",
-    readiness_check = "/api/health",
-  },
-  strategy = {
-    type = "rolling",
-    max_surge = 1,
-    max_unavailable = 0,
+
+  # Deployment configuration
+  deployment = {
+    environments = {
+      dev = {
+        replicas = 1,
+        memory = "256Mi",
+        cpu = "100m",
+        image_tag = "dev",
+      },
+      staging = {
+        replicas = 2,
+        memory = "512Mi",
+        cpu = "250m",
+        image_tag = "staging",
+      },
+      production = {
+        replicas = 3,
+        memory = "1Gi",
+        cpu = "500m",
+        image_tag = "latest",
+      },
+    },
+
+    container = {
+      image = "ghcr.io/hyperpolymath/echidna",
+      port = 8081,
+      # Process-level readiness only: /api/health reports that this HTTP process
+      # responds. It does not check dispatcher, solver or dependent-service
+      # readiness. Consumers that gate traffic on those dependencies need their
+      # own checks; this probe cannot establish that stronger contract.
+      health_check = "/api/health",
+      readiness_check = "/api/health",
+    },
+
+    strategy = {
+      type = "rolling",
+      max_surge = 1,
+      max_unavailable = 0,
+    },
   },
-} in
 
-let scripts = {
-  pre_deploy = m%"
+  # Deployment scripts (executed at Hunt level)
+  scripts = {
+    pre_deploy = m%"
 #!/bin/sh
 set -eu
 echo "K9: Pre-deployment validation for echidna..."
 cd container && selur-compose verify || podman compose --file compose.toml config
 echo "K9: Validation passed."
 "%,
-  deploy = m%"
+
+    deploy = m%"
 #!/bin/sh
 set -eu
 ENV="${1:-dev}"
@@ -102,7 +140,8 @@ cd container
 selur-compose up --detach || podman compose --file compose.toml up --detach
 echo "K9: Deployment to $ENV complete."
 "%,
-  rollback = m%"
+
+    rollback = m%"
 #!/bin/sh
 set -eu
 echo "K9: Rolling back echidna deployment..."
@@ -110,27 +149,26 @@ cd container
 selur-compose down || podman compose --file compose.toml down
 echo "K9: Rollback complete."
 "%,
-} in
+  },
 
-{
-  # The K9 validator does a literal text-scan over the toplevel
-  # `pedigree = { ... }` block and does not resolve Nickel let-bindings,
-  # so the identity fields (name / version / security_level) must appear
-  # inside the inline record here even though they are also present in
-  # the `component_pedigree` binding used by the runtime consumer.
-  pedigree = {
-    name = "echidna-deploy",
-    version = "1.5.0",
-    schema_version = "1.0.0",
-    security_level = 'Hunt,
-    signature_required = true,
-    metadata = component_pedigree.metadata,
-    target = component_pedigree.target,
-    security = component_pedigree.security,
-    validation = component_pedigree.validation,
-    recipes = component_pedigree.recipes,
+  # Just recipes: an execution surface, which is why the leash is 'Hunt
+  # (K9-S011).
+  recipes = {
+    install = {
+      description = "Build the container image",
+      commands = ["just container-build"],
+    },
+    validate = {
+      description = "Verify the compose configuration",
+      commands = ["just container-verify"],
+    },
+    deploy = {
+      description = "Start the container stack",
+      commands = ["just container-up"],
+    },
+    migrate = {
+      description = "Rebuild the image and restart the stack",
+      commands = ["just container-build", "just container-up"],
+    },
   },
-  deployment = deployment,
-  scripts = scripts,
-  required_level = 'Hunt,
 }
diff --git a/docs/ENV-VARS.adoc b/docs/ENV-VARS.adoc
index 53848308..968884ab 100644
--- a/docs/ENV-VARS.adoc
+++ b/docs/ENV-VARS.adoc
@@ -116,7 +116,7 @@ proxy
 |===
 |Variable |Note
 |`+VERISIMDB_URL+` |Old name for `+VERISIM_URL+`. Still read by
-`+tests/live_prover_suite.rs:118+` and enforced by `+k9iser.toml:47+`.
+`+tests/live_prover_suite.rs:118+`.
 Migration tracked in Stage 3c fix C3.
 |===
 
diff --git a/k9iser.toml b/k9iser.toml
deleted file mode 100644
index 29b113a0..00000000
--- a/k9iser.toml
+++ /dev/null
@@ -1,52 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-#
-# k9iser manifest for echidna
-# Generates K9 contracts from repo configuration files.
-# echidna is a neurosymbolic theorem proving platform (Rust + Julia; Bun for the static UI shell)
-
-[project]
-name = "echidna"
-safety_tier = "yard"
-
-[[source]]
-path = "Cargo.toml"
-type = "cargo"
-output = "generated/k9iser/cargo-manifest.k9"
-
-[[source]]
-path = "Justfile"
-type = "justfile"
-output = "generated/k9iser/justfile-recipes.k9"
-
-[[source]]
-path = "Containerfile"
-type = "containerfile"
-output = "generated/k9iser/container-build.k9"
-
-[[source]]
-path = ".github/workflows/hypatia-scan.yml"
-type = "workflow"
-output = "generated/k9iser/ci-security.k9"
-
-[[source]]
-path = ".github/workflows/codeql.yml"
-type = "workflow"
-output = "generated/k9iser/ci-codeql.k9"
-
-[[constraint]]
-rule = "build.dependencies has no banned_packages"
-severity = "error"
-
-[[constraint]]
-rule = "services.prover.environment contains 'VERISIMDB_URL'"
-severity = "warn"
-
-[[constraint]]
-rule = "container.base_image uses chainguard or distroless"
-severity = "warn"
-
-[[constraint]]
-rule = "workflows includes hypatia-scan"
-severity = "error"
-