diff --git a/.githooks/validate-k9.sh b/.githooks/validate-k9.sh
index fc27e8acd..f91a3be1a 100755
--- a/.githooks/validate-k9.sh
+++ b/.githooks/validate-k9.sh
@@ -1,42 +1,172 @@
 #!/usr/bin/env bash
 # SPDX-License-Identifier: MPL-2.0
-# K9 Contract Validation
-
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# validate-k9.sh — the LOCAL (hook) K9 gate. It owns no rules.
+#
+# ── WHAT THIS FILE USED TO BE ───────────────────────────────────────────
+# Until standards#1058 this hook implemented its own idea of a K9 file: it
+# grepped for a line beginning `contract` and warned if no SPDX identifier
+# appeared in the first five lines. Not one of the 30 tracked `*.k9` /
+# `*.k9.ncl` files in this repository contains a line beginning `contract`, so
+# the hook reported 30 errors on a clean tree and had no rule in common with
+# any specification. That is the "local assumption" the issue asked about: it
+# was not a weak implementation of the contract, it was an implementation of
+# something else that happened to share a filename.
+#
+# ── WHAT IT IS NOW ──────────────────────────────────────────────────────
+# A thin caller around the canonical validator,
+# 1-formats/k9/tools/k9-validate.sh, which implements
+# 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc against
+# 1-formats/k9/spec/contract/k9_contract.ncl. There is exactly one place where
+# K9 rules are written down, and this is not it.
+#
+# The only thing this hook adds is POLICY about which files block a commit:
+#
+#   * a file changed by this commit that does not conform  -> FAIL
+#   * a file in the shrink-only debt ledger that conforms  -> FAIL (stale)
+#   * an unlisted, unchanged file that does not conform    -> FAIL
+#   * a listed, UNCHANGED file that does not conform       -> advisory
+#
+# The ledger (.machine_readable/k9-contract-debt.txt) exists because the
+# contract landed after 25 files did, and turning 25 files red at once is how
+# this estate has twice ended up deleting a gate instead of fixing the files
+# (see the A2ML notes in .githooks/pre-commit). It can only shrink: fixing a
+# file forces its entry out, and an edit to a listed file removes its
+# protection for that commit.
+#
+# Runs at --layer L1 by default. L2 needs the `nickel` binary and belongs to
+# CI, where it is installed and pinned; a pre-commit hook that fails because a
+# laptop lacks a toolchain teaches people to pass --no-verify. Set
+# K9_VALIDATE_LAYER=all to check semantics locally too.
 set -euo pipefail
-SCAN_PATH="${INPUT_PATH:-.}"
+
+REPO_ROOT="${INPUT_PATH:-$(git rev-parse --show-toplevel 2>/dev/null || pwd)}"
+cd "$REPO_ROOT"
+
+VALIDATOR="1-formats/k9/tools/k9-validate.sh"
+LEDGER=".machine_readable/k9-contract-debt.txt"
+LAYER="${K9_VALIDATE_LAYER:-L1}"
 STAGED_FILES="${INPUT_STAGED_FILES:-}"
-ERRORS=0
-
-validate_file() {
-  local file="$1"
-  
-  # Basic structure check
-  if ! grep -qE '^contract' "$file"; then
-    echo "[validate-k9] ERROR: $file missing contract declaration" >&2
-    ERRORS=$((ERRORS + 1))
-  fi
-  
-  # SPDX header check
-  if ! head -5 "$file" | grep -qE '^# SPDX-License-Identifier:'; then
-    echo "[validate-k9] WARNING: $file missing SPDX header" >&2
-  fi
+
+RED='\033[0;31m'; GRN='\033[0;32m'; YEL='\033[1;33m'; BLU='\033[0;34m'; NC='\033[0m'
+[ -t 2 ] || { RED=''; GRN=''; YEL=''; BLU=''; NC=''; }
+
+if [ ! -x "$VALIDATOR" ] && [ ! -f "$VALIDATOR" ]; then
+  # Fail loudly rather than silently. A missing validator that reports success
+  # is indistinguishable from a conforming tree.
+  echo -e "${RED}[validate-k9] canonical validator missing: $VALIDATOR${NC}" >&2
+  exit 1
+fi
+
+# The conformance fixtures are the validator's own test corpus. Scanning them
+# repo-wide would report the negative controls as violations — and worse, a
+# "fix" that made them pass would be a fix that broke the suite.
+is_fixture() {
+  case "$1" in
+    1-formats/k9/tools/fixtures/*) return 0 ;;
+  esac
+  return 1
+}
+
+is_k9() {
+  case "$1" in
+    *.k9|*.k9.ncl) return 0 ;;
+  esac
+  return 1
+}
+
+ledger_entries() {
+  [ -f "$LEDGER" ] || return 0
+  grep -vE '^[[:space:]]*(#|$)' "$LEDGER"
+}
+
+in_ledger() {
+  ledger_entries | grep -qxF "$1"
 }
 
-# If staged files provided, only check those
+# Collect the file list.
+FILES=()
 if [ -n "$STAGED_FILES" ]; then
-  while IFS=$'\n' read -r file; do
-    [ -z "$file" ] && continue
-    # Only check .k9 files
-    [[ "$file" == *.k9 || "$file" == *.k9.ncl ]] || continue
-    [ -f "$file" ] || continue
-    validate_file "$file"
+  while IFS= read -r f; do
+    [ -z "$f" ] && continue
+    is_k9 "$f" || continue
+    is_fixture "$f" && continue
+    [ -f "$f" ] || continue
+    FILES+=("$f")
   done <<< "$STAGED_FILES"
 else
-  while IFS= read -r file; do
-    validate_file "$file"
-  done < <(find "$SCAN_PATH" -path '*/.git/*' -prune -o \( -name '*.k9' -o -name '*.k9.ncl' \) -type f -print 2>/dev/null)
+  while IFS= read -r f; do
+    is_fixture "$f" && continue
+    FILES+=("$f")
+  done < <(git ls-files -- '*.k9' '*.k9.ncl')
+fi
+
+if [ ${#FILES[@]} -eq 0 ]; then
+  echo -e "${BLU}[validate-k9]${NC} no K9 files to check"
+  exit 0
+fi
+
+# One validator invocation for the whole set: it is faster, and it keeps the
+# per-file verdicts coming from a single process rather than N slightly
+# different environments.
+REPORT="$(mktemp)"
+set +e
+bash "$VALIDATOR" --layer "$LAYER" --json --quiet "${FILES[@]}" > "$REPORT" 2>/dev/null
+set -e
+
+CHANGED="$STAGED_FILES"
+HARD=0
+ADVISORY=0
+CONFORMING=0
+STALE=0
+
+while IFS= read -r line; do
+  [ -z "$line" ] && continue
+  file="$(printf '%s' "$line" | sed -E 's/.*"file":"([^"]*)".*/\1/')"
+  verdict="$(printf '%s' "$line" | sed -E 's/.*"verdict":"([^"]*)".*/\1/')"
+  # `|| true` is load-bearing: a conforming file has no findings, grep exits 1,
+  # and under `set -o pipefail` that would abort the hook halfway through a
+  # clean tree — reporting neither a pass nor a failure.
+  rules="$(printf '%s' "$line" | grep -oE '"rule":"K9-[ESNC][0-9]+"' | sed 's/.*:"//; s/"//' | sort -u | tr '\n' ' ' | sed 's/ $//' || true)"
+
+  case "$verdict" in
+    pass|routed)
+      CONFORMING=$((CONFORMING + 1))
+      if in_ledger "$file"; then
+        # A conforming file must not keep its exemption: that is how a ledger
+        # becomes a permanent licence for debt that no longer exists.
+        echo -e "${RED}[validate-k9] STALE ledger entry: $file now conforms — remove it from $LEDGER in this change${NC}" >&2
+        STALE=$((STALE + 1))
+      fi
+      continue ;;
+  esac
+
+  touched=0
+  if [ -n "$CHANGED" ] && printf '%s\n' "$CHANGED" | grep -qxF "$file"; then
+    touched=1
+  fi
+
+  if [ $touched -eq 1 ] || ! in_ledger "$file"; then
+    echo -e "${RED}[validate-k9] FAIL${NC} $file ($verdict)${rules:+ — $rules}" >&2
+    HARD=$((HARD + 1))
+  else
+    echo -e "${YEL}[validate-k9] debt${NC} $file ($verdict)${rules:+ — $rules} (grandfathered; touching it makes it blocking)" >&2
+    ADVISORY=$((ADVISORY + 1))
+  fi
+done < "$REPORT"
+rm -f "$REPORT"
+
+if [ "$STALE" -gt 0 ] || [ "$HARD" -gt 0 ]; then
+  echo -e "${RED}[validate-k9] $HARD violation(s), $STALE stale ledger entr(ies)${NC}" >&2
+  echo -e "${RED}[validate-k9] spec: 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc · plan: 1-formats/k9/spec/MIGRATION-1058.adoc${NC}" >&2
+  exit 1
 fi
 
-[ $ERRORS -gt 0 ] && exit 1
-echo "[validate-k9] All K9 contracts valid"
+echo -e "${GRN}[validate-k9]${NC} $CONFORMING conforming, $ADVISORY grandfathered (layer $LAYER, contract v1.0.0)"
+if [ "$LAYER" = "L0" ] || [ "$LAYER" = "L1" ]; then
+  # Say out loud what was NOT checked. A lexical pass is not a conformance
+  # result, and the difference is the whole point of §12.
+  echo -e "${YEL}[validate-k9] lexical layers only — Nickel semantics (L2) and signature verification (L3) were not checked here${NC}" >&2
+fi
 exit 0
diff --git a/.githooks/validate-lint-format.sh b/.githooks/validate-lint-format.sh
index 9ab72d02c..7ecc4e545 100755
--- a/.githooks/validate-lint-format.sh
+++ b/.githooks/validate-lint-format.sh
@@ -100,7 +100,20 @@ else
 fi
 
 # ── Nickel ──────────────────────────────────────────────────────────────
-NCL="$(staged_matching '\.ncl$')"
+# `*.k9.ncl` is EXCLUDED here, matching .github/workflows/ci-pipeline.yml,
+# which excludes the same pathspec in both its `detect` and `nickel` jobs.
+#
+# A K9 component opens with the three-octet `K9!` sentinel, which is not
+# Nickel: `nickel typecheck` dies at 1:3 on the `!` (the CI comment says so
+# verbatim). Running it here anyway was not a strict gate, it was a wrong one
+# — it failed on a byte the format requires, on files no edit could fix, which
+# is the shape of a hook people learn to bypass with --no-verify.
+#
+# K9 files are not therefore unchecked. They are checked by the gate that
+# knows the format: .githooks/validate-k9.sh, which delegates to
+# 1-formats/k9/tools/k9-validate.sh and applies the envelope-strip rule
+# (K9-CONTRACT-SPEC §3.6) before it reaches for Nickel at all.
+NCL="$(staged_matching '\.ncl$' | grep -v '\.k9\.ncl$' || true)"
 if [ -n "$NCL" ]; then
   note "Nickel: $(echo "$NCL" | grep -c .) staged file(s)"
   if require_tool nickel Nickel "https://github.com/tweag/nickel/releases"; then
diff --git a/.githooks/validate-spdx.sh b/.githooks/validate-spdx.sh
index 03d2e7501..61edcf168 100755
--- a/.githooks/validate-spdx.sh
+++ b/.githooks/validate-spdx.sh
@@ -40,6 +40,29 @@ is_source_file() {
   esac
 }
 
+# A NEGATIVE CONTROL CANNOT ALSO SATISFY THE RULE IT TESTS.
+#
+# 1-formats/k9/tools/fixtures/invalid/ holds the K9 conformance corpus, and
+# every file in it exists to violate one named rule. L0-K9-E004-no-spdx.k9.ncl
+# is there precisely BECAUSE it has no SPDX header: it is the control that
+# proves rule K9-E004 can fire. Requiring a header on it would not tighten this
+# gate, it would delete the fixture and leave the K9 rule untested.
+#
+# The exemption is keyed to the RULE the fixture tests, not to the directory:
+# only a fixture whose name declares K9-E004 may lack a header. Every other
+# negative control still has to carry one, so this cannot become a blanket hole
+# in the corpus. It is also a separate predicate from is_source_file, so the two
+# reasons stay distinct: "is this a source file" is about syntax, "is this a
+# test vector for the licence rule" is about intent. Same reasoning as the
+# secret scanner's exclusion of published conformance vectors
+# (secret-scanner-reusable.yml).
+is_exempt_path() {
+  case "$1" in
+    1-formats/k9/tools/fixtures/invalid/*K9-E004*) return 0 ;;
+  esac
+  return 1
+}
+
 # If staged files provided, only check those
 if [ -n "$STAGED_FILES" ]; then
   FILES_TO_CHECK=$STAGED_FILES
@@ -68,6 +91,7 @@ while IFS= read -r file; do
   [ -n "$file" ] || continue
   [ -f "$file" ] || continue
   is_source_file "$file" || continue
+  is_exempt_path "$file" && continue
 
   CHECKED=$((CHECKED + 1))
 
diff --git a/.github/workflows/k9-contractile.yml b/.github/workflows/k9-contractile.yml
index c1bed4195..22f53ce8c 100644
--- a/.github/workflows/k9-contractile.yml
+++ b/.github/workflows/k9-contractile.yml
@@ -36,6 +36,12 @@ jobs:
     name: K9-SVC contractile validation
     timeout-minutes: 10
     runs-on: ubuntu-latest
+    # Needed only by the final step, which posts the validator's verdict to
+    # the pull request. Log blobs are not reachable from every machine that
+    # needs the result, so the result is published where it can be read.
+    permissions:
+      contents: read
+      pull-requests: write
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
@@ -89,4 +95,107 @@ jobs:
             echo "❌ $missing contractile(s) missing"
             exit 1
           fi
-          echo "✅ All ${#files[@]} contractiles present"
\ No newline at end of file
+          echo "✅ All ${#files[@]} contractiles present"
+      # ── K9 CONTRACT CONFORMANCE (standards#1058, ruling D173) ──────────
+      #
+      # Everything above this line checks that contractile FILES EXIST. None of
+      # it checked that a `.k9.ncl` file is a valid K9 component: the local hook
+      # grepped for a line beginning `contract`, which no file in this repo has,
+      # and ci-pipeline.yml excludes `*.k9.ncl` from Nickel entirely. So the
+      # required check named "K9-SVC contractile validation" validated the
+      # registry and never once read a pedigree.
+      #
+      # Nickel is installed here, pinned and sha256-verified with the SAME pin
+      # as ci-pipeline.yml's `nickel` job — one version estate-wide, so a file
+      # cannot typecheck in one lane and not in another.
+      - name: Install Nickel (pinned, sha256-verified)
+        env:
+          NICKEL_VERSION: '1.18.0'
+          NICKEL_SHA256: '9cba4dd65ae9915ec61f73033aafcff307a377665a83fd8f530df086763318cb'
+        run: |
+          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"
+          echo "K9_REPORT=$RUNNER_TEMP/k9-report.md" >> "$GITHUB_ENV"
+
+      # Each step mirrors its output into $GITHUB_STEP_SUMMARY as well as
+      # stdout. The PR then shows the verdict without anyone opening a raw log,
+      # and `gh api repos/{o}/{r}/check-runs/{job_id} --jq .output.summary`
+      # reads it back — which matters on a machine that cannot reach the log
+      # blob host. `set -uo pipefail` without `-e` so a failing validator still
+      # reaches the tee and its own status is what the step exits with.
+      - name: K9 contract self-test
+        run: |
+          set -uo pipefail
+          # Asserts the validator's bash mirrors still agree with the normative
+          # contract, the capability arithmetic, the structural extractor, and
+          # the envelope strip. Runs before the fixtures so a broken validator
+          # is reported as a broken validator rather than as a broken corpus.
+          {
+            echo '## K9 contract self-test'
+            echo '```'
+            bash 1-formats/k9/tools/k9-validate.sh --self-test 2>&1
+            echo '```'
+          } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT"
+          exit "${PIPESTATUS[0]}"
+
+      - name: K9 conformance fixtures (positive AND negative controls)
+        run: |
+          set -uo pipefail
+          # --strict: with Nickel on PATH every format layer (L0-L2) must
+          # actually run, so a missing toolchain cannot report a pass. The 21
+          # negative controls are the load-bearing half — a validator that
+          # accepts everything satisfies the positive half trivially.
+          {
+            echo '## K9 conformance fixtures'
+            echo '```'
+            bash 1-formats/k9/tools/k9-validate.sh --strict \
+              --fixtures 1-formats/k9/tools/fixtures 2>&1
+            echo '```'
+          } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT"
+          exit "${PIPESTATUS[0]}"
+
+      - name: K9 corpus conformance (ratcheted)
+        run: |
+          set -uo pipefail
+          # The whole tracked corpus, through the same gate the pre-commit hook
+          # uses, so CI and the hook cannot disagree about what a K9 file is.
+          # .machine_readable/k9-contract-debt.txt grandfathers the 25 files
+          # that predate the contract; it is shrink-only (a conforming file
+          # left in it fails), and it does not protect a file this PR touches.
+          {
+            echo '## K9 corpus conformance'
+            echo '```'
+            bash .githooks/validate-k9.sh 2>&1
+            echo '```'
+          } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT"
+          exit "${PIPESTATUS[0]}"
+
+      - name: Publish the K9 verdict to the pull request
+        # always(): a failing gate is exactly when the detail is needed, and a
+        # skipped step would publish nothing.
+        if: ${{ always() && github.event_name == 'pull_request' }}
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+        run: |
+          set -uo pipefail
+          [ -s "$K9_REPORT" ] || { echo "no K9 report produced"; exit 0; }
+          {
+            echo '<!-- k9-contractile-report: regenerated on every run -->'
+            echo '# K9 contract conformance'
+            echo
+            echo "_run_ $GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
+            cat "$K9_REPORT"
+          } > "$RUNNER_TEMP/body.md"
+          prev=$(gh pr view "$PR_NUMBER" --repo "$GITHUB_REPOSITORY" --json comments \
+            --jq '.comments[] | select(.body | startswith("<!-- k9-contractile-report")) | .url' | tail -1 || true)
+          if [ -n "$prev" ]; then
+            # Edit the previous report in place so repeated runs do not stack up.
+            gh api -X PATCH "${prev#https://github.com/}" -F body=@"$RUNNER_TEMP/body.md" >/dev/null
+          else
+            gh pr comment "$PR_NUMBER" --repo "$GITHUB_REPOSITORY" --body-file "$RUNNER_TEMP/body.md" >/dev/null
+          fi
diff --git a/.machine_readable/k9-contract-debt.txt b/.machine_readable/k9-contract-debt.txt
new file mode 100644
index 000000000..f220e7cef
--- /dev/null
+++ b/.machine_readable/k9-contract-debt.txt
@@ -0,0 +1,46 @@
+# .machine_readable/k9-contract-debt.txt — SHRINK-ONLY ledger of grandfathered
+# K9 files.
+#
+# 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc v1.0.0 (standards#1058, ruling D173)
+# landed AFTER these 25 files did, so the local gate cannot turn them all red at
+# once: that is the exact failure the estate has already paid for twice, when a
+# validator that passed 0 of 222 files blocked every commit and was deleted
+# instead of the files being fixed (.githooks/pre-commit, A2ML note).
+#
+# The ratchet is one-directional, and .githooks/validate-k9.sh enforces all
+# three directions:
+#   * a path here that now CONFORMS is a STALE entry and FAILS the hook —
+#     fixing a file must shrink this ledger in the same change;
+#   * a path NOT here that does not conform FAILS, so new debt cannot appear;
+#   * a path here that is TOUCHED BY THE COMMIT FAILS, so this ledger can never
+#     be used to carry a violation through an edit to the file that has it.
+#
+# One repo-relative path per line. '#' comments and blanks ignored.
+# Baseline 2026-10-03, produced by:
+#   1-formats/k9/tools/k9-validate.sh --layer L1 --json <every tracked *.k9*>
+# Count: 25
+.machine_readable/contractiles/adjust/adjust.k9.ncl
+.machine_readable/contractiles/bust/bust.k9.ncl
+.machine_readable/contractiles/dust/dust.k9.ncl
+.machine_readable/contractiles/intend/intend.k9.ncl
+.machine_readable/contractiles/must/must.k9.ncl
+.machine_readable/contractiles/trust/trust.k9.ncl
+.machine_readable/svc/k9/examples/setup-repo.k9.ncl
+.machine_readable/svc/k9/template-hunt.k9.ncl
+.machine_readable/svc/k9/template-kennel.k9.ncl
+.machine_readable/svc/k9/template-yard.k9.ncl
+2-protocols/axel/config/ci.k9.ncl
+2-protocols/axel/config/metadata.k9.ncl
+3-practice/session-management-standards/continuity/checkpoint-before-major-change/PROTOCOL.k9
+3-practice/session-management-standards/continuity/emergency-termination/PROTOCOL.k9
+3-practice/session-management-standards/continuity/planned-session-close/PROTOCOL.k9
+3-practice/session-management-standards/continuity/recovery-operation/PROTOCOL.k9
+3-practice/session-management-standards/continuity/repo-intake/PROTOCOL.k9
+3-practice/session-management-standards/handover/collaborative-transfer/PROTOCOL.k9
+3-practice/session-management-standards/handover/full-transfer/PROTOCOL.k9
+3-practice/session-management-standards/handover/human-transfer/PROTOCOL.k9
+3-practice/session-management-standards/handover/model-transfer/PROTOCOL.k9
+3-practice/session-management-standards/verify/maintenance-sweep/PROTOCOL.k9
+3-practice/session-management-standards/verify/release-audit/PROTOCOL.k9
+3-practice/session-management-standards/verify/substantial-completion/PROTOCOL.k9
+rhodium-standard-repositories/rsr-compliance-checklist.k9.ncl
diff --git a/1-formats/k9/.gitattributes b/1-formats/k9/.gitattributes
index e860a85c1..4606f2470 100644
--- a/1-formats/k9/.gitattributes
+++ b/1-formats/k9/.gitattributes
@@ -52,3 +52,10 @@ Containerfile  text eol=lf
 # Lock files
 Cargo.lock  text eol=lf -diff
 flake.lock  text eol=lf -diff
+
+# K9 conformance fixtures are byte-preserved evidence. The CRLF fixture exists
+# to be REJECTED for its line endings (rule K9-E003), so normalising it on
+# commit would silently delete the negative control while leaving the file —
+# and a suite whose negative control no longer fails is a suite that reports
+# green over nothing. Path is relative to this .gitattributes.
+tools/fixtures/invalid/L0-K9-E003-crlf.k9.ncl -text -eol
diff --git a/1-formats/k9/SPEC.adoc b/1-formats/k9/SPEC.adoc
index 5b3fe998a..1cd39cefb 100644
--- a/1-formats/k9/SPEC.adoc
+++ b/1-formats/k9/SPEC.adoc
@@ -35,8 +35,33 @@ word `must` appears in both and means different things; never conflate them.
 |Version |1.0.0
 |Stability |Stable
 |Magic Number |`K9!` (`\x4B\x39\x21`)
+|Normative contract |link:spec/K9-CONTRACT-SPEC.adoc[K9 Component Contract
+Specification v1.0.0] — *this document is the format overview; conformance is
+specified there*
+|Contract file |link:spec/contract/k9_contract.ncl[`spec/contract/k9_contract.ncl`]
+|Canonical validator |link:tools/k9-validate.sh[`tools/k9-validate.sh`]
+|Conformance suite |link:tools/fixtures/[`tools/fixtures/`] (5 positive, 21 negative)
 |===
 
+[IMPORTANT]
+.Where the normative text lives
+====
+This document describes the format: the problem, the layer model, the triad,
+the MIME path. It is *not* the conformance specification, and the Nickel
+snippets below are illustrative sketches rather than the contract.
+
+Conformance is specified by
+link:spec/K9-CONTRACT-SPEC.adoc[*K9 Component Contract Specification v1.0.0*],
+whose machine-readable form is
+link:spec/contract/k9_contract.ncl[`spec/contract/k9_contract.ncl`]. Where a
+sketch here and the contract disagree, the contract wins.
+
+Ruling *D173* (standards#1058, 2026-09-30) settled the artefact question: *"K9
+needs a Nickel contract, not an ABNF."* There is deliberately no `k9.abnf` —
+K9 has no syntax of its own, since a component body *is* a Nickel term. The
+reasoning is recorded in Appendix B of the contract specification.
+====
+
 == Problem Statement
 
 Traditional file formats are **passive containers**. They rely entirely on external
@@ -134,6 +159,17 @@ K9Pedigree = {
 
 All data must pass these contracts before deployment.
 
+[NOTE]
+====
+The sketch above is the *repository* pedigree and it is illustrative. The
+normative contract for a *component* file (`*.k9.ncl`) is
+link:spec/contract/k9_contract.ncl[`spec/contract/k9_contract.ncl`], and the
+two shapes are not interchangeable — see
+link:spec/K9-CONTRACT-SPEC.adoc#_pedigree_ncl_a_different_contract[§16.2 of the
+contract specification]. Applying one to the other is a defect, not a
+convenience.
+====
+
 === L3: The Muscle (Just Orchestration)
 
 Just recipes handle environment-specific deployment:
@@ -155,7 +191,18 @@ Podman-first deployment prevents host pollution while supporting native fallback
 === The Leash System (Normative)
 
 To prevent abuse, `.k9` mandates tiered execution levels. These are NORMATIVE:
-an implementation MUST enforce them. The canonical encoding is `leash.ncl`.
+an implementation MUST enforce them.
+
+The normative statement is
+link:spec/K9-CONTRACT-SPEC.adoc[contract spec §7]; the closed set is encoded in
+link:spec/contract/k9_contract.ncl[`k9_contract.ncl`] as both the
+`SecurityLevel` enum and the `leash_levels` list a validator can read without a
+Nickel toolchain, and `tools/k9-validate.sh --self-test` asserts the two agree.
+`leash.ncl` carries the host-side machinery (`detect_level`, `check_level`, the
+handshake formats).
+
+An unknown leash tag is a contract violation, not a warning and not a
+downgrade. Adding a fourth level is a MAJOR change.
 
 [cols="1,2,3",options="header"]
 |===
@@ -186,18 +233,44 @@ NOT sufficient (this is the normative change from the alpha).
 |===
 |Precondition |Meaning
 
-|`signature` |A valid Ed25519 signature over the payload hash.
+|`signature` |A *verified* Ed25519 signature over the payload hash — see the
+distinction below.
 |`policy` |An explicit policy decision of `allow`.
 |`sandbox` |An isolation sandbox is in force for the run.
 |`dry_run` |A dry-run plan was produced (and reviewed).
 |`capability_grant` |Every requested capability is explicitly granted (default-deny; see Capability Model).
 |===
 
-The gate is `authorize_hunt(evidence)` in `leash.ncl`: it permits `'Hunt` iff
+The gate is `authorize_hunt(evidence)` in `leash.ncl`, and identically in
+link:spec/contract/k9_contract.ncl[`k9_contract.ncl`]: it permits `'Hunt` iff
 all five evidence flags are true, and otherwise returns `permitted = false`,
 `enforced_level = 'Yard`, and the exact list of unmet preconditions (which the
 receipt records).
 
+[WARNING]
+.Presence is not verification
+====
+The `signature` precondition is satisfied by a signature that *verified*, and
+by nothing else. A `signature` block in a pedigree is a **claim**: reading it
+proves the file says it was signed, not that it was, and not that the signature
+covers the bytes about to be executed.
+
+link:spec/K9-CONTRACT-SPEC.adoc[Contract spec §10] fixes the mapping a
+conforming implementation may make — `'Absent`, `'Present_Unverified`,
+`'Verified`, `'Rejected` — and notes what is absent from it: *there is no input
+that turns "no verifier ran" into "verified".* A lexical check that counted a
+signature field and called it a Hunt authorisation would re-create exactly the
+alpha behaviour this directive removed.
+
+`tools/k9-validate.sh` therefore embeds no verifier. It reports
+`'Present_Unverified` as a SKIPPED check and says, in its output, that this
+does not authorise `'Hunt`.
+====
+
+Conformance is also not authorisation. A component that satisfies every rule in
+the contract is a well-formed *request* to run; §9 of the contract spec is what
+decides whether it runs.
+
 === Dependability Collapse Prevention
 
 **Dependability Collapse** occurs when security mitigations become so heavy
@@ -237,9 +310,32 @@ until explicitly permitted.
 == Capability Model (Normative)
 
 K9 is *default-deny*: a component is granted *no* capability unless it is
-explicitly listed in its pedigree `policy.capabilities`. The leash checks the
-grant before any Hunt-level action; an action needing an ungranted capability
-is refused even at `'Hunt`. The canonical encoding is `capabilities.ncl`.
+explicitly listed in its pedigree. The leash checks the grant before any
+Hunt-level action; an action needing an ungranted capability is refused even at
+`'Hunt`.
+
+The closed set is encoded in
+link:spec/contract/k9_contract.ncl[`k9_contract.ncl`] (`core_capabilities`) and
+mirrored in `capabilities.ncl`; the normative statement is
+link:spec/K9-CONTRACT-SPEC.adoc[contract spec §8].
+
+[IMPORTANT]
+.A flag is a request that must be paid for
+====
+New in contract v1.0.0 (§8.4): a security flag *requests* a capability, and the
+grant MUST cover it.
+
+[cols="1,1"]
+|===
+|`allow_network = true` |requires `net.fetch`
+|`allow_filesystem_write = true` |requires `fs.write`
+|`allow_subprocess = true` |requires `process.spawn`
+|===
+
+A component with `allow_network = true` and an empty grant is *invalid*, not
+merely unwise. Before this rule the flags and the grant were two unrelated
+opinions in the same block, so "default-deny" denied nothing.
+====
 
 === Closed core capabilities
 
@@ -268,6 +364,16 @@ names (no `x-` prefix) are reserved to this specification.
 
 == The Active Pedigree (Seven Sections)
 
+[NOTE]
+====
+This is the *repository* pedigree — the seven-section form a K9 repository root
+carries in `pedigree.ncl`. It is a different contract from the `pedigree` block
+inside a `*.k9.ncl` *component* file, the two shapes are not compatible, and
+they share only a name. The component pedigree is specified by
+link:spec/K9-CONTRACT-SPEC.adoc[contract spec §6]. A reader MUST NOT apply one
+to the other.
+====
+
 v1.0.0 restructures the pedigree (`pedigree.ncl`) into seven explicit, named
 sections. Two are new in v1.0.0: *recovery_recipe* and *docs_rationale*.
 
@@ -353,6 +459,16 @@ To be listed as a conforming `.k9` repository:
 |This specification document (optional but recommended)
 |===
 
+[NOTE]
+====
+These are requirements for a *repository*. They say nothing about whether an
+individual `*.k9.ncl` file is a valid component — that is
+link:spec/K9-CONTRACT-SPEC.adoc[the contract specification's] job, and a
+repository can satisfy every row above while shipping components that fail it.
+The two are checked by different things: this table by review, component
+conformance by link:tools/k9-validate.sh[`tools/k9-validate.sh`].
+====
+
 == Path to MIME Recognition
 
 === Linux (Freedesktop)
diff --git a/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc b/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc
new file mode 100644
index 000000000..23d9d9e65
--- /dev/null
+++ b/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc
@@ -0,0 +1,1095 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= K9 Component Contract Specification
+:subtitle: The normative Nickel contract for `application/vnd.k9`
+:author: hyperpolymath
+:revnumber: 1.0.0
+:revdate: 2026-10-03
+:toc: left
+:toclevels: 3
+:icons: font
+:source-highlighter: rouge
+:sectnums:
+:standard-id: application/vnd.k9
+:contract-file: contract/k9_contract.ncl
+
+:sectnums!:
+
+== Abstract
+
+This document is the **normative conformance specification** for a K9
+component. It defines the file envelope, the dialect rules, the versioned
+pedigree contract, the closed leash taxonomy, the default-deny capability
+model, the five Hunt preconditions, and the semantics of a signature block.
+
+It is deliberately *not* a grammar. Ruling *D173* (standards#1058,
+2026-09-30) settled the question this way:
+
+[quote, RULING D173, standards#1058]
+____
+Delete the stale 'pending owner ruling' line (deed.abnf is sole normative
+since #856); *K9 needs a Nickel contract, not an ABNF.*
+____
+
+The machine-readable form of everything specified here is
+link:{contract-file}[`spec/contract/k9_contract.ncl`]. Where this prose and
+that file disagree, *this prose wins and the file is a bug*.
+
+== Status
+
+[cols="1,3"]
+|===
+|Standard ID |`application/vnd.k9`
+|Document |K9 Component Contract Specification
+|Version |1.0.0
+|Stability |Normative
+|Schema major |`1`
+|Contract file |link:{contract-file}[`spec/contract/k9_contract.ncl`]
+|Canonical validator |link:../tools/k9-validate.sh[`tools/k9-validate.sh`]
+|Conformance suite |link:../tools/fixtures/[`tools/fixtures/`] (5 positive, 21 negative)
+|Ruling |D173 (standards#1058, 2026-09-30)
+|Supersedes |the prose-only contract description in link:../SPEC.adoc[`SPEC.adoc`] §L2 and §The Active Pedigree
+|===
+
+[IMPORTANT]
+.Naming hazard — unchanged, and now load-bearing
+====
+K9's execution triad is *must / just / nickel*. It is *not* the contractiles
+family *must / trust / dust / intend*. The word `must` appears in both and
+means different things; never conflate them.
+
+This specification resolves the collision by *not naming contractile verbs at
+all*. A contractile component is an ordinary K9 component whose
+`component_type` begins `contractile:` (§6.2). Nothing in the contract
+namespace belongs to the contractiles family, so translating that family to
+DEED cannot rename anything this document depends on.
+====
+
+:sectnums:
+
+== Scope
+
+=== In scope
+
+This specification governs a *K9 component*: a file carrying the `K9!`
+envelope whose body is a Nickel term declaring a `pedigree`. It specifies:
+
+* the byte-level envelope (§3);
+* which dialects may claim a K9 file extension, and how a reader tells them
+  apart (§4);
+* how the contract is versioned and what a reader does with a component from
+  another major (§5);
+* the shape of the component pedigree (§6);
+* the leash taxonomy as a closed, machine-checkable set (§7);
+* the capability model, default-deny, with the capabilities a security flag
+  *costs* (§8);
+* the five Hunt preconditions (§9);
+* what a signature block does and does not prove (§10);
+* libraries and `import` behaviour (§11);
+* the four conformance layers, and which of them may claim to have decided
+  anything (§12).
+
+=== Out of scope
+
+[horizontal]
+Nickel's own grammar:: Specified upstream and normative *by reference*
+(§3.5). K9 has no syntax of its own; a K9 component body *is* a Nickel term.
+Re-specifying Nickel in ABNF would fork a language this estate does not own,
+and would produce a grammar that drifts from the implementation on the first
+upstream release.
+The `k9-coordination` dialect:: Named in §4 so a reader can route it, but
+governed by
+link:../../../2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.1.abnf[`coordination-k9-grammar_v1.1.abnf`].
+That format is YAML-bodied and has its own ABNF, which is correct for it: it
+*does* have a syntax of its own.
+The repository pedigree:: link:../pedigree.ncl[`pedigree.ncl`] defines a
+seven-section pedigree for a *K9 repository* (metadata, validation_contract,
+policy, deploy_recipe, recovery_recipe, signature, docs_rationale). That is a
+different contract with a different subject and it is *not* applied to
+component files. See §16.2.
+Cryptographic verification:: §10 specifies the *semantics* of verification —
+what a host may infer, and what it may not. It does not specify a key
+distribution or trust mechanism, because key trust is host policy rather than
+file format.
+Receipts and evidence:: Specified by the `a2ml/k9-receipt` profile referenced
+from link:../SPEC.adoc[`SPEC.adoc`].
+
+== Conformance language
+
+The key words *MUST*, *MUST NOT*, *REQUIRED*, *SHALL*, *SHOULD*, *SHOULD NOT*,
+*MAY* and *OPTIONAL* are to be interpreted as described in RFC 2119.
+
+Every requirement in this document carries a stable *rule id* so that a
+fixture can name the rule it violates, a validator can name the rule it
+enforced, and a migration can name the rule it cleared. Rule ids are
+never renumbered; a withdrawn rule keeps its id and is marked withdrawn.
+
+[cols="1,2,3",options="header"]
+|===
+|Prefix |Layer |Meaning
+|`K9-E*` |L0 |Envelope: bytes, encoding, licence, dialect.
+|`K9-S*` |L1 |Structural: the pedigree fields the contract requires.
+|`K9-N*` |L2 |Semantic: Nickel evaluation against the contract.
+|`K9-C*` |L3 |Cryptographic: signature verification.
+|===
+
+A full index is at <<rule-index,Appendix A>>.
+
+=== Conformance classes
+
+[horizontal]
+Component:: A file that satisfies §3–§11 for the `k9-svc-component` dialect.
+Library:: A file that satisfies §3 and §11 for the `k9-svc-library` dialect.
+Reader:: An implementation that classifies a file per §4 and reports a
+verdict per §12. A reader MUST report the layers it did not run (§12.4).
+Host:: An implementation that executes components. A host MUST apply §7, §8
+and §9 before any side effect, and MUST NOT treat conformance as
+authorisation (§9.4).
+
+== File envelope
+
+=== K9-E001 — the magic line
+
+A component file's first line MUST be exactly the three octets
+`0x4B 0x39 0x21` (ASCII `K9!`) followed immediately by the line terminator. A
+reader MUST NOT tolerate case variants, trailing whitespace, or a byte-order
+mark: a magic number with a tolerance is not a magic number, and a kernel that
+sniffs bytes would disagree with a validator that forgives them.
+
+A file with no magic line is a *library* (§11) or nothing at all (§4.2). It is
+never a component.
+
+=== K9-E004 — the licence identifier
+
+The first five lines MUST include a line of the form
+`# SPDX-License-Identifier: <id>`. This is envelope metadata rather than
+content: an unlicensed component cannot be redistributed, so the absence is a
+defect and not a style note.
+
+=== K9-E002 / K9-E003 — encoding and line endings
+
+A K9 file MUST be UTF-8 text with no NUL octet (K9-E002) and MUST use LF line
+endings (K9-E003). A CR inside the magic line makes it four octets, which is
+precisely the disagreement K9-E001 forbids a reader to paper over.
+
+=== K9-E005 — reading the body
+
+After the magic line and the comment header, the first significant line
+decides the dialect (§4.3). A reader MUST classify before it validates:
+applying the component contract to a coordination file produces a list of
+missing pedigree fields that are all true and all irrelevant.
+
+=== Nickel is normative by reference
+
+The body of a component is a Nickel term. Nickel's grammar, evaluation order
+and standard library are normative *by reference* to the Nickel
+implementation, at the version the reader declares. This specification adds
+no production to that grammar and removes none.
+
+This is the reason there is no `k9.abnf` in this repository, and it is the
+substance of ruling D173. See <<no-abnf,Appendix B>>.
+
+=== The envelope-strip rule (K9-N001, precondition)
+
+`K9!` on line 1 is *not* Nickel. This estate's own CI records the consequence
+verbatim:
+
+[quote, .github/workflows/ci-pipeline.yml, `detect` step]
+____
+`*.k9.ncl` files open with a `K9!` sentinel on line 1 and are k9 contracts,
+not Nickel source — `nickel typecheck` dies at 1:3 on the `!`.
+____
+
+That is why every `*.k9.ncl` file in this repository is currently excluded
+from Nickel checking, in both the `detect` and `nickel` jobs: a format whose
+required first byte makes the language's own parser fail cannot be
+typechecked, and so none of them ever were.
+
+A reader that evaluates a component's body in Nickel MUST therefore first
+*strip the envelope*: remove the magic line, substituting a Nickel comment so
+that line numbers — and therefore every diagnostic a user sees — do not move.
+Nothing about the component's meaning changes. The magic is envelope, and the
+envelope is not part of the term.
+
+The canonical validator implements this in `strip_envelope()`, and its
+self-test asserts that the line count and the position of every subsequent
+line are preserved.
+
+== Dialects
+
+=== The four dialects
+
+[cols="1,2,2,2",options="header"]
+|===
+|Dialect |Envelope |Body |Governed by
+|`k9-svc-component` |`K9!` + SPDX |Nickel term with a top-level `pedigree` |*this document*
+|`k9-svc-library` |none |Nickel term, no `pedigree`, no `leash` |§11 of this document
+|`k9-coordination` |`K9!` + SPDX |YAML |`coordination-k9-grammar_v1.1.abnf`
+|*unclaimed* |any |anything else |nothing — and that is the defect
+|===
+
+The first two are K9 SVC. The third shares the magic bytes and the licence
+header but not the body language; it is a different format that happens to
+have been given the same scent. Naming it here is what lets a reader route it
+instead of misreporting it as a broken component.
+
+=== Extension reservation
+
+The `.k9` and `.k9.ncl` extensions are *reserved* to the dialects above. A
+file that carries one of them and belongs to none of them is *unclaimed*
+(K9-E005) and MUST be reported, not skipped.
+
+This is not pedantry. Twelve files under
+`3-practice/session-management-standards/` are named `PROTOCOL.k9` and contain
+YAML stubs for a session-management protocol that is neither K9 SVC nor
+k9-coordination. A reviewer, `file(1)`, an editor mode and every future
+validator all read the suffix as a format promise. Reserving the suffix is
+what makes that promise mean something; renaming those files is migration item
+M4.
+
+=== K9-E005 — the discriminator
+
+A reader MUST classify a file as follows, on the first significant line after
+the envelope:
+
+[cols="1,2,2",options="header"]
+|===
+|First significant line |With `K9!` magic |Without
+|`---` |`k9-coordination` |`k9-coordination`
+|`{`, `[`, `(`, `let `, or a string literal |`k9-svc-component` |`k9-svc-library`
+|an `identifier =` binding |`k9-svc-component` |`k9-svc-library`
+|a bare `key:` line (no `=`) |`k9-coordination` |*unclaimed*
+|anything else |*unclaimed* |*unclaimed*
+|===
+
+A Nickel file must ultimately be a *single* term, so a top-level binding
+sequence is a defect — but it is a Nickel defect, and belongs at L1/L2 rather
+than to a dialect mismatch.
+
+=== Routed is not passed
+
+A file classified `k9-coordination` is *routed*: the reader examined it and
+handed it to the specification that governs it. A routed file is neither a
+pass nor a failure of this contract, and a reader MUST report which of the
+three it recorded. Silently dropping out-of-scope files is how a validator
+comes to report green over a set it never looked at.
+
+== Versioning
+
+=== The two version numbers
+
+[cols="1,3"]
+|===
+|`contract_version` |The version of `k9_contract.ncl` itself.
+|`schema_major` |The major segment a component's `pedigree.schema_version`
+must carry to be readable by that contract.
+|===
+
+They are separate numbers on purpose. The contract can be revised
+(`1.0.0` → `1.0.1`) without changing what a component must look like. A reader
+MUST NOT infer one from the other.
+
+=== K9-S002 — `pedigree.schema_version`
+
+Every component MUST declare `pedigree.schema_version` as a numeric
+dot-triple `MAJOR.MINOR.PATCH`:
+
+* three non-empty segments, digits only;
+* no leading zero in any segment (`1.00.0` is invalid);
+* no leading or trailing dot;
+* `MAJOR` equal to the reader's `schema_major`.
+
+The contract encodes this as `is_semver_of`, which walks the string once using
+only `std.string.length` and `std.string.substring`.
+
+=== Compatibility
+
+Within a major, this contract follows semantic versioning:
+
+[cols="1,3",options="header"]
+|===
+|MAJOR |Breaking. A reader MUST refuse a component from another major (§5.4).
+|MINOR |Backwards-compatible additions: new OPTIONAL fields, new extension
+namespaces. A reader MUST accept a component written against a lower minor.
+|PATCH |Clarifications and validator fixes. No change to what a component must
+look like.
+|===
+
+=== K9-S002 — a component from another major is refused
+
+A reader MUST NOT guess at a `schema_version` whose major it does not
+implement. A v1 reader interpreting a v2 field layout produces a *confident
+wrong answer about a security posture*, which is worse than an error. Refuse,
+name the major you speak, and stop.
+
+=== Open and closed fields
+
+[cols="2,3",options="header"]
+|===
+|Field |Policy
+|`pedigree.schema_version`, `component_type`, `security`, `metadata` |REQUIRED
+|`security.leash` |REQUIRED, closed enum (§7)
+|`security.capabilities` |OPTIONAL, closed name space (§8)
+|`pedigree.warnings`, `pedigree.side_effects` |OPTIONAL, but see §6.5
+|`pedigree.signature` |OPTIONAL, but see §10.1
+|`config`, `recipes`, `validation` |OPEN — the component's own business
+|Unknown fields anywhere |PERMITTED. A reader SHOULD report them and MUST NOT
+consult them to relax any requirement of §8 or §9.
+|===
+
+The last row is the important one. A `security` block MAY carry extension
+fields — the estate's contractiles use `probe_scope` and
+`authorised_probes_only` — but no conforming reader may let an extension field
+*weaken* a rule in this document. An unknown field that grants access is not
+an extension, it is a vulnerability.
+
+== The component pedigree
+
+=== K9-S001 — the pedigree block
+
+A component MUST declare a top-level `pedigree` record. Without one there is
+no leash, no capability grant and no identity: nothing for a host to enforce
+and nothing for a receipt to attribute.
+
+=== K9-S003 — `component_type` is required
+
+`pedigree.component_type` MUST be present, non-empty, and MUST NOT be an
+unfilled placeholder (`TODO`, `FIXME`, `XXX`).
+
+This is the rule that makes a *presence* check into a *content* check. Before
+it, `.machine_readable/svc/k9/template-hunt.k9.ncl` satisfied every field
+check in the estate while declaring its own type as
+`"TODO: describe component type"`. A field that exists and says nothing is
+indistinguishable from a field that was never written, except that it passes
+the gate.
+
+A contractile component MUST set `component_type` to `contractile:<verb>`
+(for example `contractile:must`). This is the disambiguation promised in the
+naming-hazard block: the contractiles family owns its verbs, and this contract
+only ever sees a string with a reserved prefix.
+
+=== `pedigree.security`
+
+[cols="2,2,1,3",options="header"]
+|===
+|Field |Type |Default |Notes
+|`leash` |`'Kennel \| 'Yard \| 'Hunt` |— |REQUIRED, closed (§7)
+|`trust_level` |String |`"unset"` |Human-readable; never consulted for a
+decision
+|`allow_network` |Bool |`false` |Requests `net.fetch` (§8.4)
+|`allow_filesystem_write` |Bool |`false` |Requests `fs.write` (§8.4)
+|`allow_subprocess` |Bool |`false` |Requests `process.spawn` (§8.4)
+|`signature_required` |Bool |`false` |MUST be `true` when `leash = 'Hunt`
+(K9-S008)
+|`capabilities` |Array of §8 names |`[]` |The grant. Default-deny.
+|===
+
+`trust_level` deserves a warning. It reads like the thing that decides, and it
+decides nothing: it is a label. Every decision in this specification is taken
+from `leash`, `capabilities` and the runtime evidence of §9. A host that
+consults `trust_level` is non-conforming.
+
+=== K9-S005 — `pedigree.metadata`
+
+`metadata.name` MUST be present, non-empty, and not a placeholder. `version`,
+`description` and `author` are OPTIONAL.
+
+A receipt records what ran. An anonymous component produces a receipt that
+attributes nothing, which defeats the point of having receipts.
+
+=== K9-S010 — `side_effects` is mandatory to declare at Hunt
+
+`pedigree.side_effects` is an OPTIONAL `Array String` in general, but a
+component at `'Hunt` MUST declare at least one entry and none of them may be a
+placeholder.
+
+The reason is §9. A Hunt run requires a `dry_run` precondition: a plan was
+produced *and reviewed*. A reviewer cannot review a plan for a component that
+claims network, filesystem and subprocess access while describing none of it.
+An empty `side_effects` list at `'Hunt` makes one of the five preconditions
+impossible to discharge honestly, so it is refused at the pedigree rather than
+discovered at the gate.
+
+=== `pedigree.warnings`
+
+An OPTIONAL `Array String` of advisory notices shown to a human before a run.
+Advisory to the reader, never a control: a warning is not a precondition and
+MUST NOT be treated as one.
+
+=== K9-S011 — `recipes` forces `'Hunt`
+
+`config`, `recipes` and `validation` are OPEN records; the contract shapes
+them but does not constrain their contents. One rule is not negotiable: a
+non-empty `recipes` block is a list of shell commands, i.e. an execution
+surface, and a component declaring one MUST be at `'Hunt`.
+
+Declaring recipes at `'Yard` asks a host to *believe* the leash rather than
+check it, which is the exact inversion the leash exists to prevent.
+
+=== `pedigree.signature`
+
+See §10. The block is OPTIONAL at the contract level and REQUIRED at `'Hunt`.
+
+== Leash taxonomy
+
+=== K9-S004 — a closed set of three
+
+The leash taxonomy is a *closed* enumeration:
+
+[cols="1,3,3",options="header"]
+|===
+|Level |Permits |Typical use
+|`'Kennel` (rank 0) |Nothing. Read, parse, display. No evaluation of any kind. |Static data, templates, metadata.
+|`'Yard` (rank 1) |Nickel contract evaluation. No filesystem, no network, no subprocess. Pure. |Typed configuration, validated settings.
+|`'Hunt` (rank 2) |Triad execution — only when all five preconditions of §9 hold. |Deployments, installers, system changes.
+|===
+
+`security.leash` MUST be one of these three. An unknown tag is a *contract
+violation*, not a warning and not a downgrade: a fourth level whose meaning
+each host invents is exactly how a component marked "restricted" ends up with
+full access on one implementation and none on another.
+
+Adding a fourth level is a MAJOR change to this contract.
+
+The contract exposes the closed set twice on purpose — as the `SecurityLevel`
+enum used in the `Security` record, and as the `leash_levels` list a validator
+can read without a Nickel toolchain. The validator's `--self-test` asserts the
+two agree, so the mirror cannot drift.
+
+=== Capability differences
+
+[cols="2,1,1,1,1,1,1",options="header"]
+|===
+| |Nickel eval |Just recipes |must shim |Network |FS write |Subprocess
+|`'Kennel` |no |no |no |no |no |no
+|`'Yard` |*yes* |no |no |no |no |no
+|`'Hunt` |*yes* |*yes* |*yes* |*yes* |*yes* |*yes*
+|===
+
+The `'Yard` row is the whole value of the middle level: a component can be
+*evaluated* — its contracts checked, its configuration typechecked — without
+being able to touch anything. That is what makes it safe to open an untrusted
+`.k9.ncl` in a reader.
+
+=== Detection versus declaration
+
+A reader MAY compute the level a component *needs* from its contents (the
+`detect_level` heuristic in link:../leash.ncl[`leash.ncl`]). A reader MUST NOT
+enforce a level *laxer* than the component declares.
+
+=== Monotonicity
+
+A host MAY enforce a stricter level than declared — running a `'Hunt`
+component at `'Yard` is always permitted, and is what §9 mandates when any
+precondition is unmet. A host MUST NOT enforce a laxer one. There is no
+configuration, flag or evidence combination that makes `'Kennel` evaluate or
+`'Yard` write to disk.
+
+== Capability model
+
+=== K9-S006 — closed core, reserved extension namespace
+
+K9 is *default-deny*: a component is granted no capability unless it is
+explicitly listed in `pedigree.security.capabilities`.
+
+The core set is **closed and exhaustive**. Adding or removing a core name is a
+MAJOR change to this contract.
+
+[cols="2,4",options="header"]
+|===
+|`fs.read` |Read named filesystem paths.
+|`fs.write` |Write named filesystem paths.
+|`net.fetch` |Outbound network fetch to named hosts.
+|`process.spawn` |Spawn a child process.
+|`container.run` |Run a container image.
+|`secret.read` |Read a named secret.
+|`deploy.apply` |Apply a deployment.
+|`rollback.apply` |Apply a rollback.
+|===
+
+=== K9-S006 — capability name shape
+
+A capability name MUST be either a core name (§8.1) or a well-formed extension
+of the form `x-<vendor>.<path>` (for example `x-acme.gpu.alloc`):
+
+* the `x-` prefix;
+* a non-empty vendor segment;
+* at least one `.` after that segment.
+
+So `x-acme.gpu.alloc` is well-formed; bare `x-acme` is not (no path), and
+`x-.gpu` is not (no vendor). Reserving the namespace is what stops a vendor
+name from being silently promoted into a core meaning later.
+
+Core names (no `x-` prefix) are reserved to this specification.
+
+=== The grant
+
+`pedigree.security.capabilities` is an explicit allow-list. Default-deny is
+expressed by the *empty* grant: it permits nothing, and "nothing" is the
+correct reading of an absent grant rather than an error.
+
+=== K9-S007 — a security flag is a request that must be paid for
+
+This is the rule that makes the grant load-bearing, and it is new in this
+specification.
+
+A security flag in `pedigree.security` is a *request* for a capability:
+
+[cols="2,2",options="header"]
+|===
+|`allow_network = true` |requires `net.fetch`
+|`allow_filesystem_write = true` |requires `fs.write`
+|`allow_subprocess = true` |requires `process.spawn`
+|===
+
+Every capability a component's flags request MUST appear in its grant. A
+component with `allow_network = true` and an empty grant is **invalid**, not
+merely unwise: it asks for the network while granting itself nothing.
+
+Before #1058 the flags and the grant were two unrelated opinions in the same
+block, so "default-deny" denied nothing — a component could declare full
+network and filesystem access and be checked against a grant that was empty,
+with no rule connecting them.
+
+This *strengthens* the model. It does not weaken any existing requirement: a
+component that was valid before and is invalid now was one whose pedigree
+contradicted itself.
+
+=== Enforcement point
+
+The leash checks the grant before any Hunt-level action. An action needing an
+ungranted capability is refused *even at* `'Hunt`, and the refusal is recorded
+in the receipt with the exact deficit (the `denied` function in the contract).
+
+== Hunt preconditions
+
+=== All five, always
+
+Owner directive 2026-06-03, restated here and **not relaxed by anything in
+this specification**: `'Hunt` requires *all five* of the following, *always*.
+There is no configurable subset, and a valid signature alone is NOT
+sufficient.
+
+[cols="1,4",options="header"]
+|===
+|Precondition |Meaning
+|`signature` |A *verified* Ed25519 signature over the payload hash (§10.4).
+|`policy` |An explicit policy decision of `allow`.
+|`sandbox` |An isolation sandbox is in force for the run.
+|`dry_run` |A dry-run plan was produced *and reviewed* (see §6.5).
+|`capability_grant` |Every requested capability is explicitly granted
+(default-deny, §8).
+|===
+
+=== K9 gate: `authorize_hunt(evidence)`
+
+The host supplies one Boolean of *evidence* per precondition. Evidence is a
+runtime fact, not a static component field — which is why `check_level` in
+`leash.ncl` can never authorise Hunt on its own, and always returns
+`permitted = false` for a Hunt request.
+
+`authorize_hunt` permits `'Hunt` if and only if all five evidence flags are
+true. Otherwise it returns `permitted = false`, `enforced_level = 'Yard`, and
+the exact list of unmet preconditions, which the receipt records.
+
+The contract's `authorize_hunt` and `leash.ncl`'s `authorize_hunt` are
+semantically identical, and deliberately so: a host implementing the contract
+and a host implementing `leash.ncl` must reach the same verdict on the same
+evidence. The conformance suite asserts the precondition *lists* are equal so
+the two cannot drift.
+
+=== Evidence provenance
+
+Each precondition's evidence MUST come from the layer that can actually
+establish it:
+
+[cols="1,2,2",options="header"]
+|===
+|Precondition |Established by |MAY be established by a lexical check?
+|`signature` |L3, a cryptographic verifier |*no* (§10.4)
+|`policy` |the host's policy engine |no
+|`sandbox` |the host's isolation layer |no
+|`dry_run` |a produced and reviewed plan |no
+|`capability_grant` |§8 arithmetic over the pedigree |L1/L2 may compute it
+|===
+
+`capability_grant` is the only precondition a static analysis can discharge,
+because it is a property of the file. The other four are properties of the
+*run*, and a file cannot attest to them.
+
+=== What is NOT authorisation
+
+Conformance is not authorisation. A component that satisfies every rule in
+this document is a *well-formed request* to run. It is not permitted to run.
+An implementation that reports "valid, therefore authorised" has collapsed
+§12's layers into one and re-created the alpha's signature-only gate that the
+2026-06-03 directive removed.
+
+=== Fail-closed
+
+Any unmet precondition refuses execution and downgrades the enforced level to
+`'Yard`. There is no partial Hunt, no "Hunt without network", and no
+precondition that may be waived by the component itself. A component cannot
+grant itself evidence.
+
+== Signature semantics
+
+This section exists because *presence* and *verification* are different facts,
+and conflating them is how a lexical check becomes an execution licence.
+
+=== K9-S008 / K9-S009 — presence, per leash
+
+A component at `'Hunt` MUST set `pedigree.security.signature_required = true`
+(K9-S008) and MUST carry a `pedigree.signature` block (K9-S009).
+
+At `'Kennel` and `'Yard` a signature block is OPTIONAL and its absence is
+correct, not a defect: a data-only component has nothing to sign for.
+
+=== K9-C001 — the verdict
+
+A reader MUST report a signature in exactly one of four states:
+
+[cols="2,2,3",options="header"]
+|===
+|Verdict |Inputs |Meaning
+|`'Absent` |no signature block |Nothing was claimed.
+|`'Present_Unverified` |block present, no verifier ran |A *lexical* fact only:
+the file says it was signed.
+|`'Verified` |block present, verifier accepted |A *cryptographic* fact.
+|`'Rejected` |block present, verifier refused |A *cryptographic* fact.
+|===
+
+The contract computes this with `signature_verdict has_block check`, where
+`check` is `'Not_Run | 'Passed | 'Failed`.
+
+=== What may not be inferred
+
+Note what is absent from the table above: *there is no input that turns
+`'Not_Run` into `'Verified`.* An implementation cannot infer verification from
+presence, and a reader that reports `'Verified` without having run a verifier
+is non-conforming.
+
+A signature block is a *claim*. Reading it proves the file says it was signed.
+It does not prove the file was signed, and it does not prove the signature
+covers the bytes about to be executed.
+
+=== K9-Hunt: only `'Verified` counts
+
+The `signature` precondition of §9 is satisfiable by `'Verified` and by
+nothing else. `'Present_Unverified` yields `false`.
+
+This single mapping — `hunt_signature_evidence verdict = (verdict == 'Verified)`
+— is the reason the contract cannot be replaced by a grep, and it is the
+difference between this specification and a validator that counts fields.
+
+=== The canonical validator does not verify signatures
+
+`tools/k9-validate.sh` deliberately embeds no verifier. Verifying an Ed25519
+signature means *trusting a key*, and key trust is a host policy decision, not
+a file-format rule. Instead the validator:
+
+* reports `'Present_Unverified` for any component carrying a signature block,
+  as a SKIPPED check rather than a pass;
+* accepts an external verifier through `K9_SIG_VERIFIER`, and reports
+  `'Verified` or `'Rejected` from its exit status;
+* states in its output that `'Present_Unverified` does not authorise `'Hunt`.
+
+A format conformance suite tests the format. Cryptographic verification is a
+host obligation, and this document specifies its semantics rather than
+pretending to discharge it.
+
+== Libraries and imports
+
+=== The library dialect
+
+A library is a Nickel file with *no* `K9!` envelope, *no* top-level `pedigree`
+and *no* top-level `leash`. It is imported; it is never executed as a
+component. Its contract is a negative one.
+
+=== K9-S012 — an execution licence needs an envelope
+
+A file without the `K9!` envelope MUST NOT declare a top-level `pedigree`.
+
+A pedigree is an execution licence, and the leash is detected from the
+envelope. Without the magic line, nothing downstream — not `file(1)`, not a
+MIME handler, not a reader's classifier — can tell the file is a component at
+all. A licence in such a file is *unenforceable*, which is worse than no
+licence, because a reviewer reading the file sees one and believes it.
+
+This is the live state of all six
+`.machine_readable/contractiles/*/*.k9.ncl` files, which carry `pedigree`
+blocks (several at `'Hunt`) and no envelope. Migration item M2.
+
+=== K9-S014 — no stray leash claims
+
+A leash MUST appear only at `pedigree.security.leash`. A top-level `leash`
+field — with or without an envelope — is read by nothing that applies this
+contract, so the file declares a security level no host enforces.
+
+This is the live state of `2-protocols/axel/config/*.k9.ncl`. Migration item
+M3.
+
+=== K9-S013 — every import must resolve
+
+Every `import "path"` in a component or library MUST resolve to a file that
+exists.
+
+A dangling import is not a style problem. A component's pedigree is routinely
+built by *merging* an imported base (`pedigree = base.pedigree_schema & {...}`),
+so an unresolvable import means the pedigree a reviewer read is not the
+pedigree a host would evaluate — and the reviewer's reading is the one that
+decides whether the component is trusted.
+
+All six contractile `.k9.ncl` files import `"../k9/template-hunt.k9.ncl"`, a
+path that does not exist (`.machine_readable/contractiles/` has no `k9/`
+subdirectory), and then reference `base_k9.pedigree_schema`, a field the real
+template does not define — it is `_base.ncl` that defines `pedigree_schema`.
+Migration item M2.
+
+=== Library leash
+
+A library has no leash. Its permissions are the intersection of the components
+that import it and the host's own restrictions; a library cannot widen them.
+An `import` MUST NOT be able to raise the effective leash of the importer, and
+a host MUST evaluate an imported library at a level no laxer than the
+importer's enforced level.
+
+== Conformance layers
+
+=== The four layers
+
+[cols="1,2,3,2",options="header"]
+|===
+|Layer |Name |Establishes |Toolchain
+|L0 |Envelope |bytes, encoding, licence, dialect |none
+|L1 |Structural |the pedigree fields the contract requires, lexically |none
+|L2 |Semantic |the body satisfies the contract, in Nickel |`nickel`
+|L3 |Cryptographic |the signature verifies |an external verifier
+|===
+
+=== Why the layers are separate
+
+Each layer has a different *authority*, and collapsing them is the failure
+mode this specification is written to prevent:
+
+* L0 can prove a file *claims* to be K9. It cannot prove the file is valid.
+* L1 can prove a field is *written*. It cannot prove the field is *typed*,
+  because it does not evaluate anything.
+* L2 can prove the body *satisfies the contract*. It cannot prove the run is
+  authorised (§9.4).
+* L3 can prove a signature *verifies against a key the host trusts*. It cannot
+  prove the component should run.
+
+The recurring defect in this estate is a gate that reports the authority of a
+higher layer while performing the work of a lower one — most expensively, a
+Hunt gate satisfied by the *presence* of a signature field (§10.4).
+
+=== K9-S* is provisional
+
+An L1 pass is *provisional*. A reader MUST NOT report conformance on L1 alone
+where a Nickel toolchain is available.
+
+L1 is a bounded lexical scan. Its known limitations are documented in the
+validator: comments are stripped from the first `#`; `m%" … "%` multiline
+strings are skipped wholesale; a key and its `{` on separate lines are not
+joined. None of these can turn a non-conforming file into a *pass* at L2,
+because L2 re-derives every one of those facts from Nickel itself.
+
+The reason L1 exists at all is that it is the only layer a pre-commit hook can
+run without a toolchain — and a hook that fails because a laptop lacks Nickel
+teaches people to pass `--no-verify`.
+
+=== Reporting a check that did not run
+
+A reader MUST report every check it could not run as *SKIPPED*, naming the
+rule and the layer. A SKIPPED check is never a pass.
+
+A reader run in strict mode MUST fail if any required check was skipped. This
+is the estate's standing defence against the gate that could never fire
+(standards#49, #64): a validator with no toolchain must not be able to report
+green. `tools/k9-validate.sh --strict` exits `3` in exactly that situation,
+and says so in words rather than in an exit code alone.
+
+=== Exit codes
+
+[cols="1,3",options="header"]
+|===
+|`0` |Conforming at the requested layers.
+|`1` |At least one violation.
+|`2` |Usage error, or the normative contract could not be found.
+|`3` |Conforming so far as it could check, but required checks were SKIPPED
+(strict mode).
+|===
+
+== Validators
+
+=== One rule set, three callers
+
+The rules live in exactly one place: `spec/contract/k9_contract.ncl`, with
+this document as its prose. Three callers consume them, and none of them owns
+a rule:
+
+[cols="2,2,3",options="header"]
+|===
+|Caller |Path |Role
+|Canonical validator |`1-formats/k9/tools/k9-validate.sh` |The reference
+implementation. Owns the layering, the rule ids and the fixtures.
+|Local gate |`.githooks/validate-k9.sh` |Thin caller. Owns *policy* about
+which files block a commit, and nothing else.
+|CI gate |`.github/workflows/k9-contractile.yml` |Installs Nickel (pinned,
+sha256-verified, same pin as `ci-pipeline.yml`) and runs the validator
+`--strict`, plus the fixtures, plus the corpus through the same hook.
+|===
+
+=== What the local gate used to do
+
+Until standards#1058 the hook implemented its own idea of a K9 file: it
+grepped for a line beginning `contract` and warned if no SPDX identifier
+appeared in the first five lines. *Not one* of the 30 tracked `*.k9` /
+`*.k9.ncl` files in this repository contains a line beginning `contract`, so
+the hook reported 30 errors on a clean tree and exited 1 — while having no
+rule in common with any specification.
+
+That was not a weak implementation of the contract. It was an implementation
+of something else that happened to share a filename, which is the precise
+question #1058 asked: whether the estate's validators check a *specified*
+contract or each consumer's local assumption. This one checked its own.
+
+=== The debt ratchet
+
+The contract landed after 25 files did, so the local gate cannot turn them all
+red at once; that is how this estate has twice ended up deleting a gate rather
+than fixing the files (see the A2ML notes in `.githooks/pre-commit`). Instead:
+
+[cols="3,2",options="header"]
+|===
+|A file changed by this commit that does not conform |FAIL
+|A file in the ledger that now conforms |FAIL (stale entry)
+|An unlisted file that does not conform |FAIL
+|A listed, *unchanged* file that does not conform |advisory
+|===
+
+`.machine_readable/k9-contract-debt.txt` is therefore shrink-only in practice:
+fixing a file forces its entry out, and editing a listed file removes its
+protection for that commit. The residual risk — a contributor adding a path to
+the ledger instead of fixing it — is real and is called out here rather than
+hidden; review is the control, as it is for `.machine_readable/inline-python-allow.txt`.
+
+== Conformance suite
+
+=== Layout
+
+[source]
+----
+1-formats/k9/tools/fixtures/
+├── valid/     5 positive controls
+└── invalid/   21 negative controls
+               (19 assertable without a toolchain, 2 needing Nickel)
+----
+
+=== The negative controls are the point
+
+A validator that accepts everything passes every positive fixture, so a suite
+of positives alone proves nothing. It is the `invalid/` corpus that shows the
+gate can fire — and #1058 says so explicitly: *"a grammar with no rejecting
+validator is the same class of artefact"* as the gates that could never fire.
+
+Each negative fixture is named `L<layer>-<rule>-<reason>.k9.ncl`, and the
+runner asserts three things about it:
+
+. the file is *rejected*;
+. it is rejected *by the rule its name claims*;
+. it is rejected *at the layer its name claims*.
+
+The second and third assertions are what stop a fixture from passing for the
+wrong reason. A fixture that trips an unrelated earlier check still gets
+rejected, and a suite that only checked rejection would report that as a pass
+while the rule under test does nothing.
+
+=== Running it
+
+[source,bash]
+----
+# built-in assertions: the mirrors, the arithmetic, the extractor, the strip
+1-formats/k9/tools/k9-validate.sh --self-test
+
+# the corpus: 5 positive + 21 negative
+1-formats/k9/tools/k9-validate.sh --fixtures 1-formats/k9/tools/fixtures
+
+# with Nickel on PATH, every format layer must actually run
+1-formats/k9/tools/k9-validate.sh --strict --fixtures 1-formats/k9/tools/fixtures
+
+# one file, machine-readable
+1-formats/k9/tools/k9-validate.sh --json path/to/component.k9.ncl
+----
+
+=== Fixtures are excluded from corpus scans
+
+A repo-wide scan MUST skip `1-formats/k9/tools/fixtures/`. Scanning the
+negative controls as if they were components reports them as violations — and
+worse, a "fix" that made them pass would be a fix that broke the suite.
+
+Two further consequences of the fixtures being *evidence* rather than source:
+
+[horizontal]
+Byte preservation:: `1-formats/k9/.gitattributes` carries `-text -eol` for the
+CRLF fixture, because normalising it on commit would silently delete a negative
+control while leaving the file behind.
+Licence exemption:: `.githooks/validate-spdx.sh` exempts
+`fixtures/invalid/*K9-E004*`, and nothing else. A negative control cannot also
+satisfy the rule it tests: `L0-K9-E004-no-spdx.k9.ncl` exists precisely because
+it has no SPDX header. The exemption is keyed to the *rule id in the filename*,
+not to the directory, so the other 20 negative controls still have to carry a
+header and this cannot become a blanket hole in the corpus. A `.ncl` file
+anywhere else without a header is still caught, and that was verified.
+
+== Security considerations
+
+[cols="2,4",options="header"]
+|===
+|Presence is not verification |§10. The single most important property in this
+document. A `signature` block is a claim; `'Verified` requires a verifier.
+|Conformance is not authorisation |§9.4. A well-formed component is a
+well-formed *request*.
+|A flag is a request, not a grant |§8.4. `allow_network = true` with an empty
+grant is invalid, not permissive.
+|Unknown fields cannot relax rules |§5.5. An extension field that grants
+access is a vulnerability, not an extension.
+|A licence without an envelope is unenforceable |§11.2. Worse than no licence,
+because a reviewer sees one.
+|An unresolvable import changes the pedigree |§11.4. What was reviewed is not
+what would run.
+|A skip is not a pass |§12.4. Applies to layers, toolchains and dialects
+alike.
+|Hunt is all five or nothing |§9. No subset, no waiver, no self-granted
+evidence.
+|===
+
+== Relationship to other estate artefacts
+
+=== `SPEC.adoc`
+
+link:../SPEC.adoc[`SPEC.adoc`] remains the format overview: the problem
+statement, the layer model, the triad, the MIME registration path. This
+document replaces its prose description of the contract as the *normative*
+source for conformance. Where `SPEC.adoc` shows an illustrative Nickel sketch,
+`k9_contract.ncl` is the artefact.
+
+=== `pedigree.ncl` — a different contract
+
+link:../pedigree.ncl[`pedigree.ncl`] defines a seven-section pedigree for a
+*repository*: `metadata`, `validation_contract`, `policy`, `deploy_recipe`,
+`recovery_recipe`, `signature`, `docs_rationale`. That is a different subject
+from a component's `pedigree` block, the two shapes are not compatible, and
+they share only a name.
+
+This specification resolves the collision by naming them:
+
+[cols="1,2,2",options="header"]
+|===
+| |Subject |Normative source
+|*Component pedigree* |one `.k9.ncl` file |this document, §6
+|*Repository pedigree* |a K9 repository root |`SPEC.adoc` §The Active Pedigree
+|===
+
+A reader MUST NOT apply one to the other. Unifying them is migration item M6,
+and it is deliberately *not* attempted here: a repository pedigree and a
+component pedigree have different required fields for good reasons, and
+forcing them together to end a naming collision would be the naming collision
+winning.
+
+=== `leash.ncl` and `capabilities.ncl`
+
+link:../leash.ncl[`leash.ncl`] and link:../capabilities.ncl[`capabilities.ncl`]
+predate this contract and encode the same leash set, the same five
+preconditions and the same closed capability list. They are *not* superseded:
+they carry the host-side machinery (`detect_level`, `check_level`, the
+handshake formats) that a contract file has no business holding. The contract
+duplicates the three closed lists, and `--self-test` asserts the mirrors agree
+so the duplication cannot drift silently. Deriving them from one source is
+migration item M6.
+
+=== `coordination.k9`
+
+The root `coordination.k9` and `2-protocols/k9-coordination/examples/minimal.k9`
+are correctly classified as `k9-coordination` and *routed*. They are not
+violations, and this specification makes no claim about them.
+
+[[rule-index]]
+[appendix]
+== Rule index
+
+[cols="1,1,1,4",options="header"]
+|===
+|Rule |Layer |Class |Requirement
+|K9-E000 |L0 |error |The file exists.
+|K9-E001 |L0 |error |Line 1 is exactly `K9!`.
+|K9-E002 |L0 |error |No NUL octet.
+|K9-E003 |L0 |error |LF line endings only.
+|K9-E004 |L0 |error |SPDX identifier in the first five lines.
+|K9-E005 |L0 |error |The body belongs to a known dialect.
+|K9-S001 |L1 |error |Top-level `pedigree` present.
+|K9-S002 |L1 |error |`schema_version` is a dot-triple of this major.
+|K9-S003 |L1 |error |`component_type` present and not a placeholder.
+|K9-S004 |L1 |error |`security.leash` in the closed set.
+|K9-S005 |L1 |error |`metadata.name` present and not a placeholder.
+|K9-S006 |L1 |error |Every capability is core or `x-<vendor>.<path>`.
+|K9-S007 |L1 |error |The grant covers every capability the flags request.
+|K9-S008 |L1 |error |`'Hunt` ⇒ `signature_required = true`.
+|K9-S009 |L1 |error |`'Hunt` ⇒ a `signature` block is *present*.
+|K9-S010 |L1 |error |`'Hunt` ⇒ non-empty `side_effects`, no placeholders.
+|K9-S011 |L1 |error |A `recipes` block ⇒ `'Hunt`.
+|K9-S012 |L0 |error |No envelope ⇒ no top-level `pedigree`.
+|K9-S013 |L1 |error |Every `import` resolves.
+|K9-S014 |L0/L1 |error |No leash claim outside `pedigree.security`.
+|K9-N001 |L2 |error |The body satisfies `K9.Component` / library typecheck.
+|K9-N002 |L2 |error |The normative contract itself typechecks.
+|K9-C001 |L3 |skip/error |Signature verification, where a verifier exists.
+|===
+
+K9-S009 and K9-C001 are deliberately separate rules with separate layers. One
+proves a block exists; the other proves a signature verifies. Nothing in this
+document lets the first satisfy the second.
+
+[[no-abnf]]
+[appendix]
+== Why there is no `k9.abnf`
+
+Ruling D173 answered the question #1058 raised. The reasoning is recorded here
+so the decision does not have to be re-litigated by the next reader:
+
+. *K9 has no syntax of its own.* A component body is a Nickel term. An ABNF
+  covering the whole file would be a partial, drifting restatement of Nickel's
+  grammar, owned by nobody and correct until the next upstream release.
+. *The part that is K9's own is three bytes.* `K9!` is specified in §3.1 as an
+  octet sequence, which is more precise than a grammar production would be and
+  needs no parser generator.
+. *The load-bearing gap was never lexical.* What was missing was a normative
+  statement of what a pedigree must contain and what a host must check before
+  executing one. A grammar cannot express "the grant must cover what the flags
+  request" or "presence is not verification"; a contract can, and does.
+. *The sibling format that does need a grammar has one.* `k9-coordination` is
+  YAML-bodied with its own syntax, and
+  `coordination-k9-grammar_v1.1.abnf` is the right artefact for it. The
+  difference is not inconsistency; it is that one format has a syntax and the
+  other borrows one.
+
+The only lexical rules in this document are the envelope's, and they are stated
+as bytes and as a first-significant-line table precisely so that no reader has
+to infer a grammar from prose.
+
+[appendix]
+== References
+
+* https://nickel-lang.org[Nickel Language] — normative by reference (§3.5)
+* RFC 2119 — Key words for use in RFCs to Indicate Requirement Levels
+* RFC 8017 / RFC 8032 — Ed25519
+* link:../SPEC.adoc[K9 SVC Specification]
+* link:../IANA-MEDIA-TYPE-APPLICATION.adoc[`application/vnd.k9` media type]
+* link:../../../2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.1.abnf[K9 Coordination File Grammar v1.1.0]
+* standards#1058 (grammar artifacts), ruling D173; standards#837, #856, #752, #49, #64
+
+[appendix]
+== License
+
+SPDX-License-Identifier: CC-BY-SA-4.0
diff --git a/1-formats/k9/spec/MIGRATION-1058.adoc b/1-formats/k9/spec/MIGRATION-1058.adoc
new file mode 100644
index 000000000..fffecb9d6
--- /dev/null
+++ b/1-formats/k9/spec/MIGRATION-1058.adoc
@@ -0,0 +1,358 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= K9 Contract Migration Plan — standards#1058
+:subtitle: From "no contract at all" to a gated one, without a red wall
+:revnumber: 1.0
+:revdate: 2026-10-03
+:toc: left
+:toclevels: 3
+:sectnums:
+
+== What landed, and what it costs
+
+link:K9-CONTRACT-SPEC.adoc[K9-CONTRACT-SPEC v1.0.0] is now the normative
+contract for `application/vnd.k9`, with
+link:contract/k9_contract.ncl[`contract/k9_contract.ncl`] as its
+machine-readable form, link:../tools/k9-validate.sh[`tools/k9-validate.sh`] as
+the canonical validator, and link:../tools/fixtures/[`tools/fixtures/`] as the
+conformance suite (5 positive controls, 21 negative).
+
+Landed with it:
+
+[cols="2,4"]
+|===
+|`.githooks/validate-k9.sh` |Rewritten. It owned its own rule set (`grep '^contract'`,
+which no file in this repo has); it now delegates and owns only commit policy.
+|`.githooks/validate-lint-format.sh` |Excludes `*.k9.ncl` from the bare
+`nickel typecheck`, matching `ci-pipeline.yml`, and routes K9 files to the gate
+that knows the format.
+|`.github/workflows/k9-contractile.yml` |Installs Nickel (pinned, sha256-verified,
+same pin as `ci-pipeline.yml`) and runs `--self-test`, the fixtures `--strict`,
+and the whole corpus through the same hook.
+|`.machine_readable/k9-contract-debt.txt` |Shrink-only ledger of the 25 files
+that predate the contract.
+|`1-formats/k9/.gitattributes` |`-text -eol` for the CRLF negative control, so
+normalising it on commit cannot silently delete it.
+|`.githooks/validate-spdx.sh` |Exempts `fixtures/invalid/*K9-E004*` — a negative
+control cannot also satisfy the rule it tests. Keyed to the rule id in the
+filename, not the directory, so the other 20 controls still need a header.
+|===
+
+Two of those are gate changes made *because* the fixtures exist, and both were
+verified in both directions: the exempted control passes the SPDX gate while a
+`.ncl` file elsewhere without a header still fails it.
+
+=== The baseline, measured
+
+Produced by running the canonical validator over every tracked `*.k9` and
+`*.k9.ncl` outside the fixtures directory:
+
+[source,bash]
+----
+git ls-files -z -- '*.k9' '*.k9.ncl' \
+  | grep -zv '^1-formats/k9/tools/fixtures/' \
+  | xargs -0 1-formats/k9/tools/k9-validate.sh --layer L1 --json
+----
+
+[cols="2,1,4"]
+|===
+|Files in scope |30 |
+|Conforming |*5* |3 components pass; 2 `coordination.k9` files are *routed*
+|Non-conforming |*25* |13 violations, 12 unclaimed-dialect errors
+|===
+
+By dialect: 8 component, 8 library, 2 coordination (routed), 12 unclaimed.
+
+Rule incidence across the 25:
+
+[cols="1,1,4"]
+|===
+|K9-E004 |11 |No SPDX identifier — the 11 `PROTOCOL.k9` stubs missing one.
+|K9-E005 |12 |Body belongs to no K9 dialect — the 12 `PROTOCOL.k9` stubs.
+|K9-S003 |3 |`component_type` is a `TODO` placeholder — the three templates.
+|K9-S004 |1 |`security.leash` missing — `rsr-compliance-checklist.k9.ncl`.
+|K9-S005 |4 |`metadata.name` missing or a placeholder.
+|K9-S007 |2 |Security flags request capabilities the grant does not cover.
+|K9-S009 |2 |`'Hunt` with no `signature` block.
+|K9-S010 |4 |`'Hunt` with empty or placeholder `side_effects`.
+|K9-S012 |6 |Pedigree in a file with no `K9!` envelope — the 6 contractiles.
+|K9-S013 |6 |Unresolvable `import` — the same 6 contractiles.
+|K9-S014 |3 |Leash claim outside `pedigree.security`.
+|===
+
+== Why this is a ratchet and not a wall
+
+Turning 25 files red in one commit is how this estate has twice ended up
+*deleting a gate* rather than fixing the files. The A2ML note in
+`.githooks/pre-commit` records the shape of it exactly: a validator that passed
+0 of 222 tracked files meant no commit could be made, so the validator was
+removed.
+
+`.githooks/validate-k9.sh` therefore fails on three things and advises on one:
+
+[cols="3,2"]
+|===
+|A file this commit touches that does not conform |FAIL
+|A ledger entry whose file now conforms |FAIL (stale)
+|An unlisted file that does not conform |FAIL
+|A listed, *unchanged* file that does not conform |advisory
+|===
+
+All four paths were exercised against the hook before this plan was written:
+touching `.machine_readable/contractiles/must/must.k9.ncl` fails, adding a
+conforming path to the ledger fails as stale, a new non-conforming file fails,
+and an untouched listed file reports as debt.
+
+The residual risk is honest and stated in §13.3 of the spec: a contributor can
+add a path to the ledger instead of fixing it. Review is the control, as it is
+for `.machine_readable/inline-python-allow.txt`.
+
+== Migration items
+
+Ordered by value-per-risk. Each item names the rules it clears and the ledger
+entries it removes, so "done" is checkable rather than a matter of opinion.
+
+=== M1 — Six contractile components have no envelope and a dangling import
+
+*Files:* `.machine_readable/contractiles/{adjust,bust,dust,intend,must,trust}/*.k9.ncl`
+*Rules cleared:* K9-S012 (6), K9-S013 (6) · *ledger entries removed:* 6
+
+Each of the six carries a `pedigree` block — four of them at `'Hunt` — with no
+`K9!` magic on line 1. Per §11.2 an execution licence in a file with no
+envelope is *unenforceable*: nothing downstream can detect the leash, because
+the leash is detected from the envelope. A reviewer reading the file sees a
+licence and believes it.
+
+Each also begins:
+
+[source,nickel]
+----
+let base_k9 = import "../k9/template-hunt.k9.ncl" in
+----
+
+`.machine_readable/contractiles/` has no `k9/` subdirectory, so the import does
+not resolve; and the real template (`.machine_readable/svc/k9/template-hunt.k9.ncl`)
+defines `pedigree`, not the `pedigree_schema` these files then merge from.
+`_base.ncl` is what defines `pedigree_schema`. So the pedigree a reviewer reads
+is not the pedigree a host would evaluate — which is precisely why §11.4 makes
+a dangling import a conformance failure rather than a style note.
+
+*Work:*
+
+. Add `K9!` as line 1 to all six (they are components, not libraries).
+. Point the import at a file that exists — `_base.ncl` for `pedigree_schema`, or
+  a new `.machine_readable/contractiles/k9/` base if a contractile-specific
+  base is wanted.
+. Add `component_type = "contractile:<verb>"` (§6.2) — this is also the
+  resolution of the `must` naming collision the issue raised: the contractiles
+  family keeps its verbs, and the K9 contract only ever sees a reserved prefix.
+. Confirm `capabilities` covers whatever `allow_*` flags each verb sets
+  (K9-S007, §8.4). `must` and `trust` set `allow_subprocess = true`, so they
+  need `process.spawn`.
+
+*Blocks:* nothing. *Blocked by:* nothing. This is the highest-value item: six
+files, twelve rule instances, and it closes the only place in the repo where a
+`'Hunt` pedigree is invisible to every tool.
+
+=== M2 — Twelve `PROTOCOL.k9` stubs claim a reserved suffix
+
+*Files:* `3-practice/session-management-standards/*/*/PROTOCOL.k9`
+*Rules cleared:* K9-E005 (12), K9-E004 (11) · *ledger entries removed:* 12
+
+These are YAML stubs for a session-management protocol. They are neither K9 SVC
+(no Nickel body) nor `k9-coordination` (no `K9!` magic, and a different schema
+again). `.machine_readable/scorecards/session-management-standards.scorecard.a2ml`
+already flags the collision in its own words: *".k9 files that don't follow the
+actual K9 grammar could confuse tooling or reviewers who expect the k9-svc
+schema."*
+
+Two acceptable outcomes, owner's choice:
+
+[horizontal]
+(a) *Rename off the suffix* — `PROTOCOL.yaml`. Cheapest, and correct if these
+are ordinary structured data.
+(b) *Adopt a dialect* — if a session-management protocol is meant to be
+machine-consumed as K9, give it the `K9!` envelope and either the Nickel
+component shape or a registered dialect of its own.
+
+*Note:* the same scorecard references
+`1-formats/k9/actions/validate/validate-k9.sh`, a path that does not exist
+(`ls` confirms no `1-formats/k9/actions/`). Whatever is chosen, that reference
+should be repointed at `1-formats/k9/tools/k9-validate.sh`.
+
+=== M3 — Three templates ship placeholders and one example is unsigned
+
+*Files:* `.machine_readable/svc/k9/template-{hunt,kennel,yard}.k9.ncl`,
+`.machine_readable/svc/k9/examples/setup-repo.k9.ncl`
+*Rules cleared:* K9-S003 (3), K9-S005 (3), K9-S007 (2), K9-S009 (2),
+K9-S010 (3) · *ledger entries removed:* 4
+
+Two separate problems in one directory.
+
+*The templates.* `template-hunt.k9.ncl` declares
+`component_type = "TODO: describe component type"`, `name = "TODO: component-name"`,
+and a `side_effects` list made entirely of `TODO` lines. §6.2 and §6.5 refuse
+placeholders on purpose: a field that exists and says nothing is
+indistinguishable from a field that was never written, except that it passes
+the gate.
+
+But a *template* is not a component — it is never loaded. The right fix is to
+stop claiming the component suffix for it: rename to
+`template-*.k9.ncl.in` (or move them under a `templates/` directory with a
+non-reserved suffix) and keep the placeholders, which are the point of a
+template. Adding them to the ledger instead would be recording a defect that
+should not exist.
+
+*The example.* `setup-repo.k9.ncl` is a real component at `'Hunt` that sets all
+three `allow_*` flags, grants no capabilities (K9-S007), carries no
+`signature` block (K9-S009), and declares no `side_effects` (K9-S010). It is
+the clearest single illustration of why §8.4 exists. Fix it as a component:
+grant `net.fetch`, `fs.write`, `process.spawn`, add a `signature` block, and
+describe what it actually does.
+
+=== M4 — Two Axel config files declare a leash nothing reads
+
+*Files:* `2-protocols/axel/config/{ci,metadata}.k9.ncl`
+*Rules cleared:* K9-S014 (2) · *ledger entries removed:* 2
+
+Both open with a top-level `leash = 'Kennel,` and no pedigree. A leash outside
+`pedigree.security` is read by nothing that applies this contract, so the files
+declare a security level no host enforces.
+
+Cheapest fix: make them Kennel *components* — add the `K9!` envelope and a
+minimal pedigree. They are project metadata and CI configuration, which is
+exactly what `'Kennel` is for. Alternatively drop the stray `leash` and let them
+be libraries, but then nothing records that they are data-only.
+
+=== M5 — `rsr-compliance-checklist.k9.ncl` is not a single Nickel term
+
+*File:* `rhodium-standard-repositories/rsr-compliance-checklist.k9.ncl`
+*Rules cleared:* K9-S004, K9-S005, K9-S014 · *ledger entries removed:* 1
+
+The file has the envelope and a `pedigree`, but its top level is a *sequence of
+bindings* — `leash = 'Kennel` then `pedigree = { … }` then `rsr_standards = { … }`
+— and a Nickel file must be a single term. The leash sits outside the pedigree
+(K9-S014), the pedigree has no `security` block at all (K9-S004), and it puts
+`author` and `description` at pedigree level rather than in `metadata` (K9-S005).
+
+Restructure into one record with the leash inside `pedigree.security`. This one
+is also the file most likely to fail at L2 once Nickel runs, since the
+top-level binding sequence is a parse error.
+
+=== M6 — Three closed lists are written down three times
+
+*Files:* `1-formats/k9/{leash,capabilities,pedigree}.ncl`,
+`spec/contract/k9_contract.ncl`
+*Rules cleared:* none (hygiene) · *ledger entries removed:* 0
+
+The leash set, the five Hunt preconditions and the eight core capabilities now
+exist in both `leash.ncl` / `capabilities.ncl` and the contract. That
+duplication is deliberate for now — those files carry host-side machinery
+(`detect_level`, `check_level`, the handshake formats) a contract file has no
+business holding — and `--self-test` asserts the mirrors agree, so it cannot
+drift silently.
+
+Deriving them from one source is the right end state. Do it *after* M1–M5, so
+that the change can be verified against a corpus that already conforms rather
+than against one that does not.
+
+Also in scope here: §16.2 of the spec names the collision between the
+*component* pedigree (this contract) and the *repository* pedigree
+(`pedigree.ncl`, seven sections). They are different contracts with the same
+name. This plan deliberately does *not* unify them — a repository pedigree and
+a component pedigree have different required fields for good reasons, and
+merging them to end a naming collision would be the naming collision winning.
+What M6 should do is make the relationship explicit in `SPEC.adoc`.
+
+=== M7 — L2 has never actually run on this corpus
+
+*Rules cleared:* unknown until it runs · *ledger entries removed:* unknown
+
+This is the honest gap in the work. `nickel` is not available in the
+environment where this migration was prepared (the GitHub release-asset host is
+unreachable from it), so **L2 has not been executed against the corpus or the
+fixtures**. Everything asserted in this plan was asserted at L0/L1, plus the
+self-test.
+
+The conformance suite is built so this cannot pass unnoticed: `--strict` exits
+`3` with the message *"no nickel binary — L2 semantics were never checked, so
+this run is not a conformance result"*, and the CI step runs `--strict` with
+Nickel installed. The first CI run on a branch with Nickel will be the first
+time K9 semantics have ever been checked in this repository.
+
+Expect it to find things. At minimum:
+
+* M5's top-level binding sequence is a Nickel parse error;
+* the two `L2-K9-N001-*` negative fixtures become assertable (they are held to
+  be lexically clean by the runner today, which is the precondition for being
+  an L2 control at all);
+* `nickel format --check` has never been run on any `.k9.ncl` body, and may
+  object to all of them.
+
+== Suggested issue breakdown
+
+[cols="1,3,1,2",options="header"]
+|===
+|Issue |Title |Depends |Clears
+|#A |K9 contract: give the six contractile components an envelope and a
+resolvable import |— |M1 · K9-S012 ×6, K9-S013 ×6
+|#B |K9 contract: settle the `PROTOCOL.k9` suffix collision |— |M2 · K9-E005 ×12,
+K9-E004 ×11
+|#C |K9 contract: templates are not components; make `setup-repo` a real
+component |— |M3 · K9-S003 ×3, K9-S005 ×3, K9-S007 ×2, K9-S009 ×2, K9-S010 ×3
+|#D |K9 contract: Axel config files declare a leash nothing reads |— |M4 · K9-S014 ×2
+|#E |K9 contract: restructure `rsr-compliance-checklist` into one Nickel term |— |M5
+|#F |K9 contract: first `--strict` CI run — triage whatever L2 finds |#A–#E |M7
+|#G |K9 contract: derive the closed lists from one source |#F |M6
+|===
+
+#A, #B, #C, #D and #E are independent and can run in parallel. #F should not
+start before them, because triaging a first L2 run is much easier against a
+corpus whose lexical defects are already gone. #G is last for the same reason.
+
+Every one of them ends with the same acceptance test:
+
+[source,bash]
+----
+# the ledger must have shrunk by exactly the entries the issue fixed
+grep -c . .machine_readable/k9-contract-debt.txt
+
+# and the gate must still be able to fire
+1-formats/k9/tools/k9-validate.sh --self-test
+1-formats/k9/tools/k9-validate.sh --fixtures 1-formats/k9/tools/fixtures
+----
+
+A stale ledger entry fails the hook, so an issue that fixes a file without
+shrinking the ledger does not pass. That is the ratchet doing its job.
+
+== What is deliberately NOT in this plan
+
+[horizontal]
+Hunt is unchanged:: All five preconditions, always, no configurable subset, no
+self-granted evidence. Nothing in M1–M7 relaxes §9. Two of the items (M1, M3)
+make `'Hunt` *harder* to reach, by requiring the grant to cover the flags and
+the signature block to be present.
+No ABNF:: Ruling D173. See Appendix B of the spec for the reasoning, recorded
+so it does not have to be re-litigated.
+No signature verification:: §10.5. The canonical validator embeds no verifier,
+because key trust is host policy. M1–M7 require signature *blocks* to be
+present at `'Hunt`; none of them claims to verify one, and a reader that
+reported `'Verified` without a verifier would be non-conforming (§10.3).
+No unification of the two pedigrees:: §16.2, and M6 above.
+
+== Verification status of this document
+
+Every count and path in this plan was produced by running the tools named in
+it, in the repository, at the revision this plan was written against. The two
+exceptions are stated rather than hidden:
+
+* *L2 (Nickel semantics) was not run.* No `nickel` binary was obtainable in the
+  preparation environment. See M7.
+* *`nickel format --check` was not run*, for the same reason. It has never been
+  run on a `.k9.ncl` body in this repository, because `ci-pipeline.yml`
+  excludes that pathspec.
+
+What *was* run, and passed: the validator's 26-assertion self-test; the
+conformance suite (5 positive controls, 19 negative controls asserted, 2 L2
+controls held to be lexically clean); the local hook in all four ratchet paths;
+and the corpus baseline above.
diff --git a/1-formats/k9/spec/contract/k9_contract.ncl b/1-formats/k9/spec/contract/k9_contract.ncl
new file mode 100644
index 000000000..c9d85c0e4
--- /dev/null
+++ b/1-formats/k9/spec/contract/k9_contract.ncl
@@ -0,0 +1,435 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# k9_contract.ncl — THE NORMATIVE K9 COMPONENT CONTRACT (v1.0.0).
+#
+# Ruling D173 (standards#1058, 2026-09-30): "K9 needs a Nickel contract, not an
+# ABNF." This file is that contract. It is normative; the prose that governs it
+# is ../K9-CONTRACT-SPEC.adoc, and where the two disagree the prose wins and
+# this file is a bug.
+#
+# WHAT THIS FILE IS
+#   The closed, versioned, machine-checkable shape of a K9 component's
+#   `pedigree` block, plus the decision functions a host must consult before
+#   it lets a component do anything:
+#
+#     leash_levels / is_leash      §7  the leash taxonomy as a CLOSED set
+#     required_capabilities        §8  what a security flag costs you
+#     granted_ok / denied          §8  default-deny capability arithmetic
+#     authorize_hunt               §9  all five preconditions, always
+#     signature_verdict            §10 presence is NOT verification
+#
+# WHAT THIS FILE IS NOT
+#   * It is not a grammar. K9 has no syntax of its own: the body of a
+#     `.k9.ncl` file is a Nickel term and Nickel's grammar is normative by
+#     reference (K9-CONTRACT-SPEC §3.5). Re-specifying it here, in ABNF or
+#     otherwise, would fork a language we do not own.
+#   * It is not a validator. A contract states what holds; the canonical
+#     validator (../../tools/k9-validate.sh) decides whether a check could be
+#     run at all, and reports a check it could not run as SKIPPED rather than
+#     as a pass.
+#   * It does not verify signatures. Nickel has no cryptographic primitive,
+#     so nothing in this file can produce `signature_check = 'Passed`. See
+#     §10: an implementation that has not run a verifier MUST report 'Not_Run,
+#     and 'Not_Run can never authorise Hunt.
+#
+# NAMING HAZARD — carried from SPEC.adoc, unchanged:
+#   K9's execution triad is  must / just / nickel.
+#   The contractiles family is  must / trust / dust / intend.
+#   `must` appears in both and means different things. Never conflate them.
+#   Nothing in this file names a contractile verb; a contractile component is
+#   an ordinary K9 component whose `component_type` begins "contractile:".
+#
+# API SURFACE DISCIPLINE
+#   Every std function used below is one already exercised by a `.ncl` file
+#   this repository typechecks in CI (capabilities.ncl, leash.ncl,
+#   pedigree.ncl): std.string.length, std.string.substring, std.string.split,
+#   std.string.join, std.array.length, std.array.any, std.array.filter,
+#   std.record.has_field, std.contract.from_predicate. A normative artefact
+#   must not be the first thing in the estate to touch an unexercised corner
+#   of a dependency's standard library.
+#
+# ─────────────────────────────────────────────────────────────────────────
+# Type aliases (top-level `let` — the idiom pedigree.ncl and leash.ncl use)
+# ─────────────────────────────────────────────────────────────────────────
+
+# §7 — the leash taxonomy. CLOSED: three members, and adding a fourth is a
+# MAJOR change to this contract, not an extension.
+let SecurityLevel = [| 'Kennel, 'Yard, 'Hunt |] in
+
+# §10 — the result of an attempted cryptographic check. 'Not_Run is the honest
+# default and it is load-bearing: it is the value a validator reports when no
+# verifier was available, and it must never be silently upgraded.
+let SignatureCheck = [| 'Not_Run, 'Passed, 'Failed |] in
+
+# §10 — what a host may infer from "does the file carry a signature block"
+# (lexical) combined with "did a verifier accept it" (cryptographic).
+let SignatureVerdict = [| 'Absent, 'Present_Unverified, 'Verified, 'Rejected |] in
+
+# §8.1 — the reserved extension namespace prefix.
+let ExtensionPrefix = "x-" in
+
+# ─────────────────────────────────────────────────────────────────────────
+# §5.2 / §8.1 — name shapes, using nothing beyond length and substring
+# ─────────────────────────────────────────────────────────────────────────
+
+let is_digit = fun c =>
+  c == "0"
+    || c == "1"
+    || c == "2"
+    || c == "3"
+    || c == "4"
+    || c == "5"
+    || c == "6"
+    || c == "7"
+    || c == "8"
+    || c == "9" in
+
+# A numeric dot-triple whose MAJOR segment equals `major`. Walks the string
+# once. Rejects: non-digits, a leading or trailing dot, an empty segment, a
+# leading zero in any segment ("1.00.0"), and the wrong number of segments.
+#
+# `prev_dot` starts TRUE so a leading "." is refused by the same branch that
+# refuses ".."; `seg_len` must end > 0 so a trailing "." is refused too.
+let is_semver_of = fun major v =>
+  let want = major ++ "." in
+  let rec go = fun i dots seg_len first_zero s =>
+    if i >= std.string.length s then
+      dots == 2 && seg_len > 0
+    else
+      let c = std.string.substring i 1 s in
+      if c == "." then
+        seg_len > 0 && go (i + 1) (dots + 1) 0 false s
+      else if is_digit c then
+        (first_zero == false || seg_len == 0)
+          && go (i + 1) dots (seg_len + 1) (c == "0") s
+      else
+        false
+  in
+  std.string.length v >= (std.string.length want + 3)
+    && std.string.substring 0 (std.string.length want) v == want
+    && go 0 0 0 false v in
+
+# ─────────────────────────────────────────────────────────────────────────
+# The contract record. Nickel records are recursive, so fields below refer to
+# their siblings by name; the type aliases above stay top-level so no field
+# ever shadows the binding it is defined in terms of.
+# ─────────────────────────────────────────────────────────────────────────
+{
+  # ── §5 Identity and versioning ───────────────────────────────────────
+  #
+  # `contract_version` is the version of THIS file. `schema_major` is the
+  # major segment a conforming component's `pedigree.schema_version` must
+  # carry to be readable by this contract. They are separate numbers on
+  # purpose: this contract can be revised (1.0.0 -> 1.0.1) without changing
+  # what a component must look like.
+  contract_name = "k9-svc-component",
+  contract_version = "1.0.0",
+  schema_major = "1",
+
+  # §4 — the dialects a K9 envelope may carry. A file whose body is not one of
+  # these is not a K9 file, whatever its suffix says.
+  dialect = {
+    # `K9!` envelope + Nickel body declaring a `pedigree`. In scope here.
+    component = "k9-svc-component",
+    # No `K9!` envelope, Nickel body, no top-level `pedigree`. Imported, never
+    # executed. In scope for §11 only.
+    library = "k9-svc-library",
+    # `K9!` envelope + YAML body. Governed by
+    # 2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.1.abnf,
+    # NOT by this contract. Named here so a validator can route it instead of
+    # misreporting it as a broken component.
+    coordination = "k9-coordination",
+  },
+
+  # ── §7 Leash taxonomy — CLOSED SET ───────────────────────────────────
+  #
+  # Machine-checkable enumeration of the three levels in ascending order of
+  # what they permit. This list IS the closed set the prose promises, and it
+  # lives in the same file as the `SecurityLevel` enum it mirrors so the two
+  # cannot drift silently; the conformance suite asserts they agree.
+  leash_levels = ['Kennel, 'Yard, 'Hunt],
+
+  # Total order over the closed set. Used for the monotonicity rule (§7.4): a
+  # host may enforce a level STRICTER than the component declares, never laxer.
+  level_rank = fun l =>
+    if l == 'Kennel then
+      0
+    else if l == 'Yard then
+      1
+    else
+      2,
+
+  is_leash = fun v =>
+    std.array.length (std.array.filter (fun l => l == v) leash_levels) == 1,
+
+  # The leash a component DECLARES. Fail-closed: a pedigree with no readable
+  # `security.leash` ranks as 'Kennel here, and is rejected outright by the
+  # Pedigree contract below. This helper exists so a host handed a partial
+  # pedigree cannot crash on it.
+  leash_of = fun pedigree =>
+    if std.record.has_field "security" pedigree
+      && std.record.has_field "leash" pedigree.security
+    then
+      pedigree.security.leash
+    else
+      'Kennel,
+
+  # ── §8 Capability model — DEFAULT-DENY ───────────────────────────────
+  #
+  # §8.1 CLOSED CORE SET. Exhaustive for the core namespace. Adding or
+  # removing a name here is a MAJOR change to this contract.
+  core_capabilities = [
+    "fs.read",
+    "fs.write",
+    "net.fetch",
+    "process.spawn",
+    "container.run",
+    "secret.read",
+    "deploy.apply",
+    "rollback.apply",
+  ],
+
+  # §8.1 RESERVED EXTENSION NAMESPACE. Non-core names MUST be "x-<vendor>.<p>"
+  # so they can never collide with a future core name.
+  extension_prefix = ExtensionPrefix,
+
+  is_core = fun name => std.array.any (fun c => c == name) core_capabilities,
+
+  # A well-formed extension: starts with the prefix and has at least one "."
+  # after the vendor segment, i.e. "x-vendor.something", never bare "x-vendor".
+  is_extension = fun name =>
+    std.string.length name > std.string.length ExtensionPrefix
+      && std.string.substring 0 (std.string.length ExtensionPrefix) name
+        == ExtensionPrefix
+      && std.array.length (std.string.split "." name) >= 2,
+
+  Capability = std.contract.from_predicate (fun name =>
+    is_core name || is_extension name
+  ),
+
+  # An explicit allow-list. DEFAULT-DENY is expressed by the empty grant: it
+  # permits nothing, and "nothing" is the correct answer for an absent grant.
+  CapabilityGrant = Array Capability,
+
+  default_grant = [],
+
+  permits = fun grant name => std.array.any (fun g => g == name) grant,
+
+  denied = fun grant requested =>
+    std.array.filter (fun r => !(permits grant r)) requested,
+
+  granted_ok = fun grant requested =>
+    std.array.length (denied grant requested) == 0,
+
+  # §8.4 DERIVED REQUIREMENTS — the rule that makes the grant load-bearing.
+  #
+  # A security flag is a REQUEST for a capability, and a request the grant
+  # does not cover is a contradiction inside the pedigree, not a preference.
+  # `allow_network = true` with an empty grant is therefore INVALID, not
+  # merely unwise: the component asks for the network while granting itself
+  # nothing. This STRENGTHENS the pre-#1058 state, where the flags and the
+  # grant were two unrelated opinions in the same block.
+  required_capabilities = fun security =>
+    (
+      if std.record.has_field "allow_network" security
+        && security.allow_network
+      then
+        ["net.fetch"]
+      else
+        []
+    )
+      @ (
+        if std.record.has_field "allow_filesystem_write" security
+          && security.allow_filesystem_write
+        then
+          ["fs.write"]
+        else
+          []
+      )
+      @ (
+        if std.record.has_field "allow_subprocess" security
+          && security.allow_subprocess
+        then
+          ["process.spawn"]
+        else
+          []
+      ),
+
+  # What the grant fails to cover. Empty iff the pedigree is self-consistent.
+  grant_deficit = fun grant security =>
+    denied grant (required_capabilities security),
+
+  # ── §9 Hunt preconditions — ALL FIVE, ALWAYS ─────────────────────────
+  #
+  # Owner directive 2026-06-03, restated and NOT RELAXED by this contract:
+  # Hunt requires all five, always. There is no configurable subset, and a
+  # valid signature alone is not sufficient. Reproduced from leash.ncl
+  # verbatim so the two cannot drift; the conformance suite asserts equality.
+  hunt_preconditions = [
+    "signature",
+    "policy",
+    "sandbox",
+    "dry_run",
+    "capability_grant",
+  ],
+
+  # The host supplies one Bool of EVIDENCE per precondition. Evidence is
+  # runtime fact, not a static component field — which is why `check_level`
+  # in leash.ncl can never authorise Hunt on its own.
+  HuntEvidence = {
+    signature | Bool,
+    policy | Bool,
+    sandbox | Bool,
+    dry_run | Bool,
+    capability_grant | Bool,
+  },
+
+  # §9.2 The gate. Identical semantics to leash.ncl `authorize_hunt`, and
+  # deliberately so: a host implementing this file and a host implementing
+  # leash.ncl must reach the same verdict on the same evidence.
+  authorize_hunt = fun evidence =>
+    let unmet =
+      (if evidence.signature then [] else ["signature"])
+        @ (if evidence.policy then [] else ["policy"])
+        @ (if evidence.sandbox then [] else ["sandbox"])
+        @ (if evidence.dry_run then [] else ["dry_run"])
+        @ (if evidence.capability_grant then [] else ["capability_grant"])
+    in
+    if std.array.length unmet == 0 then
+      {
+        permitted = true,
+        enforced_level = 'Hunt,
+        unmet_preconditions = [],
+      }
+    else
+      {
+        permitted = false,
+        enforced_level = 'Yard,
+        reason =
+          "Hunt requires all five preconditions; unmet: "
+            ++ std.string.join ", " unmet,
+        unmet_preconditions = unmet,
+      },
+
+  # ── §10 Signature semantics — PRESENCE IS NOT VERIFICATION ───────────
+  #
+  # A `signature` block in a pedigree is a CLAIM. Reading it proves the file
+  # says it was signed. It does not prove the file was signed, and it does not
+  # prove the signature covers the bytes about to be executed.
+  signature_checks = ['Not_Run, 'Passed, 'Failed],
+  signature_verdicts = ['Absent, 'Present_Unverified, 'Verified, 'Rejected],
+
+  # §10.2 — the only mapping a conforming implementation may make.
+  #   no block                 -> 'Absent             (nothing was claimed)
+  #   block, verifier passed   -> 'Verified           (cryptographic fact)
+  #   block, verifier rejected -> 'Rejected           (cryptographic fact)
+  #   block, no verifier ran   -> 'Present_Unverified (lexical fact ONLY)
+  #
+  # Note what is absent from that table: there is no input that turns
+  # 'Not_Run into 'Verified. An implementation cannot infer verification from
+  # presence, and a validator that reports 'Verified without having run a
+  # verifier is non-conforming (§10.3).
+  signature_verdict = fun has_block check =>
+    if has_block == false then
+      'Absent
+    else if check == 'Passed then
+      'Verified
+    else if check == 'Failed then
+      'Rejected
+    else
+      'Present_Unverified,
+
+  # §10.4 — the Hunt `signature` precondition is satisfiable by 'Verified and
+  # by nothing else. Presence yields 'Present_Unverified, which is false here.
+  # This is the line that stops a lexical check from becoming an execution
+  # licence, and it is the reason this contract cannot be replaced by a grep.
+  hunt_signature_evidence = fun verdict => verdict == 'Verified,
+
+  # The signature block a component MAY carry. Every field but `algorithm` is
+  # optional at the CONTRACT level, because §10.1 makes presence a per-leash
+  # rule rather than a universal one: 'Kennel and 'Yard components are
+  # ordinarily unsigned, and that is correct rather than a defect.
+  Signature = {
+    algorithm | String | default = "Ed25519",
+    public_key | String | optional,
+    signature | String | optional,
+    payload_hash | String | optional,
+    signed_at | String | optional,
+    key_id | String | default = "primary",
+  },
+
+  # ── §6 The component pedigree, v1 ────────────────────────────────────
+  #
+  # Field-for-field this is the shape the estate's `.k9.ncl` components
+  # actually carry (`.machine_readable/svc/k9/template-*.k9.ncl`), with two
+  # normative tightenings: `component_type` is REQUIRED (§6.2), and the
+  # security flags must be paid for in the capability grant (§8.4).
+
+  Metadata = {
+    name | String,
+    version | String | default = "0.0.0",
+    description | String | optional,
+    author | String | optional,
+  },
+
+  Security = {
+    # §7 — closed set. An unknown tag is a contract violation, not a warning.
+    leash | SecurityLevel,
+    trust_level | String | default = "unset",
+    allow_network | Bool | default = false,
+    allow_filesystem_write | Bool | default = false,
+    allow_subprocess | Bool | default = false,
+    # §10.1 — REQUIRED to be true when leash == 'Hunt. The validator enforces
+    # the implication; this contract cannot, because it is a cross-field rule.
+    signature_required | Bool | default = false,
+    # §8.3 — the explicit grant. Default-deny: absent means empty.
+    capabilities | CapabilityGrant | default = [],
+  },
+
+  Pedigree = {
+    # §5.2 — a numeric dot-triple whose major segment equals `schema_major`.
+    # A component from another major is not "older"; it is unreadable, and
+    # must be refused rather than guessed at (§5.4).
+    schema_version | std.contract.from_predicate (is_semver_of schema_major),
+    # §6.2 — REQUIRED: what this component IS. A template placeholder is not
+    # a value; the canonical validator rejects "TODO" here at L1.
+    component_type | String,
+    security | Security,
+    metadata | Metadata,
+    # §6.5 — advisory to a reader, mandatory to declare. A 'Hunt component
+    # with an empty side_effects list claims full system access and describes
+    # none of it, which the validator rejects at L1.
+    warnings | Array String | default = [],
+    side_effects | Array String | default = [],
+    # §10.1 — the signature claim. Presence is per-leash; see Signature above.
+    signature | Signature | optional,
+  },
+
+  # The whole component: the pedigree plus the optional Nickel payload.
+  # `config`, `recipes` and `validation` stay open on purpose — they are the
+  # component's own business — but §6.7 makes one thing non-negotiable: a
+  # non-empty `recipes` block is an execution surface and therefore forces
+  # 'Hunt. The validator enforces that; this contract only shapes the blocks.
+  Component = {
+    pedigree | Pedigree,
+    # `{ _ : Any }` is the open record: any fields, any values. These three
+    # blocks are the component's own business and the contract deliberately
+    # does not shape them — §6.7's `recipes`-forces-'Hunt rule is enforced by
+    # the validator over the extracted facts, not by a type here. There is no
+    # `Record` builtin in Nickel; this field used to name one, so the contract
+    # itself failed to typecheck and every L2 verdict downstream was void.
+    config | { _ : Any } | optional,
+    recipes | { _ : Any } | optional,
+    validation | { _ : Any } | optional,
+  },
+
+  # ── §11 Library dialect ──────────────────────────────────────────────
+  #
+  # A library is imported; it is never executed as a component and never
+  # carries an envelope. The contract it must satisfy is the negative one:
+  # no pedigree, no leash claim, no execution licence of any kind.
+  is_library = fun lib =>
+    !(std.record.has_field "pedigree" lib)
+      && !(std.record.has_field "leash" lib),
+}
diff --git a/1-formats/k9/tools/README.adoc b/1-formats/k9/tools/README.adoc
new file mode 100644
index 000000000..f6ba54bfa
--- /dev/null
+++ b/1-formats/k9/tools/README.adoc
@@ -0,0 +1,138 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= K9 conformance lane — tools
+Campaign: standards#1058 · Ruling: D173 ·
+Contract: link:../spec/contract/k9_contract.ncl[`spec/contract/k9_contract.ncl` (v1.0.0, normative)] ·
+Prose: link:../spec/K9-CONTRACT-SPEC.adoc[`spec/K9-CONTRACT-SPEC.adoc`]
+
+== What lives here
+
+[cols="1,3"]
+|===
+|`k9-validate.sh` |The canonical validator. The only place K9 rules are
+*executed*; the contract file is where they are *stated*.
+|`fixtures/valid/` |5 positive controls.
+|`fixtures/invalid/` |21 negative controls. The load-bearing half.
+|===
+
+The local gate (`.githooks/validate-k9.sh`) and the CI gate
+(`.github/workflows/k9-contractile.yml`) both call `k9-validate.sh`. Neither
+owns a rule.
+
+== Running it
+
+[source,bash]
+----
+# 1. the validator's own assertions — run this first
+./k9-validate.sh --self-test
+
+# 2. the corpus
+./k9-validate.sh --fixtures fixtures
+
+# 3. with Nickel on PATH, every format layer must actually run
+./k9-validate.sh --strict --fixtures fixtures
+
+# 4. one file
+./k9-validate.sh path/to/component.k9.ncl
+./k9-validate.sh --json path/to/component.k9.ncl
+----
+
+Exit codes: `0` conforming · `1` violation · `2` usage error · `3` required
+checks were SKIPPED under `--strict`.
+
+== The four layers, and why the difference matters
+
+[cols="1,2,3",options="header"]
+|===
+|Layer |Establishes |Needs
+|L0 |the file *claims* to be K9 (bytes, licence, dialect) |nothing
+|L1 |the pedigree fields are *written* |nothing
+|L2 |the body *satisfies the contract* |`nickel`
+|L3 |the signature *verifies* |an external verifier
+|===
+
+Each row is strictly weaker than the one below it, and the recurring defect in
+this estate is a gate that reports the authority of a higher layer while doing
+the work of a lower one. The two most expensive instances, both closed by this
+lane:
+
+* a Hunt gate satisfied by the *presence* of a `signature` field (§10.4 — only
+  `'Verified` counts, and `'Present_Unverified` is false);
+* a lexical pass reported as conformance (§12.3 — L1 is a screen, and a reader
+  MUST NOT report conformance on L1 alone where Nickel is available).
+
+A check that could not run is reported as `SKIPPED`, naming the rule and the
+layer. It is never a pass, and `--strict` turns it into a failure.
+
+== Negative controls
+
+A validator that accepts everything passes every positive fixture, so a suite
+of positives alone proves nothing. `fixtures/invalid/` is what shows the gate
+can fire — standards#1058 says so directly: *"a grammar with no rejecting
+validator is the same class of artefact"* as the gates that could never fire
+(#49, #64).
+
+Each negative fixture is named `L<layer>-<rule>-<reason>.k9.ncl`, and the
+runner asserts three things:
+
+. the file is rejected;
+. it is rejected *by the rule its name claims*;
+. it is rejected *at the layer its name claims*.
+
+Assertions 2 and 3 are what stop a fixture from passing for the wrong reason.
+A fixture that trips an unrelated earlier check still gets rejected, and a
+runner that only checked rejection would report that as a pass while the rule
+under test does nothing.
+
+Coverage, measured: *20 of the 23* rules in the contract have a negative
+control that names them. Of the three that do not:
+
+[horizontal]
+`K9-C001` |Asserted in `--self-test` with a stub verifier rather than by a
+fixture, because no fixture can make a verifier appear. All three verdicts a
+host can reach are exercised there.
+`K9-N002` |A self-check on the contract file itself, run before the contract is
+used to judge anything.
+`K9-E000` |A usage error (the file does not exist), not a conformance rule.
+
+=== The two L2 controls
+
+`L2-K9-N001-wrong-field-type.k9.ncl` and
+`L2-K9-N001-two-segment-version.k9.ncl` are rejected *only* by Nickel:
+
+* `allow_network = "yes"` is spelled correctly, sits at the right path and
+  carries a value — it is just a `String` where the contract requires a `Bool`.
+  L1 has no notion of a type.
+* `schema_version = "1.0"` has the right major and only digits and dots, so L1's
+  bounded screen accepts it. §5.2 requires a dot-*triple*, and it is the
+  contract's `is_semver_of` that counts the segments.
+
+Between them they are the argument for the layering. Without a `nickel` binary
+the runner does not pretend to assert them: it verifies the half it *can* —
+that they are lexically clean, which is the precondition for being an L2
+control at all — reports `SKIP`, and `--strict` refuses the run outright.
+
+== Byte-preserved fixtures
+
+`L0-K9-E003-crlf.k9.ncl` exists to be rejected for its line endings.
+`1-formats/k9/.gitattributes` carries `-text -eol` for it, because normalising
+it on commit would delete the negative control while leaving the file behind —
+and a suite whose negative control no longer fails is a suite that reports
+green over nothing.
+
+Corpus scans must skip `fixtures/` entirely, for the mirror-image reason: a
+"fix" that made the negative controls pass would be a fix that broke the suite.
+`.githooks/validate-k9.sh` excludes the directory.
+
+== Adding a rule
+
+. State it in link:../spec/K9-CONTRACT-SPEC.adoc[`K9-CONTRACT-SPEC.adoc`] with
+  a rule id, and add it to the rule index (Appendix A). Rule ids are never
+  renumbered; a withdrawn rule keeps its id.
+. Encode it in link:../spec/contract/k9_contract.ncl[`k9_contract.ncl`] if it
+  is semantic, or in `k9-validate.sh` if it is lexical — and say which layer it
+  belongs to. A rule that cannot say is not ready.
+. Add a negative control named for it, and assert it fires *at the layer you
+  claimed*.
+. If the rule duplicates a list already in `leash.ncl` or `capabilities.ncl`,
+  add a `--self-test` mirror assertion so the duplication cannot drift.
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-E001-bad-magic.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-E001-bad-magic.k9.ncl
new file mode 100644
index 000000000..b3e5830c5
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L0-K9-E001-bad-magic.k9.ncl
@@ -0,0 +1,20 @@
+k9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §3.1: the magic number is exactly 0x4B 0x39 0x21.
+# `k9!` is a different three octets and must not be tolerated: a magic number
+# with a tolerance is not a magic number, and a kernel that sniffs on it would
+# disagree with a validator that forgives it.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "bad-magic",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "bad-magic" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-E002-nul-byte.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-E002-nul-byte.k9.ncl
new file mode 100644
index 000000000..f02109eb7
Binary files /dev/null and b/1-formats/k9/tools/fixtures/invalid/L0-K9-E002-nul-byte.k9.ncl differ
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-E003-crlf.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-E003-crlf.k9.ncl
new file mode 100644
index 000000000..ec31f1a31
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L0-K9-E003-crlf.k9.ncl
@@ -0,0 +1,19 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §3.3: CRLF line endings. K9 is LF-only; a CR inside
+# the magic line makes it four octets, so a reader that compares bytes and a
+# reader that trims whitespace would disagree about what this file is.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "crlf",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "crlf" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-E004-no-spdx.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-E004-no-spdx.k9.ncl
new file mode 100644
index 000000000..302298391
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L0-K9-E004-no-spdx.k9.ncl
@@ -0,0 +1,18 @@
+K9!
+# Negative control §3.2: no SPDX-License-Identifier in the first five lines.
+# The licence identifier is envelope metadata, so this is an L0 defect, not a
+# style note: an unlicensed component cannot be redistributed.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "no-licence",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "no-licence" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-E005-unclaimed-body.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-E005-unclaimed-body.k9.ncl
new file mode 100644
index 000000000..44478d97e
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L0-K9-E005-unclaimed-body.k9.ncl
@@ -0,0 +1,10 @@
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §4.4: a `.k9.ncl` suffix with neither a Nickel body nor the
+# coordination dialect's YAML body. This is the shape of the estate's twelve
+# session-management PROTOCOL.k9 stubs, which claim a K9 suffix and belong to
+# no K9 dialect. Reserving the suffix is what stops a reviewer (or `file`)
+# from believing a format promise the body does not keep.
+protocol:
+  family: "handover"
+  name: "unclaimed"
+  status: "stub"
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-S012-library-with-pedigree.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-S012-library-with-pedigree.ncl
new file mode 100644
index 000000000..b642c6944
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L0-K9-S012-library-with-pedigree.ncl
@@ -0,0 +1,22 @@
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §11.2: an execution licence in a file with no envelope.
+# A pedigree is a leash declaration, and the leash is detected from the
+# envelope. Without `K9!` on line 1 nothing downstream can tell this file is a
+# component at all, so the licence it grants is unenforceable — which is worse
+# than no licence, because a reviewer sees one.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "envelopeless-component",
+    security = {
+      leash = 'Hunt,
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = true,
+      capabilities = ["net.fetch", "fs.write", "process.spawn"],
+    },
+    metadata = { name = "envelopeless-component" },
+    side_effects = ["writes to the host filesystem"],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L0-K9-S014-stray-leash.ncl b/1-formats/k9/tools/fixtures/invalid/L0-K9-S014-stray-leash.ncl
new file mode 100644
index 000000000..4379e81d5
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L0-K9-S014-stray-leash.ncl
@@ -0,0 +1,13 @@
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §11.3: a leash claim outside pedigree.security.
+# This is the shape of 2-protocols/axel/config/*.k9.ncl. A top-level `leash`
+# is not a pedigree field, so no host applying the contract would ever read
+# it — the file declares a security level nothing enforces.
+{
+  leash = 'Kennel,
+
+  project = {
+    name = "stray-leash",
+    version = "0.1.0",
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S001-no-pedigree.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S001-no-pedigree.k9.ncl
new file mode 100644
index 000000000..9fad0f6c4
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S001-no-pedigree.k9.ncl
@@ -0,0 +1,9 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §6.1: a component with no pedigree. Without one there is no
+# leash, no capability grant and no identity — nothing for a host to enforce.
+{
+  config = {
+    target_dir = "/tmp/k9",
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S002-wrong-major.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S002-wrong-major.k9.ncl
new file mode 100644
index 000000000..1352929a7
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S002-wrong-major.k9.ncl
@@ -0,0 +1,19 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §5.4: a component from a different schema major. It is not
+# "older" or "newer", it is unreadable: a v1 reader that guesses at a v2 field
+# layout produces a confident wrong answer about a security posture.
+{
+  pedigree = {
+    schema_version = "2.0.0",
+    component_type = "future-component",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "future-component" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S003-todo-component-type.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S003-todo-component-type.k9.ncl
new file mode 100644
index 000000000..bab378f93
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S003-todo-component-type.k9.ncl
@@ -0,0 +1,19 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §6.2: an unfilled component_type placeholder. This is the
+# exact state of .machine_readable/svc/k9/template-hunt.k9.ncl today: the field
+# exists, so a presence check passes, and the value says nothing.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "TODO: describe component type (e.g., 'deployment')",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "placeholder-type" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S004-unknown-leash.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S004-unknown-leash.k9.ncl
new file mode 100644
index 000000000..668700ab1
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S004-unknown-leash.k9.ncl
@@ -0,0 +1,19 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §7.1: a leash tag outside the closed set. The taxonomy is
+# closed on purpose — a fourth level whose meaning each host invents is exactly
+# how a "restricted" component ends up with full access on one implementation.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "unknown-leash",
+    security = {
+      leash = 'Paddock,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "unknown-leash" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S005-missing-name.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S005-missing-name.k9.ncl
new file mode 100644
index 000000000..bfc6dda50
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S005-missing-name.k9.ncl
@@ -0,0 +1,20 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §6.4: no metadata.name. A receipt records what ran; an
+# anonymous component produces a receipt that attributes nothing.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "anonymous",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = {
+      version = "1.0.0",
+    },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S006-unknown-capability.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S006-unknown-capability.k9.ncl
new file mode 100644
index 000000000..afead75c5
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S006-unknown-capability.k9.ncl
@@ -0,0 +1,23 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §8.1: a capability name that is neither core nor a
+# well-formed "x-<vendor>.<path>" extension. Reserving the namespace is what
+# stops a vendor name from being silently promoted into a core meaning later.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "bad-capability",
+    security = {
+      leash = 'Yard,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [
+        "fs.delete",
+        "x-acme",
+      ],
+    },
+    metadata = { name = "bad-capability" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S007-ungranted-flag.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S007-ungranted-flag.k9.ncl
new file mode 100644
index 000000000..70c0fd0c2
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S007-ungranted-flag.k9.ncl
@@ -0,0 +1,20 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §8.4: a security flag with nothing in the grant to pay for
+# it. Before #1058 this was accepted — the flags and the grant were two
+# unrelated opinions in the same block, so "default-deny" denied nothing.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "ungranted-flag",
+    security = {
+      leash = 'Yard,
+      allow_network = true,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = { name = "ungranted-flag" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S008-hunt-signature-not-required.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S008-hunt-signature-not-required.k9.ncl
new file mode 100644
index 000000000..b3f154281
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S008-hunt-signature-not-required.k9.ncl
@@ -0,0 +1,27 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §10.1: 'Hunt with signature_required = false.
+# A Hunt component that does not require a signature has declared full system
+# access and then declined the one control SPEC.adoc makes non-negotiable. The
+# signature block below is present, so presence is not the problem — the
+# pedigree says it is optional, and "optional" is how a gate gets skipped.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "hunt-optional-signature",
+    security = {
+      leash = 'Hunt,
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = false,
+      capabilities = ["net.fetch", "fs.write", "process.spawn"],
+    },
+    metadata = { name = "hunt-optional-signature" },
+    side_effects = ["spawns a child process"],
+    signature = {
+      algorithm = "Ed25519",
+      key_id = "fixture",
+    },
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S009-hunt-no-signature-block.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S009-hunt-no-signature-block.k9.ncl
new file mode 100644
index 000000000..aff0fcca5
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S009-hunt-no-signature-block.k9.ncl
@@ -0,0 +1,23 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §10.1: 'Hunt that requires a signature and carries none.
+# Note the limit of this check: it is PRESENCE. Passing it would prove only
+# that a signature block exists, never that the signature verifies. K9-C001 is
+# the check that could establish that, and it needs a verifier this validator
+# does not embed.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "hunt-unsigned",
+    security = {
+      leash = 'Hunt,
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = true,
+      capabilities = ["net.fetch", "fs.write", "process.spawn"],
+    },
+    metadata = { name = "hunt-unsigned" },
+    side_effects = ["spawns a child process"],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S010-hunt-empty-side-effects.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S010-hunt-empty-side-effects.k9.ncl
new file mode 100644
index 000000000..7ee3624aa
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S010-hunt-empty-side-effects.k9.ncl
@@ -0,0 +1,26 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §6.5: 'Hunt with an empty side_effects list.
+# A component claiming network, filesystem and subprocess access while
+# describing none of it gives the dry-run reviewer nothing to review, which
+# makes the `dry_run` precondition (§9) impossible to discharge honestly.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "hunt-undocumented",
+    security = {
+      leash = 'Hunt,
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = true,
+      capabilities = ["net.fetch", "fs.write", "process.spawn"],
+    },
+    metadata = { name = "hunt-undocumented" },
+    side_effects = [],
+    signature = {
+      algorithm = "Ed25519",
+      key_id = "fixture",
+    },
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl
new file mode 100644
index 000000000..0dc6fb025
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl
@@ -0,0 +1,28 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §6.7: a `recipes` block at 'Yard.
+# 'Yard permits Nickel evaluation and nothing else. A recipes block is a list
+# of shell commands, so declaring one at 'Yard asks for the leash to be
+# believed rather than checked — the exact inversion the leash exists to stop.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "sneaky-recipes",
+    security = {
+      leash = 'Yard,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = { name = "sneaky-recipes" },
+    side_effects = [],
+  },
+
+  recipes = {
+    default = { recipe = "run" },
+    run = {
+      commands = ["echo 'this should never be reachable at Yard'"],
+    },
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S013-dangling-import.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S013-dangling-import.k9.ncl
new file mode 100644
index 000000000..fd4fb7e00
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S013-dangling-import.k9.ncl
@@ -0,0 +1,24 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §11.4: an import that does not resolve.
+# The pedigree is built by merging the imported file, so a dangling import
+# means the pedigree a reviewer read is not the pedigree a host would evaluate.
+# This is the live state of all six .machine_readable/contractiles/*/*.k9.ncl
+# files, which import "../k9/template-hunt.k9.ncl" — a path that does not exist.
+let base = import "does-not-exist.ncl" in
+
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "dangling-import",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = { name = "dangling-import" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L2-K9-N001-two-segment-version.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L2-K9-N001-two-segment-version.k9.ncl
new file mode 100644
index 000000000..a24f04d37
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L2-K9-N001-two-segment-version.k9.ncl
@@ -0,0 +1,26 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §5.2: a two-segment schema_version.
+#
+# "1.0" is the major this reader speaks, and every character in it is a digit
+# or a dot, so L1's bounded lexical screen accepts it — correctly, given what
+# L1 claims to establish. §5.2 requires a numeric dot-TRIPLE, and it is the
+# contract's `is_semver_of` that counts the segments.
+#
+# Read this fixture together with L2-K9-N001-wrong-field-type: between them
+# they show that L1 is a screen and L2 is the decision.
+{
+  pedigree = {
+    schema_version = "1.0",
+    component_type = "short-version",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = { name = "short-version" },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/invalid/L2-K9-N001-wrong-field-type.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L2-K9-N001-wrong-field-type.k9.ncl
new file mode 100644
index 000000000..f1bc9a790
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/invalid/L2-K9-N001-wrong-field-type.k9.ncl
@@ -0,0 +1,30 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# Negative control §12.2: a defect only L2 can see.
+#
+# Every lexical check passes on this file. `allow_network` is spelled correctly,
+# sits at the right path, and carries a value — the value is just a String
+# where the contract requires a Bool. L1 compares it against the literal
+# "true", finds no match, and moves on; it has no notion of a type.
+#
+# This fixture is the argument for the layering: a validator that stopped at L1
+# would report this component as conforming, and a host would then have to
+# decide for itself what "yes" means.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "wrong-field-type",
+    security = {
+      leash = 'Kennel,
+      allow_network = "yes",
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = {
+      name = "wrong-field-type",
+      version = "1.0.0",
+    },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/valid/extension-capability.k9.ncl b/1-formats/k9/tools/fixtures/valid/extension-capability.k9.ncl
new file mode 100644
index 000000000..c2e3f58a1
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/valid/extension-capability.k9.ncl
@@ -0,0 +1,28 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# extension-capability.k9.ncl — positive control: the reserved namespace.
+# Rule coverage: §8.1 — a non-core capability MUST be "x-<vendor>.<path>" so
+# it can never collide with a future core name.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "accelerator-job",
+    security = {
+      leash = 'Yard,
+      trust_level = "contract-eval-only",
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [
+        "x-acme.gpu.alloc",
+        "x-acme.gpu.release",
+      ],
+    },
+    metadata = {
+      name = "extension-capability",
+      version = "0.3.0",
+      description = "Grants vendor-extension capabilities only.",
+    },
+    side_effects = [],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl b/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl
new file mode 100644
index 000000000..b48d1b21c
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl
@@ -0,0 +1,65 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# hunt-fully-granted.k9.ncl — positive control: a conforming Hunt component.
+#
+# Every §8.4-derived capability is granted, §10.1's signature block is
+# PRESENT, and side_effects are declared. Note what this file still does NOT
+# prove: the signature block below is a claim. K9-C001 will report it
+# 'Present_Unverified unless a verifier runs, and 'Present_Unverified does not
+# authorise Hunt. Conformance and authorisation are different questions.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "deployment",
+    security = {
+      leash = 'Hunt,
+      trust_level = "controlled-execution",
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      signature_required = true,
+      capabilities = [
+        "net.fetch",
+        "fs.write",
+        "process.spawn",
+        "deploy.apply",
+        "rollback.apply",
+      ],
+    },
+    metadata = {
+      name = "hunt-fully-granted",
+      version = "1.0.0",
+      description = "Reference Hunt component: every request is paid for in the grant.",
+      author = "K9 conformance suite",
+    },
+    warnings = [
+      "This component has network, filesystem and subprocess access.",
+      "A signature block being present is not a signature being verified.",
+      "Use dry-run first: ./must --dry-run run hunt-fully-granted.k9.ncl",
+    ],
+    side_effects = [
+      "writes the deployment tree under /srv/k9-conformance",
+      "spawns `just deploy` as a child process",
+      "fetches the release manifest from releases.example.org",
+    ],
+    signature = {
+      algorithm = "Ed25519",
+      key_id = "conformance-fixture",
+      payload_hash = "sha256:0000000000000000000000000000000000000000000000000000000000000000",
+      signature = "FIXTURE-NOT-A-REAL-SIGNATURE",
+    },
+  },
+
+  config = {
+    target_dir | String = "/srv/k9-conformance",
+    dry_run | Bool = true,
+  },
+
+  recipes = {
+    default = { recipe = "deploy" },
+    deploy = {
+      description = "Apply the deployment.",
+      commands = ["echo '[fixture] would deploy to %{config.target_dir}'"],
+    },
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/valid/kennel-data.k9.ncl b/1-formats/k9/tools/fixtures/valid/kennel-data.k9.ncl
new file mode 100644
index 000000000..615d84e7d
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/valid/kennel-data.k9.ncl
@@ -0,0 +1,30 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# kennel-data.k9.ncl — positive control: a data-only component.
+# Rule coverage: the smallest conforming component. No flags, so §8.4 derives
+# no capability requirement and the empty grant is correct rather than thin.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "project-metadata",
+    security = {
+      leash = 'Kennel,
+      trust_level = "data-only",
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = {
+      name = "kennel-data",
+      version = "1.0.0",
+      description = "Data-only K9 component: parsed and displayed, never evaluated.",
+    },
+    side_effects = [],
+  },
+
+  config = {
+    project = "k9-conformance",
+    languages = ["Nickel", "Bash"],
+  },
+}
diff --git a/1-formats/k9/tools/fixtures/valid/library-base.ncl b/1-formats/k9/tools/fixtures/valid/library-base.ncl
new file mode 100644
index 000000000..6ec33ca8f
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/valid/library-base.ncl
@@ -0,0 +1,17 @@
+# SPDX-License-Identifier: MPL-2.0
+# library-base.ncl — positive control: the library dialect (§11).
+#
+# No `K9!` envelope, no pedigree, no leash claim. This file is imported; it is
+# never executed as a component. That is the whole contract a library has to
+# satisfy, and it is a negative one: an execution licence in a file with no
+# envelope would be unenforceable, because nothing downstream could see it.
+{
+  shared_metadata = {
+    maintainer = "K9 conformance suite",
+    licence = "MPL-2.0",
+  },
+
+  default_warnings = [
+    "Imported from library-base.ncl; this file carries no execution licence.",
+  ],
+}
diff --git a/1-formats/k9/tools/fixtures/valid/yard-typed-config.k9.ncl b/1-formats/k9/tools/fixtures/valid/yard-typed-config.k9.ncl
new file mode 100644
index 000000000..cb466b601
--- /dev/null
+++ b/1-formats/k9/tools/fixtures/valid/yard-typed-config.k9.ncl
@@ -0,0 +1,37 @@
+K9!
+# SPDX-License-Identifier: MPL-2.0
+# yard-typed-config.k9.ncl — positive control: contract evaluation, no I/O.
+# Rule coverage: 'Yard permits Nickel evaluation, so a `validation` block is
+# allowed; it is not an execution surface, so K9-S011 does not fire.
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "typed-configuration",
+    security = {
+      leash = 'Yard,
+      trust_level = "contract-eval-only",
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+      capabilities = [],
+    },
+    metadata = {
+      name = "yard-typed-config",
+      version = "1.2.0",
+      description = "Typed configuration validated by Nickel contracts.",
+    },
+    warnings = [
+      "This component is evaluated; it does not execute.",
+    ],
+    side_effects = [],
+  },
+
+  config = {
+    port | Number = 8080,
+    host | String = "localhost",
+  },
+
+  validation = {
+    port_in_range = config.port > 0 && config.port < 65536,
+  },
+}
diff --git a/1-formats/k9/tools/k9-validate.sh b/1-formats/k9/tools/k9-validate.sh
new file mode 100755
index 000000000..2bfa86884
--- /dev/null
+++ b/1-formats/k9/tools/k9-validate.sh
@@ -0,0 +1,1013 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# k9-validate.sh — the CANONICAL K9 conformance validator.
+#
+# Implements 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc v1.0.0 against the
+# normative contract 1-formats/k9/spec/contract/k9_contract.ncl.
+#
+# ── WHY THIS IS LAYERED ─────────────────────────────────────────────────
+#
+# Four layers, each with a different authority. Collapsing them is how a
+# lexical check quietly becomes an execution licence, which is the failure
+# mode §12 of the spec exists to prevent.
+#
+#   L0  ENVELOPE      bytes only. Magic, encoding, line endings, SPDX, and the
+#                     dialect discriminator. Always runnable: no toolchain.
+#   L1  STRUCTURAL    a bounded lexical scan of the Nickel body for the fields
+#                     the contract requires. Always runnable. PROVISIONAL:
+#                     it is a screen, not a decision procedure, and §12.3
+#                     forbids reporting conformance on L1 alone.
+#   L2  SEMANTIC      the real thing — `nickel typecheck` of the envelope-
+#                     stripped body against k9_contract.ncl. Needs `nickel`.
+#   L3  CRYPTOGRAPHIC Ed25519 verification of the signature block. Needs an
+#                     external verifier this script deliberately does not
+#                     embed. Absent one, it reports 'Not_Run and says so.
+#
+# A check that could not run is reported as SKIPPED, never as a pass. With
+# --strict, a SKIP fails the run. That is the defence against the estate's
+# recurring "gate that could never fire" defect (standards#49, #64): a
+# validator with no toolchain must not be able to report green.
+#
+# ── RULE IDS ────────────────────────────────────────────────────────────
+# Every finding carries a stable id (K9-E*, K9-S*, K9-N*, K9-C*) so a fixture
+# can name the rule it violates and a migration can name the rule it clears.
+#
+# ── USAGE ───────────────────────────────────────────────────────────────
+#   k9-validate.sh [OPTIONS] FILE...
+#   k9-validate.sh --fixtures DIR     valid/ must pass, invalid/ must fail
+#   k9-validate.sh --self-test        built-in assertions, no fixtures needed
+#
+# OPTIONS
+#   --layer L0|L1|L2|L3|all   run up to this layer (default: all)
+#   --strict                  a SKIPPED check fails the run (exit 3)
+#   --json                    one JSON object per file on stdout
+#   --nickel PATH             the nickel binary (default: $K9_NICKEL or PATH)
+#   --no-route                do not route out-of-scope dialects; report them
+#   -q, --quiet               findings only
+#
+# EXIT  0 conforming · 1 violation · 2 usage error · 3 skipped under --strict
+set -uo pipefail
+
+SCRIPT_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)"
+SPEC_DIR="$(cd -- "$SCRIPT_DIR/../spec" && pwd)"
+CONTRACT="$SPEC_DIR/contract/k9_contract.ncl"
+
+CONTRACT_VERSION="1.0.0"
+SCHEMA_MAJOR="1"
+
+# §7 — the closed leash set. Mirrors k9_contract.ncl `leash_levels`; the
+# --self-test mode asserts the two agree, so the mirror cannot drift.
+# Values are carried TAGGED ('Kennel) because that is how they are written in
+# a pedigree, and the comparison is against what the file says.
+LEASH_LEVELS="'Kennel 'Yard 'Hunt"
+
+# §8.1 — the closed core capability set. Mirrors `core_capabilities`.
+CORE_CAPABILITIES="fs.read fs.write net.fetch process.spawn container.run secret.read deploy.apply rollback.apply"
+EXTENSION_PREFIX="x-"
+
+LAYER="all"
+STRICT=0
+JSON=0
+QUIET=0
+ROUTE=1
+NICKEL="${K9_NICKEL:-}"
+FIXTURES=""
+SELFTEST=0
+
+usage() { sed -n '2,44p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'; }
+
+while [ $# -gt 0 ]; do
+  case "$1" in
+    --layer) LAYER="${2:?--layer needs L0|L1|L2|L3|all}"; shift 2 ;;
+    --strict) STRICT=1; shift ;;
+    --json) JSON=1; shift ;;
+    --nickel) NICKEL="${2:?--nickel needs a path}"; shift 2 ;;
+    --no-route) ROUTE=0; shift ;;
+    --fixtures) FIXTURES="${2:?--fixtures needs a directory}"; shift 2 ;;
+    --self-test) SELFTEST=1; shift ;;
+    -q|--quiet) QUIET=1; shift ;;
+    -h|--help) usage; exit 0 ;;
+    --) shift; break ;;
+    -*) echo "k9-validate: unknown option: $1" >&2; usage >&2; exit 2 ;;
+    *) break ;;
+  esac
+done
+
+case "$LAYER" in
+  L0|L1|L2|L3|all) : ;;
+  *) echo "k9-validate: --layer must be L0, L1, L2, L3 or all" >&2; exit 2 ;;
+esac
+
+layer_reached() {
+  case "$LAYER" in
+    all|L3) return 0 ;;
+    L2) [ "$1" != "L3" ] ;;
+    L1) [ "$1" = "L0" ] || [ "$1" = "L1" ] ;;
+    L0) [ "$1" = "L0" ] ;;
+  esac
+}
+
+RED='\033[0;31m'; GRN='\033[0;32m'; YEL='\033[1;33m'; BLU='\033[0;34m'; NC='\033[0m'
+[ -t 1 ] || { RED=''; GRN=''; YEL=''; BLU=''; NC=''; }
+
+note() { [ "$QUIET" -eq 1 ] || [ "$JSON" -eq 1 ] || echo -e "${BLU}[k9]${NC} $*"; }
+
+# ── per-file state ───────────────────────────────────────────────────────
+F=""
+DIALECT=""
+HAS_MAGIC=0
+ERRORS=0
+WARNINGS=0
+SKIPS=0
+FINDINGS=()
+
+err()  { FINDINGS+=("error|$1|$2|$3");   ERRORS=$((ERRORS + 1)); }
+warn() { FINDINGS+=("warning|$1|$2|$3"); WARNINGS=$((WARNINGS + 1)); }
+skip() { FINDINGS+=("skipped|$1|$2|$3"); SKIPS=$((SKIPS + 1)); }
+
+emit_findings() {
+  local f sev rule lay msg
+  for f in ${FINDINGS+"${FINDINGS[@]}"}; do
+    [ -z "$f" ] && continue
+    IFS='|' read -r sev rule lay msg <<< "$f"
+    case "$sev" in
+      error)   echo -e "${RED}ERROR${NC}   $rule [$lay] $F: $msg" >&2 ;;
+      warning) echo -e "${YEL}WARN${NC}    $rule [$lay] $F: $msg" >&2 ;;
+      skipped) echo -e "${YEL}SKIPPED${NC} $rule [$lay] $F: $msg" >&2 ;;
+    esac
+  done
+}
+
+emit_json() {
+  local verdict="$1" f first=1 sev rule lay msg
+  printf '{"file":"%s","dialect":"%s","contract_version":"%s","verdict":"%s","errors":%d,"warnings":%d,"skipped":%d,"findings":[' \
+    "$F" "$DIALECT" "$CONTRACT_VERSION" "$verdict" "$ERRORS" "$WARNINGS" "$SKIPS"
+  for f in ${FINDINGS+"${FINDINGS[@]}"}; do
+    [ -z "$f" ] && continue
+    IFS='|' read -r sev rule lay msg <<< "$f"
+    [ $first -eq 0 ] && printf ','
+    first=0
+    printf '{"severity":"%s","rule":"%s","layer":"%s","message":"%s"}' \
+      "$sev" "$rule" "$lay" \
+      "$(printf '%s' "$msg" | sed 's/\\/\\\\/g; s/"/\\"/g')"
+  done
+  printf ']}\n'
+}
+
+# ── the structural extractor ─────────────────────────────────────────────
+#
+# A bounded lexical scan emitting `FACT <path> <value>` and
+# `ARRAY <path> <item>` triples for the Nickel body. It tracks brace/bracket
+# depth to build a dotted path, which is what lets it tell
+# `pedigree.security.leash` apart from a stray top-level `leash`.
+#
+# KNOWN LIMITATIONS, all deliberate and all of them the reason L1 is
+# provisional rather than authoritative (§12.3):
+#   * comments are stripped from the first `#`, so a `#` inside a string is
+#     mis-handled;
+#   * `m%" ... "%` multiline strings are skipped wholesale, so a key inside
+#     one is not reported;
+#   * a key and its `{` on separate lines are not joined.
+# None of these can turn a non-conforming file into a PASS at L2, because L2
+# re-derives every one of these facts from Nickel itself.
+extract_facts() {
+  awk '
+    function trim(s) { sub(/^[ \t]+/, "", s); sub(/[ \t]+$/, "", s); return s }
+    function path(   i, p) { p = ""; for (i = 1; i <= depth; i++) p = p (i > 1 ? "." : "") stk[i]; return p }
+    BEGIN { depth = 0; in_ml = 0 }
+    {
+      line = $0
+      if (in_ml) { if (line ~ /"%/) in_ml = 0; next }
+      if (line ~ /m%"/ && line !~ /"%/) { in_ml = 1; next }
+
+      sub(/[ \t]*#.*$/, "", line)
+      line = trim(line)
+      if (line == "") next
+
+      if (line ~ /^[\}\]][,;]?$/) { if (depth > 0) depth--; next }
+
+      if (match(line, /^[A-Za-z_][A-Za-z0-9_."-]*[ \t]*=/)) {
+        eq = index(line, "=")
+        key = trim(substr(line, 1, eq - 1))
+        gsub(/^"|"$/, "", key)
+        val = trim(substr(line, eq + 1))
+        sub(/[,;]$/, "", val)
+        p = path()
+        full = (p == "" ? key : p "." key)
+
+        if (val ~ /\{$/)      { print "FACT\t" full "\t{"; stk[++depth] = key; next }
+        if (val ~ /\[$/)      { print "FACT\t" full "\t["; stk[++depth] = key; next }
+
+        # Single-line record: `metadata = { name = "x" }`. Split the inner
+        # text on commas and emit one FACT per pair. A nested record inside a
+        # one-liner would be mis-split; that is a documented L1 limitation.
+        if (val ~ /^\{.*\}$/) {
+          inner = substr(val, 2, length(val) - 2)
+          m = split(inner, parts, ",")
+          for (i = 1; i <= m; i++) {
+            kv = trim(parts[i])
+            e2 = index(kv, "=")
+            if (kv == "" || e2 == 0) continue
+            k2 = trim(substr(kv, 1, e2 - 1)); gsub(/^"|"$/, "", k2)
+            print "FACT\t" full "." k2 "\t" trim(substr(kv, e2 + 1))
+          }
+          next
+        }
+
+        # Single-line array: `capabilities = ["a", "b"]` or `side_effects = []`.
+        if (val ~ /^\[.*\]$/) {
+          inner = substr(val, 2, length(val) - 2)
+          m = split(inner, parts, ",")
+          for (i = 1; i <= m; i++) {
+            it = trim(parts[i])
+            if (it != "") print "ARRAY\t" full "\t" it
+          }
+          next
+        }
+
+        print "FACT\t" full "\t" val
+        next
+      }
+
+      if (depth > 0) {
+        item = line
+        sub(/[,;]$/, "", item)
+        item = trim(item)
+        if (item != "") print "ARRAY\t" path() "\t" item
+      }
+    }
+  ' "$1"
+}
+
+# fact_get returns the value with any trailing comma already removed, so
+# callers compare against `true` rather than `true,`.
+fact_get() { awk -F'\t' -v want="$2" '$1 == "FACT" && $2 == want { print $3; exit }' "$1"; }
+fact_paths() { awk -F'\t' '$1 == "FACT" { print $2 }' "$1"; }
+array_items() { awk -F'\t' -v want="$2" '$1 == "ARRAY" && $2 == want { print $3 }' "$1"; }
+
+unquote() { local s="$1"; s="${s#\"}"; s="${s%\"}"; printf '%s' "$s"; }
+is_todo() { case "$1" in *TODO*|*FIXME*|*XXX*) return 0 ;; esac; return 1; }
+
+# ════════════════════════════════════════════════════════════════════════
+# L0 — ENVELOPE
+# ════════════════════════════════════════════════════════════════════════
+check_l0() {
+  local f="$1" first head5 body_start
+
+  # K9-E002 — a component is text. A NUL byte means this is not a K9 file.
+  if ! LC_ALL=C tr -d '\000' < "$f" | cmp -s - "$f"; then
+    err K9-E002 L0 "file contains a NUL byte; not a text K9 component"
+    return 1
+  fi
+
+  # K9-E003 — LF only. CRLF changes the magic line's bytes as seen by a
+  # strict reader, and .gitattributes already mandates eol=repo-wide.
+  if LC_ALL=C grep -qU $'\r' "$f"; then
+    err K9-E003 L0 "file contains CR; K9 files are LF-only"
+  fi
+
+  # K9-E001 — the magic line. §3.1: exactly the three octets 0x4B 0x39 0x21
+  # and nothing else on the line. `K9`, `k9!` and `K9! ` are all rejected: a
+  # magic number with a tolerance is not a magic number.
+  first="$(head -n 1 "$f")"
+  if [ "$first" = 'K9!' ]; then
+    HAS_MAGIC=1
+  else
+    HAS_MAGIC=0
+    if printf '%s' "$first" | grep -qE '^[Kk]9!?[[:space:]]*$'; then
+      err K9-E001 L0 "line 1 is '$first', not exactly 'K9!'"
+    fi
+  fi
+
+  # K9-E004 — SPDX within the first five lines. Envelope metadata, so an L0
+  # concern, and an ERROR: the estate licence gate treats a missing
+  # identifier as a defect, not a nicety.
+  head5="$(head -n 5 "$f")"
+  if ! printf '%s\n' "$head5" | grep -q '^#[[:space:]]*SPDX-License-Identifier:'; then
+    err K9-E004 L0 "no SPDX-License-Identifier in the first 5 lines"
+  fi
+
+  # K9-E005 — the dialect discriminator (§4.3). After the magic line and the
+  # comment header, the first significant line decides the dialect. `---` is
+  # the coordination dialect's document marker; `{`, `[`, `(`, `let`, a string,
+  # or a top-level `ident =` binding is a Nickel term; a bare `key:` line with
+  # no `=` is YAML that belongs to no K9 dialect at all.
+  if [ "$HAS_MAGIC" -eq 1 ]; then
+    body_start="$(sed -n '2,$p' "$f" | grep -vE '^[[:space:]]*#' | grep -vE '^[[:space:]]*$' | head -n 1)"
+  else
+    body_start="$(grep -vE '^[[:space:]]*#' "$f" | grep -vE '^[[:space:]]*$' | head -n 1)"
+  fi
+
+  if printf '%s' "$body_start" | grep -qE '^-{3}'; then
+    DIALECT="coordination"
+  elif printf '%s' "$body_start" | grep -qE '^(\{|\[|\(|let[[:space:]]|")'; then
+    if [ "$HAS_MAGIC" -eq 1 ]; then DIALECT="component"; else DIALECT="library"; fi
+  elif printf '%s' "$body_start" | grep -qE '^[A-Za-z_][A-Za-z0-9_."-]*[[:space:]]*='; then
+    # A Nickel binding. Note that a Nickel FILE must still be a single term,
+    # so a top-level binding sequence is a defect — but it is a Nickel defect
+    # and belongs at L1/L2, not to a dialect mismatch.
+    if [ "$HAS_MAGIC" -eq 1 ]; then DIALECT="component"; else DIALECT="library"; fi
+  elif printf '%s' "$body_start" | grep -qE '^[A-Za-z_][A-Za-z0-9_.-]*:'; then
+    # A `key:` line: the coordination dialect permits one, and so do the
+    # unclaimed session-management PROTOCOL.k9 stubs. Only the magic line
+    # separates the two, so with no magic this file claims nothing.
+    if [ "$HAS_MAGIC" -eq 1 ]; then DIALECT="coordination"; else DIALECT="unclaimed"; fi
+  else
+    DIALECT="unclaimed"
+  fi
+
+  if [ "$DIALECT" = "unclaimed" ]; then
+    if [ "$ROUTE" -eq 1 ]; then
+      err K9-E005 L0 "suffix claims K9 but the body is neither a Nickel term nor the coordination dialect (first significant line: '${body_start:-<empty>}')"
+    else
+      err K9-E005 L0 "suffix claims K9 but the body is neither a Nickel term nor the coordination dialect"
+    fi
+    return 1
+  fi
+
+  if [ "$DIALECT" = "coordination" ]; then
+    note "$f: dialect k9-coordination — governed by coordination-k9-grammar_v1.1.abnf, out of scope here"
+    return 2
+  fi
+
+  # K9-S012 / K9-S014 — the envelope/role rule, checked at L0 because it IS
+  # about the envelope. §11.2: an execution licence in a file with no magic is
+  # unenforceable, because nothing downstream can detect it.
+  if [ "$DIALECT" = "library" ]; then
+    if grep -qE '^[[:space:]]{0,2}pedigree[[:space:]]*=' "$f"; then
+      err K9-S012 L0 "no 'K9!' envelope but a top-level pedigree: a component without an envelope cannot be leashed"
+    fi
+    if grep -qE '^[[:space:]]{0,2}leash[[:space:]]*=' "$f"; then
+      err K9-S014 L0 "no 'K9!' envelope but a top-level leash claim; a leash belongs in pedigree.security"
+    fi
+  fi
+  return 0
+}
+
+# ════════════════════════════════════════════════════════════════════════
+# L1 — STRUCTURAL (lexical, PROVISIONAL)
+# ════════════════════════════════════════════════════════════════════════
+check_l1() {
+  local f="$1" facts sv ct leash name lvl cap req deficit side n sig_req
+  facts="$(mktemp)"
+  extract_facts "$f" > "$facts"
+
+  if [ "$DIALECT" = "library" ]; then
+    # §11 — a library has no pedigree to check. Its obligations are the
+    # negative one already enforced at L0, plus resolvable imports.
+    check_imports "$f"
+    rm -f "$facts"
+    return 0
+  fi
+
+  # K9-S001 — a component declares a pedigree.
+  if [ -z "$(fact_get "$facts" pedigree)" ]; then
+    err K9-S001 L1 "no top-level 'pedigree' block"
+    rm -f "$facts"
+    return 0
+  fi
+
+  # K9-S002 — schema_version, and its major must match this contract's.
+  sv="$(unquote "$(fact_get "$facts" pedigree.schema_version)")"
+  if [ -z "$sv" ]; then
+    err K9-S002 L1 "pedigree.schema_version is missing"
+  else
+    case "$sv" in
+      "$SCHEMA_MAJOR".*)
+        case "$sv" in
+          *[!0-9.]*) err K9-S002 L1 "pedigree.schema_version '$sv' is not a numeric dot-triple" ;;
+          *) : ;;
+        esac ;;
+      *) err K9-S002 L1 "pedigree.schema_version '$sv' is not readable by contract v$CONTRACT_VERSION (needs major $SCHEMA_MAJOR)" ;;
+    esac
+  fi
+
+  # K9-S003 — component_type is required and must not be a placeholder.
+  ct="$(unquote "$(fact_get "$facts" pedigree.component_type)")"
+  if [ -z "$ct" ]; then
+    err K9-S003 L1 "pedigree.component_type is missing (required by contract v$CONTRACT_VERSION §6.2)"
+  elif is_todo "$ct"; then
+    err K9-S003 L1 "pedigree.component_type is an unfilled placeholder: '$ct'"
+  fi
+
+  # K9-S004 — the leash tag must be in the closed set. Compared TAGGED, so
+  # the message quotes exactly what the file says.
+  leash="$(fact_get "$facts" pedigree.security.leash)"
+  if [ -z "$leash" ]; then
+    err K9-S004 L1 "pedigree.security.leash is missing"
+  else
+    lvl=0
+    for l in $LEASH_LEVELS; do [ "$l" = "$leash" ] && lvl=1; done
+    [ $lvl -eq 0 ] && err K9-S004 L1 "leash '$leash' is not in the closed set {$LEASH_LEVELS}"
+  fi
+
+  # K9-S014 — a leash claim outside pedigree.security. Same rule as the L0
+  # library check, but reachable from a component too: a file may carry the
+  # envelope and still declare its level somewhere no host reads. This is the
+  # live shape of rhodium-standard-repositories/rsr-compliance-checklist.k9.ncl.
+  if [ -n "$(fact_get "$facts" leash)" ]; then
+    err K9-S014 L1 "top-level 'leash = $(fact_get "$facts" leash)' outside pedigree.security; a leash declared there is read by nothing"
+  fi
+
+  # K9-S005 — metadata.name.
+  name="$(unquote "$(fact_get "$facts" pedigree.metadata.name)")"
+  if [ -z "$name" ]; then
+    err K9-S005 L1 "pedigree.metadata.name is missing"
+  elif is_todo "$name"; then
+    err K9-S005 L1 "pedigree.metadata.name is an unfilled placeholder: '$name'"
+  fi
+
+  # K9-S006 — every granted capability is a core name or an x- extension.
+  while IFS= read -r cap; do
+    [ -z "$cap" ] && continue
+    cap="$(unquote "$cap")"
+    if ! capability_ok "$cap"; then
+      err K9-S006 L1 "capability '$cap' is neither a core name nor an '${EXTENSION_PREFIX}<vendor>.<path>' extension"
+    fi
+  done < <(array_items "$facts" pedigree.security.capabilities)
+
+  # K9-S007 — the grant must cover what the security flags ask for.
+  req="$(required_capabilities "$facts")"
+  deficit=""
+  for r in $req; do
+    if ! array_items "$facts" pedigree.security.capabilities | grep -qxF "\"$r\""; then
+      deficit="$deficit $r"
+    fi
+  done
+  if [ -n "$deficit" ]; then
+    err K9-S007 L1 "security flags request capabilities the grant does not cover:$deficit (default-deny: list them in pedigree.security.capabilities)"
+  fi
+
+  # K9-S008 / K9-S009 / K9-S010 — the Hunt-specific obligations. None of
+  # these is relaxed relative to SPEC.adoc; K9-S007 and K9-S010 are new and
+  # both make Hunt harder to reach, not easier.
+  if [ "$leash" = "'Hunt" ]; then
+    sig_req="$(fact_get "$facts" pedigree.security.signature_required)"
+    if [ "$sig_req" != "true" ]; then
+      err K9-S008 L1 "leash is 'Hunt but pedigree.security.signature_required is not true"
+    fi
+    # PRESENCE ONLY. This proves the file carries a signature block. It says
+    # nothing about whether that signature verifies — that is K9-C001.
+    if [ -z "$(fact_get "$facts" pedigree.signature)" ]; then
+      err K9-S009 L1 "leash is 'Hunt but no pedigree.signature block is present (presence required here; verification is K9-C001)"
+    fi
+    n="$(array_items "$facts" pedigree.side_effects | grep -c . || true)"
+    if [ "${n:-0}" -eq 0 ]; then
+      err K9-S010 L1 "leash is 'Hunt but pedigree.side_effects is empty: full access must be described"
+    else
+      while IFS= read -r side; do
+        [ -z "$side" ] && continue
+        side="$(unquote "$side")"
+        if is_todo "$side"; then
+          err K9-S010 L1 "pedigree.side_effects contains an unfilled placeholder: $side"
+        fi
+      done < <(array_items "$facts" pedigree.side_effects)
+    fi
+  fi
+
+  # K9-S011 — a recipes block is an execution surface, so it forces 'Hunt.
+  if [ -n "$(fact_paths "$facts" | grep -E '^recipes(\.|$)' | head -n 1)" ] \
+    && [ "$leash" != "'Hunt" ]; then
+    err K9-S011 L1 "component declares a 'recipes' block at leash $leash; recipes are an execution surface and require 'Hunt"
+  fi
+
+  check_imports "$f"
+  rm -f "$facts"
+  return 0
+}
+
+capability_ok() {
+  local n="$1" c
+  for c in $CORE_CAPABILITIES; do [ "$c" = "$n" ] && return 0; done
+  case "$n" in
+    "$EXTENSION_PREFIX".*) return 1 ;;   # "x-.foo" has no vendor segment
+    "$EXTENSION_PREFIX"*.*) return 0 ;;
+  esac
+  return 1
+}
+
+# §8.4 — capabilities the security flags request. Mirrors
+# k9_contract.ncl `required_capabilities`; --self-test exercises both.
+required_capabilities() {
+  local facts="$1" out=""
+  [ "$(fact_get "$facts" pedigree.security.allow_network)" = "true" ] && out="$out net.fetch"
+  [ "$(fact_get "$facts" pedigree.security.allow_filesystem_write)" = "true" ] && out="$out fs.write"
+  [ "$(fact_get "$facts" pedigree.security.allow_subprocess)" = "true" ] && out="$out process.spawn"
+  printf '%s' "${out# }"
+}
+
+# §11.4 — every import must resolve. A dangling import is not a style
+# problem: the component's pedigree is built by merging the imported file, so
+# an unresolvable import means the pedigree a reviewer read is not the
+# pedigree a host would evaluate.
+check_imports() {
+  local f="$1" dir imp cand
+  dir="$(dirname "$f")"
+  while IFS= read -r imp; do
+    [ -z "$imp" ] && continue
+    cand="$dir/$imp"
+    if [ ! -f "$cand" ]; then
+      err K9-S013 L1 "import \"$imp\" does not resolve to $cand"
+    fi
+  done < <(sed 's/#.*//' "$f" | grep -oE 'import[[:space:]]+"[^"]+"' | sed -E 's/.*"([^"]+)".*/\1/')
+}
+
+# ════════════════════════════════════════════════════════════════════════
+# L2 — SEMANTIC (Nickel)
+# ════════════════════════════════════════════════════════════════════════
+nickel_bin() {
+  if [ -n "$NICKEL" ]; then
+    [ -x "$NICKEL" ] && { printf '%s' "$NICKEL"; return 0; }
+    return 1
+  fi
+  command -v nickel 2>/dev/null && return 0
+  return 1
+}
+
+# §3.6 — THE ENVELOPE-STRIP RULE.
+#
+# `K9!` on line 1 is not Nickel: this estate's own CI records that
+# `nickel typecheck` dies at 1:3 on the `!` (.github/workflows/ci-pipeline.yml,
+# `detect` step), which is why every `*.k9.ncl` here is excluded from Nickel
+# checking today. Stripping the magic line — replacing it with a Nickel
+# comment so line numbers do not move — is what makes the body checkable at
+# all. Nothing about the component's meaning changes: the magic is envelope,
+# and the envelope is not part of the term.
+strip_envelope() {
+  local f="$1" out="$2"
+  if [ "$(head -n 1 "$f")" = 'K9!' ]; then
+    { echo '# K9! (envelope magic, stripped for Nickel evaluation)'; tail -n +2 "$f"; } > "$out"
+  else
+    cat "$f" > "$out"
+  fi
+}
+
+check_l2() {
+  local f="$1" nb out body_tmp drv_tmp dir base
+  if ! nb="$(nickel_bin)"; then
+    skip K9-N001 L2 "nickel not available; Nickel semantics were NOT checked (a skip is not a pass)"
+    skip K9-N002 L2 "nickel not available; the normative contract itself was not typechecked"
+    return 0
+  fi
+
+  # K9-N002 — the contract must typecheck before it judges anything. A broken
+  # contract that rejects everything would otherwise look like a very strict
+  # validator rather than a broken one.
+  if ! out="$("$nb" typecheck "$CONTRACT" 2>&1)"; then
+    err K9-N002 L2 "the normative contract does not typecheck: $(printf '%s' "$out" | head -n 3 | tr '\n' ' ')"
+    return 0
+  fi
+
+  # The stripped body and its driver are written BESIDE the original so that
+  # the body's own relative `import`s still resolve. Both are removed on the
+  # way out; a crash leaves at most two dotfiles, which is why they are dotted.
+  dir="$(dirname "$f")"
+  base=".k9-validate.$$.${RANDOM}"
+  body_tmp="$dir/$base.body.ncl"
+  drv_tmp="$dir/$base.driver.ncl"
+  # shellcheck disable=SC2064
+  trap "rm -f '$body_tmp' '$drv_tmp'" RETURN
+
+  strip_envelope "$f" "$body_tmp"
+
+  if [ "$DIALECT" = "library" ]; then
+    if ! out="$("$nb" typecheck "$body_tmp" 2>&1)"; then
+      err K9-N001 L2 "library does not typecheck: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')"
+    fi
+  else
+    cat > "$drv_tmp" <<EOF
+let K9 = import "$CONTRACT" in
+let doc = import "./$(basename "$body_tmp")" in
+doc | K9.Component
+EOF
+    if ! out="$("$nb" typecheck "$drv_tmp" 2>&1)"; then
+      err K9-N001 L2 "component does not satisfy K9.Component: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')"
+    fi
+  fi
+  rm -f "$body_tmp" "$drv_tmp"
+  return 0
+}
+
+# ════════════════════════════════════════════════════════════════════════
+# L3 — CRYPTOGRAPHIC
+# ════════════════════════════════════════════════════════════════════════
+#
+# §10.5 — this validator does NOT verify signatures and must not pretend to.
+# Verifying an Ed25519 signature means trusting a key, and key trust is a host
+# policy decision, not a file-format rule. What this layer does instead is
+# state the consequence: with no verifier the verdict is 'Present_Unverified,
+# the Hunt `signature` precondition is FALSE, and Hunt is unauthorised.
+check_l3() {
+  local f="$1" facts
+  [ "$DIALECT" = "library" ] && return 0
+  facts="$(mktemp)"
+  extract_facts "$f" > "$facts"
+
+  if [ -n "$(fact_get "$facts" pedigree.signature)" ]; then
+    if [ -n "${K9_SIG_VERIFIER:-}" ] && [ -x "${K9_SIG_VERIFIER}" ]; then
+      if "$K9_SIG_VERIFIER" "$f" >/dev/null 2>&1; then
+        note "$f: signature verdict 'Verified (external verifier)"
+      else
+        err K9-C001 L3 "signature verdict 'Rejected by the external verifier"
+      fi
+    else
+      skip K9-C001 L3 "signature block present but no verifier ran (set K9_SIG_VERIFIER); verdict is 'Present_Unverified, which does NOT authorise 'Hunt"
+    fi
+  fi
+  rm -f "$facts"
+  return 0
+}
+
+# ════════════════════════════════════════════════════════════════════════
+validate_one() {
+  F="$1"; DIALECT=""; HAS_MAGIC=0
+  ERRORS=0; WARNINGS=0; SKIPS=0; FINDINGS=()
+
+  if [ ! -f "$F" ]; then
+    err K9-E000 L0 "no such file"
+    if [ "$JSON" -eq 1 ]; then emit_json "error"; else emit_findings; fi
+    return 1
+  fi
+
+  check_l0 "$F"
+  local rc=$?
+  if [ $rc -eq 2 ]; then
+    # Routed out of scope: examined, and handed to the spec that governs it.
+    # That is neither a pass nor a failure of THIS contract.
+    [ "$JSON" -eq 1 ] && emit_json "routed"
+    return 0
+  fi
+  if [ "$DIALECT" = "unclaimed" ]; then
+    if [ "$JSON" -eq 1 ]; then emit_json "error"; else emit_findings; fi
+    return 1
+  fi
+
+  layer_reached L1 && check_l1 "$F"
+  layer_reached L2 && check_l2 "$F"
+  layer_reached L3 && check_l3 "$F"
+
+  local verdict="pass"
+  [ "$ERRORS" -gt 0 ] && verdict="fail"
+  if [ "$JSON" -eq 1 ]; then
+    emit_json "$verdict"
+  else
+    emit_findings
+    if [ "$ERRORS" -eq 0 ] && [ "$QUIET" -eq 0 ]; then
+      echo -e "${GRN}OK${NC}      $F (dialect=$DIALECT, warnings=$WARNINGS, skipped=$SKIPS)"
+    fi
+  fi
+
+  [ "$ERRORS" -gt 0 ] && return 1
+  [ "$STRICT" -eq 1 ] && [ "$SKIPS" -gt 0 ] && return 3
+  return 0
+}
+
+# ════════════════════════════════════════════════════════════════════════
+# --self-test — assertions that do not depend on the fixture corpus
+# ════════════════════════════════════════════════════════════════════════
+SELFTEST_FAILS=0
+t() { # t <desc> <expected> <actual>
+  if [ "$2" = "$3" ]; then
+    echo -e "${GRN}ok${NC}   $1"
+  else
+    echo -e "${RED}FAIL${NC} $1: expected '$2', got '$3'"
+    SELFTEST_FAILS=$((SELFTEST_FAILS + 1))
+  fi
+}
+expect_ok()  { if "$@"; then t "$* accepted" ok ok; else t "$* accepted" ok no; fi; }
+expect_bad() { if "$@"; then t "$* rejected" no ok; else t "$* rejected" no no; fi; }
+
+self_test() {
+  local n tmp facts stripped
+
+  echo "== the bash mirrors cannot drift from the normative contract =="
+  n="$(grep -oE "leash_levels = \[[^]]*\]" "$CONTRACT" | grep -oE "'[A-Za-z]+" | tr '\n' ' ' | sed 's/ $//')"
+  t "leash_levels mirrors k9_contract.ncl" "$LEASH_LEVELS" "$n"
+  n="$(awk '/core_capabilities = \[/,/^  \]/' "$CONTRACT" | grep -oE '"[a-z]+\.[a-z]+"' | tr -d '"' | tr '\n' ' ' | sed 's/ $//')"
+  t "core_capabilities mirrors k9_contract.ncl" "$CORE_CAPABILITIES" "$n"
+  t "contract_version mirrors k9_contract.ncl" "$CONTRACT_VERSION" \
+    "$(grep -oE 'contract_version = "[^"]+"' "$CONTRACT" | sed 's/.*"\(.*\)"/\1/')"
+  t "schema_major mirrors k9_contract.ncl" "$SCHEMA_MAJOR" \
+    "$(grep -oE 'schema_major = "[^"]+"' "$CONTRACT" | sed 's/.*"\(.*\)"/\1/')"
+
+  echo "== capability arithmetic (§8) =="
+  expect_ok  capability_ok "fs.read"
+  expect_ok  capability_ok "rollback.apply"
+  expect_ok  capability_ok "x-acme.gpu.alloc"
+  expect_bad capability_ok "x-acme"
+  expect_bad capability_ok "x-.gpu"
+  expect_bad capability_ok "fs.delete"
+  expect_bad capability_ok ""
+
+  echo "== the extractor =="
+  tmp="$(mktemp --suffix=.k9.ncl)"
+  cat > "$tmp" <<'EOF'
+K9!
+# SPDX-License-Identifier: MPL-2.0
+{
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "self-test",
+    security = {
+      leash = 'Kennel,
+      allow_network = false,
+      allow_filesystem_write = false,
+      allow_subprocess = false,
+    },
+    metadata = { name = "self-test" },
+    side_effects = [],
+  },
+}
+EOF
+  facts="$(mktemp)"
+  extract_facts "$tmp" > "$facts"
+  t "extracts pedigree.security.leash" "'Kennel" "$(fact_get "$facts" pedigree.security.leash)"
+  t "extracts pedigree.component_type" '"self-test"' "$(fact_get "$facts" pedigree.component_type)"
+  t "extracts pedigree.metadata.name" '"self-test"' "$(fact_get "$facts" pedigree.metadata.name)"
+  t "pedigree leash is not reported as top-level leash" "" "$(fact_get "$facts" leash)"
+  t "required_capabilities for a quiet component" "" "$(required_capabilities "$facts")"
+
+  sed -i.bak 's/allow_network = false/allow_network = true/' "$tmp" && rm -f "$tmp.bak"
+  extract_facts "$tmp" > "$facts"
+  t "required_capabilities follows allow_network" "net.fetch" "$(required_capabilities "$facts")"
+
+  echo "== the envelope strip keeps line numbers (§3.6) =="
+  stripped="$(mktemp --suffix=.ncl)"
+  strip_envelope "$tmp" "$stripped"
+  t "line 1 becomes a comment" 1 "$(head -n 1 "$stripped" | grep -c '^#')"
+  t "line count is preserved" "$(wc -l < "$tmp" | tr -d ' ')" "$(wc -l < "$stripped" | tr -d ' ')"
+  t "schema_version stays on line 5" '    schema_version = "1.0.0",' "$(sed -n '5p' "$stripped")"
+  rm -f "$tmp" "$facts" "$stripped"
+
+  echo "== L3: signature presence is not verification (§10) =="
+  # No fixture can make a verifier appear, so the three verdicts a host can
+  # reach are asserted here with a stub verifier instead. What is under test is
+  # the code path, not the cryptography: this validator performs none.
+  local stub_ok stub_bad hunt out
+  stub_ok="$(mktemp)";  printf '#!/bin/sh\nexit 0\n' > "$stub_ok";  chmod +x "$stub_ok"
+  stub_bad="$(mktemp)"; printf '#!/bin/sh\nexit 1\n' > "$stub_bad"; chmod +x "$stub_bad"
+  hunt="$SCRIPT_DIR/fixtures/valid/hunt-fully-granted.k9.ncl"
+  if [ -f "$hunt" ]; then
+    QUIET=1
+    unset K9_SIG_VERIFIER
+    out="$(validate_one "$hunt" 2>&1 || true)"
+    t "no verifier -> K9-C001 is SKIPPED, never a pass" 1 \
+      "$(printf '%s' "$out" | grep -c 'SKIPPED K9-C001')"
+    t "the skip states presence does not authorise 'Hunt" 1 \
+      "$(printf '%s' "$out" | grep -c "does NOT authorise")"
+
+    K9_SIG_VERIFIER="$stub_ok"
+    out="$(validate_one "$hunt" 2>&1 || true)"
+    unset K9_SIG_VERIFIER
+    t "verifier accepts -> verdict 'Verified, no K9-C001 finding" 0 \
+      "$(printf '%s' "$out" | grep -c 'K9-C001')"
+
+    K9_SIG_VERIFIER="$stub_bad"
+    out="$(validate_one "$hunt" 2>&1 || true)"
+    unset K9_SIG_VERIFIER
+    t "verifier refuses -> K9-C001 error, verdict 'Rejected" 1 \
+      "$(printf '%s' "$out" | grep -c "K9-C001.*'Rejected")"
+    QUIET=0
+  else
+    echo -e "${YEL}SKIP${NC} L3 assertions: $hunt not present"
+  fi
+  rm -f "$stub_ok" "$stub_bad"
+
+  echo "== the fixture runner's attribution cannot be fooled by a filename =="
+  # This block exists because of a real failure. A negative control's filename
+  # contains its rule id, and attribution used to grep the human-readable
+  # finding line — which echoes the path. So `L2-K9-N001-*.k9.ncl` "proved"
+  # itself whenever ANY rule fired, including K9-N002 (the contract does not
+  # typecheck). Both L2 controls reported ok on a contract that judged nothing.
+  # The suite's whole purpose is catching gates that cannot fire, so the
+  # predicate is asserted here rather than trusted.
+  local impostor fired
+  impostor="$SCRIPT_DIR/fixtures/invalid/L0-K9-E001-bad-magic.k9.ncl"
+  if [ -f "$impostor" ]; then
+    QUIET=1
+    local sj="$JSON"; JSON=1
+    fired="$(validate_one "$impostor" 2>/dev/null \
+      | grep -oE '"severity":"error","rule":"K9-[A-Z][0-9]+","layer":"L[0-9]+"' \
+      | sed -E 's/.*"rule":"(K9-[A-Z][0-9]+)","layer":"(L[0-9])"/\1 \2/' \
+      | sort -u || true)"
+    JSON="$sj"; QUIET=0
+
+    # Every extracted pair must be well-formed, not merely "at least one": a
+    # silently unmatched finding would vanish from the set and a control could
+    # then fail to be attributed. (E001 fires twice — bad magic also leaves the
+    # body unclaimed — so the count is compared, not asserted to be 1.)
+    t "every extracted finding is well-formed rule+layer" \
+      "$(printf '%s\n' "$fired" | grep -c . || true)" \
+      "$(printf '%s\n' "$fired" | grep -cE '^[A-Z0-9-]+ L[0-9]$' || true)"
+    t "the rule that really fired is attributed" 1 \
+      "$(printf '%s\n' "$fired" | grep -cE '^K9-E001 L0$' || true)"
+    # The assertion that was missing: a rule id present in the PATH but absent
+    # from the findings must NOT satisfy the control.
+    t "a rule named only in the filename is NOT attributed" 0 \
+      "$(printf '%s\n' "$fired" | grep -cE '^K9-S004 L0$' || true)"
+    # Nor may a skip satisfy it: only severity "error" counts. hunt-fully-granted
+    # carries a signature block with no verifier, so K9-C001 is SKIPPED; if a
+    # skip could satisfy a control, a missing toolchain would pass a gate.
+    local hunt_json
+    hunt_json="$(QUIET=1 JSON=1 validate_one "$SCRIPT_DIR/fixtures/valid/hunt-fully-granted.k9.ncl" 2>/dev/null || true)"
+    t "K9-C001 is present as a skipped finding" 1 \
+      "$(printf '%s' "$hunt_json" | grep -cE '"severity":"skipped","rule":"K9-C001"' || true)"
+    t "and that same finding is NOT extractable as a rejection" 0 \
+      "$(printf '%s' "$hunt_json" \
+        | grep -oE '"severity":"error","rule":"K9-[A-Z][0-9]+","layer":"L[0-9]+"' \
+        | grep -c 'K9-C001' || true)"
+  else
+    echo -e "${YEL}SKIP${NC} attribution assertions: $impostor not present"
+  fi
+
+  echo
+  if [ $SELFTEST_FAILS -eq 0 ]; then
+    echo -e "${GRN}self-test: all assertions passed${NC}"
+    return 0
+  fi
+  echo -e "${RED}self-test: $SELFTEST_FAILS assertion(s) failed${NC}"
+  return 1
+}
+
+# ════════════════════════════════════════════════════════════════════════
+# --fixtures — positive AND negative controls
+# ════════════════════════════════════════════════════════════════════════
+#
+# The negative controls are the point. A validator that accepts everything
+# passes every positive fixture, so a suite of positives alone proves nothing;
+# it is the invalid/ corpus that shows the gate can fire. Each invalid fixture
+# is named `L<layer>-<rule>-<reason>.k9.ncl` so the runner asserts not only
+# that the file was rejected, but that it was rejected BY THE RULE IT NAMES.
+run_fixtures() {
+  local dir="$1" fails=0 f base want_layer want_rule rc out npos=0 nneg=0
+  local outer_strict="$STRICT"
+  [ -d "$dir/valid" ] || { echo "k9-validate: no valid/ under $dir" >&2; return 2; }
+  if [ ! -d "$dir/invalid" ]; then
+    echo "k9-validate: no invalid/ under $dir — a suite with no negative controls proves nothing" >&2
+    return 2
+  fi
+
+  # Fixture assertions are about CONFORMANCE VERDICTS, so a check that could
+  # not run must not be able to fail a fixture: --strict's job here is the
+  # end-of-run refusal below, not turning every positive control red because
+  # no nickel binary happens to be installed. Without this, --strict on a
+  # machine without Nickel reports "0 positive fixtures pass", which reads as
+  # a broken corpus when it is a missing toolchain.
+  STRICT=0
+
+  echo "== positive controls (must pass) =="
+  while IFS= read -r f; do
+    npos=$((npos + 1))
+    if out="$(validate_one "$f" 2>&1)"; then
+      echo -e "${GRN}ok${NC}   $(basename "$f")"
+    else
+      rc=$?
+      printf '%s\n' "$out" >&2
+      echo -e "${RED}FAIL${NC} $(basename "$f") should conform (exit $rc)"
+      fails=$((fails + 1))
+    fi
+  done < <(find "$dir/valid" -type f \( -name '*.k9.ncl' -o -name '*.k9' -o -name '*.ncl' \) | sort)
+  if [ $npos -eq 0 ]; then
+    echo -e "${RED}FAIL${NC} no positive fixtures found"; fails=$((fails + 1))
+  fi
+
+  echo
+  echo "== negative controls (must fail, by the named rule) =="
+  local nskipped=0
+  while IFS= read -r f; do
+    nneg=$((nneg + 1))
+    base="$(basename "$f")"
+    want_layer="${base%%-*}"
+    want_rule="$(printf '%s' "${base#*-}" | grep -oE '^K9-[ESNC][0-9]+' || true)"
+
+    # An L2-named fixture is rejected by Nickel and by nothing else — that is
+    # the entire point of it. Without a nickel binary the runner cannot assert
+    # that, and reporting FAIL would blame the corpus for a missing toolchain.
+    # Report it as SKIPPED, count it separately, and let --strict (which
+    # refuses to run at all without nickel) be what turns that into a failure.
+    if [ "$want_layer" = "L2" ] && ! nickel_bin >/dev/null; then
+      # Assert the half that CAN be asserted. An L2 control must be lexically
+      # clean, or it is not testing L2 at all — it is an L1 fixture with the
+      # wrong name, and it would keep "passing" after the L2 check broke.
+      local saved_layer="$LAYER"
+      LAYER="L1"
+      if out="$(validate_one "$f" 2>&1)"; then
+        echo -e "${YEL}SKIP${NC} $base — lexically clean as required; needs nickel to assert L2 rejection"
+        nskipped=$((nskipped + 1))
+      else
+        printf '%s\n' "$out" >&2
+        echo -e "${RED}FAIL${NC} $base is an L2 control but already fails at L1 — it is not testing L2"
+        fails=$((fails + 1))
+      fi
+      LAYER="$saved_layer"
+      continue
+    fi
+
+    # Attribution is read off the JSON findings, NOT off free text. The human
+    # line is `ERROR <rule> [<layer>] <path>: <msg>`, and a negative control's
+    # path deliberately CONTAINS its rule id — so grepping the human output for
+    # K9-N001 matched the filename and the control "proved" itself no matter
+    # which rule fired. The first CI run caught exactly that: the contract did
+    # not typecheck, both L2 controls were rejected by K9-N002, and both still
+    # reported ok. A gate that cannot fire is the defect class this suite
+    # exists to prevent, so the assertion reads the structured verdict.
+    local saved_json="$JSON"
+    JSON=1
+    out="$(validate_one "$f" 2>/dev/null)"; rc=$?
+    JSON="$saved_json"
+
+    if [ $rc -eq 0 ]; then
+      echo -e "${RED}FAIL${NC} $base was ACCEPTED — the gate did not fire"
+      fails=$((fails + 1))
+      continue
+    fi
+
+    # Error findings only: a skip or a warning is not a rejection, and letting
+    # one satisfy a negative control would let a missing toolchain pass a gate.
+    local fired
+    fired="$(printf '%s' "$out" \
+      | grep -oE '"severity":"error","rule":"K9-[A-Z][0-9]+","layer":"L[0-9]+"' \
+      | sed -E 's/.*"rule":"(K9-[A-Z][0-9]+)","layer":"(L[0-9])"/\1 \2/' \
+      | sort -u || true)"
+
+    # K9-N002 means the normative contract itself is broken, in which case no
+    # L2 control can have proved anything — say that, not "wrong rule".
+    if printf '%s' "$fired" | grep -q '^K9-N002 '; then
+      echo -e "${RED}FAIL${NC} $base cannot assert $want_rule: the normative contract does not typecheck (K9-N002), so L2 rejected nothing on its own merits"
+      printf '%s\n' "$out" >&2
+      fails=$((fails + 1))
+      continue
+    fi
+
+    if [ -n "$want_rule" ] && ! printf '%s\n' "$fired" | grep -qE "^$want_rule $want_layer$"; then
+      printf '%s\n' "$out" >&2
+      echo -e "${RED}FAIL${NC} $base was rejected, but not by $want_rule at $want_layer"
+      [ -n "$fired" ] && echo "        fired instead: $(printf '%s\n' "$fired" | tr '\n' ';')" >&2
+      fails=$((fails + 1))
+      continue
+    fi
+    echo -e "${GRN}ok${NC}   $base (rejected by $want_rule at $want_layer)"
+  done < <(find "$dir/invalid" -type f \( -name '*.k9.ncl' -o -name '*.k9' -o -name '*.ncl' \) | sort)
+  if [ $nneg -eq 0 ]; then
+    echo -e "${RED}FAIL${NC} no negative fixtures found"; fails=$((fails + 1))
+  fi
+
+  echo
+  echo "fixtures: $npos positive, $nneg negative ($nskipped needing nickel), $fails failure(s)"
+  STRICT="$outer_strict"
+  [ $fails -eq 0 ] || return 1
+  return 0
+}
+
+# ════════════════════════════════════════════════════════════════════════
+main() {
+  local total=0 bad=0 skipped_only=0 rc
+
+  if [ "$SELFTEST" -eq 1 ]; then
+    [ -f "$CONTRACT" ] || { echo "k9-validate: contract not found at $CONTRACT" >&2; exit 2; }
+    self_test; exit $?
+  fi
+
+  if [ ! -f "$CONTRACT" ]; then
+    echo "k9-validate: normative contract not found at $CONTRACT" >&2
+    exit 2
+  fi
+
+  if [ -n "$FIXTURES" ]; then
+    local want_strict="$STRICT"
+    run_fixtures "$FIXTURES"; rc=$?
+    STRICT="$want_strict"   # run_fixtures lowers it for the per-file verdicts
+    if [ $rc -eq 0 ] && [ "$STRICT" -eq 1 ] && ! nickel_bin >/dev/null; then
+      echo -e "${YEL}k9-validate: --strict, but no nickel binary — L2 semantics were never checked, so this run is not a conformance result${NC}" >&2
+      exit 3
+    fi
+    exit $rc
+  fi
+
+  if [ $# -eq 0 ]; then usage >&2; exit 2; fi
+
+  for F in "$@"; do
+    total=$((total + 1))
+    validate_one "$F"; rc=$?
+    case $rc in
+      0) : ;;
+      3) skipped_only=1 ;;
+      *) bad=$((bad + 1)) ;;
+    esac
+  done
+
+  if [ "$bad" -gt 0 ]; then
+    [ "$QUIET" -eq 1 ] || echo -e "${RED}k9-validate: $bad of $total file(s) non-conforming${NC}" >&2
+    exit 1
+  fi
+  if [ "$skipped_only" -eq 1 ]; then
+    echo -e "${YEL}k9-validate: conforming so far as it could check, but required checks were SKIPPED${NC}" >&2
+    exit 3
+  fi
+  [ "$QUIET" -eq 1 ] || note "$total file(s) conforming at layer $LAYER (contract v$CONTRACT_VERSION)"
+  exit 0
+}
+
+main "$@"