diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index 5ef9a75f..d5008103 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -21,18 +21,20 @@ workflows:
     '.github/workflows/dogfood-gate.yml':
         - 'actions/checkout@v7.0.1'
         - 'hyperpolymath/deed-ecosystem@main'
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/e2e.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
         - 'goto-bus-stop/setup-zig@v2.2.1'
         - 'swatinem/rust-cache@v2.9.3'
+    '.github/workflows/fork-governance-publish.yml':
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/fork-governance.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/governance.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/hypatia-scan.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/instant-sync.yml':
         - 'peter-evans/repository-dispatch@v4.0.1'
     '.github/workflows/label-triage.yml': []
@@ -40,15 +42,15 @@ workflows:
     '.github/workflows/main-estate-audit.yml':
         - 'hyperpolymath/cicd-suite@4f5404281dd7092fa77cc18daec7237c4f1ee4ac'
     '.github/workflows/mirror.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/push-email-notify.yml':
         - 'hyperpolymath/smtp-notify-action@v0.5.0'
     '.github/workflows/rust-ci.yml':
         - 'metadatastician/standards@412a7031577112b31ee287cc6060179d638d6500'
     '.github/workflows/scorecard.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/secret-scanner.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
 dependencies:
     'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9':
         ref: 'v6.1.0'
@@ -183,9 +185,14 @@ dependencies:
         commit: 'sha1-c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef'
         owner_id: 6759885
         repo_id: 1352485172
-    'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6':
-        ref: 'e064539116c2dcfdf282a4749dbd58c69961c7e6'
-        commit: 'sha1-e064539116c2dcfdf282a4749dbd58c69961c7e6'
+    'metadatastician/standards@412a7031577112b31ee287cc6060179d638d6500':
+        ref: '412a7031577112b31ee287cc6060179d638d6500'
+        commit: 'sha1-412a7031577112b31ee287cc6060179d638d6500'
+        owner_id: 297579217
+        repo_id: 1116521501
+    'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5':
+        ref: '9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
+        commit: 'sha1-9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
         owner_id: 297579217
         repo_id: 1116521501
         uses:
@@ -201,11 +208,6 @@ dependencies:
             - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e'
             - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6'
             - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555'
-    'metadatastician/standards@412a7031577112b31ee287cc6060179d638d6500':
-        ref: '412a7031577112b31ee287cc6060179d638d6500'
-        commit: 'sha1-412a7031577112b31ee287cc6060179d638d6500'
-        owner_id: 297579217
-        repo_id: 1116521501
     'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e':
         ref: 'v2.5.0'
         commit: 'sha1-fa7117db83c52d787ae5a89f350999701505d78e'
diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml
index 96cb85b1..57760159 100644
--- a/.github/workflows/build-validation.yml
+++ b/.github/workflows/build-validation.yml
@@ -44,6 +44,39 @@ jobs:
       - name: Build Panel Contract Compiler
         run: cargo build --locked --release --manifest-path tools/pcc/Cargo.toml
 
+  # Provenance model (docs/models/Provenance.tla, a PROOF-POLICY §4
+  # exception recorded in PROOF-NEEDS.adoc): TLC checks that a chain
+  # verifies only if it is the genuine one while either signing key is
+  # uncompromised, and must find the forgery when both are.
+  #
+  # PROOF-POLICY §6 deviation (also recorded in PROOF-NEEDS.adoc, state
+  # open): PanLL has no Guix manifest or proof container that provides TLC,
+  # so the official tla2tools.jar release asset is fetched and checked
+  # against the SHA-256 recorded here; the script asserts the TLC version
+  # it ran.  Java is the runner image's.
+  provenance-model:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    permissions:
+      contents: read
+    env:
+      TLA2TOOLS_URL: https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+      TLA2TOOLS_SHA256: 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Fetch TLA+ tools v1.7.4 (pinned by digest)
+        run: |
+          curl -fsSL --proto '=https' --proto-redir '=https' --tlsv1.2 --retry 3 -o "$RUNNER_TEMP/tla2tools.jar" "$TLA2TOOLS_URL"
+          echo "$TLA2TOOLS_SHA256  $RUNNER_TEMP/tla2tools.jar" | sha256sum -c -
+          java -version
+
+      - name: Model-check the provenance binding (both ways)
+        run: bash scripts/check-provenance-model.sh "$RUNNER_TEMP/tla2tools.jar"
+
   # panel-clades ABI: every PanelClades.ABI module typechecks against
   # typed-wasm's grade kernel at its pin, and the expected rejections are
   # refused.  Idris2 publishes no binaries, so 0.8.0 is built from source,
@@ -62,6 +95,11 @@ jobs:
         with:
           persist-credentials: false
 
+      # The source scans check-abi.sh relies on, tested both ways; needs no
+      # Idris2, so it fails fast before the 8-minute toolchain build.
+      - name: ABI scan regression tests
+        run: bash panel-clades/tests/scan/test-abi-scan.sh
+
       - name: Install Chez Scheme and GMP
         run: |
           sudo apt-get update -qq
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index ae480ec8..52742375 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -74,7 +74,7 @@ jobs:
   k9-conformance:
     name: K9-DEED conformance (push)
     if: github.event_name == 'push'
-    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
       pull-requests: read
diff --git a/.github/workflows/fork-governance-publish.yml b/.github/workflows/fork-governance-publish.yml
new file mode 100644
index 00000000..031f610e
--- /dev/null
+++ b/.github/workflows/fork-governance-publish.yml
@@ -0,0 +1,181 @@
+# This workflow is managed by gh actions-lock.
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+# fork-governance-publish.yml — post the Fork governance comment on pull
+# requests from forks.
+#
+# On a fork PR GitHub gives the "Fork governance" run a read-only token, so
+# its verdict job uploads the rendered comment as an artifact instead of
+# posting it. This workflow runs after every "Fork governance" run, from the
+# default branch's copy with this repository's token, and posts that comment
+# as escaped, explicitly untrusted text. It skips same-repository runs,
+# which post their own comment. It takes effect once merged to main.
+#
+# Publisher vendored from metadatastician/standards at
+# 9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5, with safe artifact rendering.
+# Preserve the shared comment marker and publisher stamp protocol.
+name: Fork governance publish
+
+# workflow_run, deliberately: it is the only way to write a comment for a
+# fork PR. Nothing from the fork runs here. This job checks out no code,
+# reads the artifact as data, and posts only to the open PR whose head is
+# the commit the run built.
+on:
+  workflow_run:
+    workflows: ["Fork governance"]
+    types: [completed]
+
+permissions:
+  contents: read
+
+jobs:
+  publish:
+    name: Publish the fork governance summary (fork PR)
+    # Only a completed pull_request run from a fork has anything to publish;
+    # every other run posted its own comment.
+    if: >-
+      ${{ github.event_name == 'workflow_run'
+          && github.event.workflow_run.event == 'pull_request'
+          && github.event.workflow_run.head_repository.full_name != github.repository }}
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    # One publisher at a time per fork branch, so the read-compare-write of
+    # the comment below never interleaves with another publisher's.
+    concurrency:
+      group: fork-governance-publish-${{ github.event.workflow_run.head_repository.full_name }}-${{ github.event.workflow_run.head_branch }}
+      cancel-in-progress: false
+    permissions:
+      actions: read
+      pull-requests: write
+    steps:
+      - name: Download the rendered comment
+        id: download
+        continue-on-error: true
+        uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
+        with:
+          name: fork-governance-comment
+          path: ${{ runner.temp }}/fork-governance-comment
+          run-id: ${{ github.event.workflow_run.id }}
+          github-token: ${{ github.token }}
+
+      # A run may leave no artifact only when it was replaced: a newer attempt
+      # of the same run, or a newer push to the fork branch (a newer run at a
+      # different commit; a push re-runs every pull request from the branch,
+      # so each one gets its own successor). Anything else is a missing report
+      # and fails here, including a run cancelled by hand with no successor.
+      - name: Fail on a missing comment
+        if: ${{ steps.download.outcome != 'success' }}
+        env:
+          GH_TOKEN: ${{ github.token }}
+          RUN_ID: ${{ github.event.workflow_run.id }}
+          RUN_ATTEMPT: ${{ github.event.workflow_run.run_attempt }}
+          WORKFLOW_ID: ${{ github.event.workflow_run.workflow_id }}
+          RUN_HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+          RUN_HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          RUN_HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+          RUN_CONCLUSION: ${{ github.event.workflow_run.conclusion }}
+          RUN_URL: ${{ github.event.workflow_run.html_url }}
+        run: |
+          set -euo pipefail
+          pushed=$(gh api -X GET "repos/$GITHUB_REPOSITORY/actions/workflows/$WORKFLOW_ID/runs" \
+              -f event=pull_request -f branch="$RUN_HEAD_BRANCH" -f per_page=100 \
+            | jq --arg repo "$RUN_HEAD_REPO" --arg sha "$RUN_HEAD_SHA" --argjson id "$RUN_ID" \
+                '[.workflow_runs[] | select(.head_repository.full_name == $repo and .id > $id and .head_sha != $sha)] | length')
+          attempt=$(gh api "repos/$GITHUB_REPOSITORY/actions/runs/$RUN_ID" --jq '.run_attempt')
+          if [ "$pushed" -gt 0 ] || [ "$attempt" -gt "$RUN_ATTEMPT" ]; then
+            echo "$RUN_URL left no comment, but a newer push or attempt replaced it; that run publishes."
+            exit 0
+          fi
+          echo "::error::$RUN_URL ($RUN_CONCLUSION) uploaded no fork-governance-comment artifact and nothing replaced it, so its pull request has no governance comment"
+          exit 1
+
+      - name: Publish the comment
+        if: ${{ steps.download.outcome == 'success' }}
+        env:
+          GH_TOKEN: ${{ github.token }}
+          GRID_AUTHOR: github-actions[bot]
+          RUN_ID: ${{ github.event.workflow_run.id }}
+          RUN_ATTEMPT: ${{ github.event.workflow_run.run_attempt }}
+          RUN_HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+          RUN_HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          RUN_HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+          RUN_URL: ${{ github.event.workflow_run.html_url }}
+        run: |
+          set -euo pipefail
+          dir="$RUNNER_TEMP/fork-governance-comment"
+          body="$dir/body.md"
+          meta="$dir/meta.json"
+          [ -f "$body" ] && [ -f "$meta" ] || { echo "::error::artifact is missing body.md or meta.json"; exit 1; }
+
+          pr=$(jq -r '.pr_number // ""' "$meta")
+          if ! [[ "$pr" =~ ^[1-9][0-9]{0,9}$ ]]; then
+            echo "::error::artifact pr_number is not a pull request number"; exit 1
+          fi
+
+          # The pull request must be this run's own: open, at the commit the
+          # run built, from the fork and branch the run came from (header).
+          # Captured first, so a failed lookup fails the step under `set -e`
+          # instead of reading as "not open".
+          pr_info=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$pr" \
+            --jq '[.state, .head.sha, (.head.repo.full_name // "-"), .head.ref] | join(" ")')
+          # A git ref cannot contain whitespace, so the branch is the last field.
+          read -r pr_state pr_sha pr_repo pr_branch <<< "$pr_info"
+          if [ "$pr_state" != open ]; then
+            echo "Pull request #$pr is $pr_state; nothing to publish."; exit 0
+          fi
+          if [ "$pr_sha" != "$RUN_HEAD_SHA" ]; then
+            echo "Pull request #$pr has moved past $RUN_HEAD_SHA; its newer run publishes."; exit 0
+          fi
+          if [ "$pr_repo" != "$RUN_HEAD_REPO" ] || [ "$pr_branch" != "$RUN_HEAD_BRANCH" ]; then
+            echo "::error::artifact names #$pr, which is not from $RUN_HEAD_REPO:$RUN_HEAD_BRANCH"; exit 1
+          fi
+
+          if ! head -n 1 "$body" | grep -q '^<!-- fork-governance-verdict:'; then
+            echo "::error::body does not start with the fork-governance marker"; exit 1
+          fi
+          # The run stamp is the comment's last line, written here and never by
+          # the fork, so the last stamp in a comment is always the publisher's.
+          {
+            # Fixed trusted framing; artifact bytes are text, never Markdown/HTML.
+            printf '<!-- fork-governance-verdict: untrusted-fork-report -->\n'
+            printf '## Untrusted fork governance report\n\n'
+            printf 'The following text was supplied by the fork. It is not a verified bot verdict. Consult the lane checks for results.\n\n'
+            printf '<pre>\n'
+            jq -Rrs '@html' "$body"
+            printf '</pre>\n'
+            printf '\n<sub>Rendered by the fork pull request run %s and published by fork-governance-publish.</sub>\n' "$RUN_URL"
+            printf '<!-- fork-governance-publish-run: %s.%s -->\n' "$RUN_ID" "$RUN_ATTEMPT"
+          } > "$dir/published.md"
+          # GitHub's limit is 65536 characters, not bytes; the glyphs are
+          # multibyte, so count characters.
+          if [ "$(LC_ALL=C.UTF-8 wc -m < "$dir/published.md")" -gt 65000 ]; then
+            echo "::error::body exceeds the 65000-character comment limit"; exit 1
+          fi
+
+          existing=$(gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/issues/$pr/comments" \
+            | jq -c --arg a "$GRID_AUTHOR" \
+                '[.[][] | select((.user.login // "") == $a and ((.body // "") | contains("<!-- fork-governance-verdict:")))]
+                 | last // {} | {id: (.id // ""), body: (.body // "")}')
+          comment_id=$(jq -r '.id' <<< "$existing")
+          # Runs for one pull request can finish out of order (a re-run, or a
+          # close and reopen). Never replace a comment a newer run published:
+          # compare this run's id, then attempt, with the comment's last stamp.
+          stamp=$(jq -r '.body' <<< "$existing" \
+            | sed -n 's/^<!-- fork-governance-publish-run: \([0-9]*\)\.\([0-9]*\) -->$/\1 \2/p' | tail -n 1)
+          if [ -n "$stamp" ]; then
+            read -r prev_id prev_attempt <<< "$stamp"
+            if [ "$prev_id" -gt "$RUN_ID" ] || { [ "$prev_id" -eq "$RUN_ID" ] && [ "$prev_attempt" -gt "$RUN_ATTEMPT" ]; }; then
+              echo "#$pr already carries the comment from newer run $prev_id.$prev_attempt; leaving it."; exit 0
+            fi
+          fi
+
+          jq -n --rawfile body "$dir/published.md" '{body: $body}' > "$dir/comment.json"
+          if [ -n "$comment_id" ]; then
+            gh api -X PATCH "repos/$GITHUB_REPOSITORY/issues/comments/$comment_id" \
+              --input "$dir/comment.json" >/dev/null
+            echo "updated the fork governance comment on #$pr ($comment_id)"
+          else
+            gh api -X POST "repos/$GITHUB_REPOSITORY/issues/$pr/comments" \
+              --input "$dir/comment.json" >/dev/null
+            echo "posted the fork governance comment on #$pr"
+          fi
diff --git a/.github/workflows/fork-governance.yml b/.github/workflows/fork-governance.yml
index a2810da1..556624fb 100644
--- a/.github/workflows/fork-governance.yml
+++ b/.github/workflows/fork-governance.yml
@@ -29,7 +29,7 @@ permissions:
 jobs:
   deed:
     name: DEED syntax
-    uses: metadatastician/standards/.github/workflows/deed-conformance.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/deed-conformance.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
     with:
@@ -37,7 +37,7 @@ jobs:
 
   k9:
     name: K9-DEED conformance
-    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
       pull-requests: read
@@ -47,7 +47,7 @@ jobs:
 
   hypatia:
     name: Hypatia verdict grid
-    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       actions: read
       contents: read
@@ -59,7 +59,7 @@ jobs:
     name: Post the fork governance summary
     needs: [deed, k9, hypatia]
     if: ${{ always() && github.event_name == 'pull_request' }}
-    uses: metadatastician/standards/.github/workflows/fork-governance-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/fork-governance-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
       actions: read
@@ -72,4 +72,4 @@ jobs:
       hypatia-result: ${{ needs.hypatia.result }}
       hypatia-verdict: ${{ needs.hypatia.outputs.verdict }}
       hypatia-advisory: ${{ needs.hypatia.outputs.advisory }}
-      canon-ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
+      canon-ref: 9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index f6fbd6fa..4f41c538 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -33,6 +33,6 @@ permissions:
 
 jobs:
   governance:
-    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     secrets:
       HYPATIA_SCAN_PAT: ${{ secrets.HYPATIA_SCAN_PAT }}
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index 0cece4aa..2ec0e9a5 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -34,6 +34,6 @@ jobs:
       actions: read
       contents: read
       security-events: write
-    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     secrets:
       HYPATIA_SCAN_PAT: ${{ secrets.HYPATIA_SCAN_PAT }}
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index b8159a9a..7d168193 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -16,7 +16,7 @@ jobs:
     # A manual dispatch from a feature branch has no local main ref to push.
     # Mirror only the canonical branch, as the push trigger already requires.
     if: github.ref == 'refs/heads/main'
-    uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     secrets:
       GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }}
       CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }}
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
index d30c1e18..65511c8e 100644
--- a/.github/workflows/scorecard.yml
+++ b/.github/workflows/scorecard.yml
@@ -16,4 +16,4 @@ jobs:
       contents: read
       security-events: write
       id-token: write
-    uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml
index b165dfe5..9e1e4f1e 100644
--- a/.github/workflows/secret-scanner.yml
+++ b/.github/workflows/secret-scanner.yml
@@ -21,4 +21,4 @@ jobs:
       contents: read
       pull-requests: write
       actions: read
-    uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 4f23bd0d..a6fea9e6 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -9,6 +9,37 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === https://github.com/hyperpolymath/panll/compare/v0.1.0...HEAD[Unreleased]
 
+==== Added (2026-11-09 — panel-clades layout proofs and a stricter ABI gate)
+
+* *Rounding up is tight.* For an alignment `+a ≥ 1+`, `+alignUp+` is at or
+above the size and below size plus `+a+` (`+alignUpCovers+`,
+`+alignUpTight+`).
+* *Struct size covers every field.* `+calcStructSizeCovers+` and
+`+fieldWithinStruct+` prove it, so `+verifyLayout+` drops its run-time
+check and refuses only an alignment of 0. `+StructLayout+` now carries
+that coverage as an `+LTE+` proof instead of a Boolean `+So+`.
+* *C layout evidence.* `+CABICompliant+` now also carries at least one
+field, the first at offset 0 (`+FirstAtZero+`), fields in order without overlap
+(`+FieldsOrdered+`), power-of-two alignments
+(`+AlignmentsPow2+`, decided by `+decPow2+`), and a struct alignment equal
+to the largest field alignment (`+maxAlignment+`). `+checkCABI+` decides
+all five parts.
+* *Tag tables agree.* `+resultTagsAgree+` and `+cladeKindTagsAgree+` tie
+each `+Bits32+` C encoding to its `+Nat+` equality tag.
+* Five more expected rejections: `+EmptyStruct+`, `+FirstFieldNotAtZero+`,
+`+OverlappingFields+`, `+AlignmentNotPow2+`, `+StructUnderAligned+`.
+* `+check-abi.sh+` now also fails on holes, `+partial+`, `+covering+` and a
+module without `+%default total+` before its first declaration, reads
+code only (not comments, strings, raw or multi-line strings, or character
+literals, though string interpolations are scanned as code), and holds the typed-wasm import cone to the same scan.
+* *Provenance model rewritten and run in CI.* `+docs/models/Provenance.tla+`
+now has an adversary that signs under a leaked key, separate author and
+witness signatures, and the invariant `+Genuine+`: a verified chain is
+exactly the genuine one while either key is uncompromised. The previous
+invariant held by construction. The `+provenance-model+` job
+(`+build-validation.yml+`) runs TLC with each single key leaked (must hold)
+and with both leaked (must find the forgery).
+
 ==== Removed (2026-11-05)
 
 * *The PCC ReScript scanner (`tools/pcc/src/rescript_scanner.rs`) is
diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index cfadd97a..ef033d38 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -6,17 +6,47 @@ What PanLL proves today, what it deliberately does not, and what is still
 owed. Escape hatches and their dispositions are tracked separately in
 link:docs/proof-debt.adoc[`docs/proof-debt.adoc`].
 
-Last reconciled against the tree: 2026-10-26 (`main` at `1937c6b`).
+Last reconciled against the tree: 2026-11-09 (`main` at `7d1feaa`).
+
+The policy is hyperpolymath/standards `3-practice/PROOF-POLICY.adoc`.
+Statuses in this file use its closed §5 vocabulary: `PROVEN`, `TESTED`,
+`ASSUMED`, `OPEN`. Anything else said about an item is in a separate
+note, never in place of the token.
 
 toc::[]
 
+== Policy class
+
+Every obligation PanLL owns is an *engineering* obligation (PROOF-POLICY §1):
+
+* interface and ABI contracts (types, layouts, tags, grade contracts) in
+  *Idris2*;
+* first-party Rust in *Creusot* with *Pearlite* contracts, and *Verus*
+  (§1.2);
+* Rust `unsafe` blocks and FFI seams additionally in *Kani*, reported as
+  `TESTED` with its bounds (§4.1).
+
+PanLL owns no theory theorem, so Proof Witness Grades do not apply here
+(§8.1): no `PWG` is stated or owed. The laws of the grade algebras that
+`Grades.idr` uses (occupancy, loss, max-plus) are theory. Their source of
+truth is hyperpolymath/resource-algebra's Agda, and any grade for them is
+recorded there. PanLL uses typed-wasm's Idris2 transcription of them as a
+checked dependency (the import cone below); whether that transcription
+states the same laws is the open item "Grade kernel identity" (#143).
+
+The Mathesis catalogue (hyperpolymath/mathesis, `docs/catalogue/`) lists
+PanLL as an engineering repository whose status document is this file.
+Its row comes from the census of 2026-10-26, so it does not yet count the
+TLA+ model added since (`docs/models/`); Mathesis derives its rows from
+the tree at each census and does not assign them.
+
 == Current state
 
 The only machine-checked proofs live in the panel-clades ABI,
 `panel-clades/src/abi/PanelClades/ABI/` (Idris2 0.8.0, `%default total`,
 about 1,300 lines). As of the date above, no `.idr` file contains a hole,
 `believe_me`, `assert_total`, `assert_smaller`, `idris_crash`,
-`unsafePerformIO` or `postulate`.
+`unsafePerformIO`, `postulate`, `partial` or `covering`.
 
 The CI job `panel-clades-abi` in `.github/workflows/build-validation.yml`
 runs `panel-clades/scripts/check-abi.sh`, which:
@@ -25,35 +55,102 @@ runs `panel-clades/scripts/check-abi.sh`, which:
   `panel-clades/scripts/fetch-siblings.sh` (`117bbf8`);
 * builds `panel-clades/src/abi/panel-clades-grades.ipkg` against it and
   fails on any `Error:` line, even when `idris2` exits 0;
-* fails if any module under `PanelClades/` is missing from the ipkg, or
-  contains `believe_me`, `assert_total`, `assert_smaller`, `idris_crash`,
-  `unsafePerformIO` or `postulate` (a keyword scan; it does not look for
-  holes);
+* fails if any module under `PanelClades/` is missing from the ipkg or
+  does not declare `%default total` before its first declaration (the
+  directive applies only from where it appears), or if its code contains
+  a hole (`?name`, any case; `idris2 --build` accepts a module with
+  holes), `believe_me`, `assert_total`, `assert_smaller`,
+  `idris_crash`, `unsafePerformIO`, `postulate`, `partial` or `covering`.
+  Comments, string literals and character literals are set aside, but an
+  interpolation (`\{...}`) inside a string is code and is scanned;
+* holds the typed-wasm modules those modules import (the import cone,
+  PROOF-POLICY §1.1) to the same scan, and prints the cone;
 * fails if `Budgets.idr` is stale against the clade configs
   (`scripts/gen-budgets.sh --check`);
 * requires each of the six fixtures in `panel-clades/tests/reject/` to be
   refused at its `invalid` declaration, with the expected message.
 
-=== What is proved
+=== Receipt
+
+The most recent receipt is the `panel-clades-abi` job of Build Validation
+run
+https://github.com/hyperpolymath/panll/actions/runs/42408104327[42408104327]
+(job 128510101342), on `main` at
+`7d1feaaf112b3d91fd504aaf871be5ae49840434`, 2026-11-07.
 
 [cols="1,3",options="header"]
 |===
-|Module |Proved
+|Field |Value
+
+|Checker
+|Idris2 0.8.0, built from idris-lang/Idris2
+`15a3e4e70843f7a34100f6470c04b791330788df` on Chez Scheme (Ubuntu
+package)
+
+|Invocation
+|`bash panel-clades/scripts/check-abi.sh`, which runs
+`idris2 --build panel-clades-grades.ipkg` with the kernel's TTCs on
+`IDRIS2_PATH`, then `idris2 --check` on each reject fixture
+
+|Import cone
+|hyperpolymath/typed-wasm `117bbf895b513673ba06eb6c4ebb0e26e276e295`:
+`TypedWasm.ABI.ResourceAlgebra`, `.Nat`, `.Loss`, `.MaxPlus`, `.HWM`, all
+`%default total`, no escape hatch or hole. Below that, only Idris2's own
+prelude and base (`Data.List`, `Data.Nat`, `Data.So`, `Data.Vect`,
+`Data.Vect.Elem`, `Decidable.Equality`), which are the prover's trust base.
+
+|Result
+|5 modules built, 0 errors; 6 of 6 fixtures refused at their `invalid`
+declaration
+|===
+
+That run predates the import-cone and hole scans, the tag-agreement
+proofs, the layout bounds and the C layout evidence. On 2026-11-09 the
+same `check-abi.sh`, with those additions, ran locally with Idris2 0.8.0
+built from the same commit and passed: 5 modules, 0 errors, 11 of 11
+fixtures refused, and the cone above clean. A local run is not a receipt. The
+first `main` run after this change is the first receipt to include them.
+A receipt is current only for its commit: rerun the job, never carry a
+result forward.
+
+=== What is proved
+
+[cols="1,1,3",options="header"]
+|===
+|Module |Status |Proved
 
 |`Types.idr`
+|`PROVEN`
 |The C tag encodings of `Result` and `CladeKind` round-trip, so they are
 injective (`resultRoundTrip`, `cladeKindRoundTrip`). Equality on both is
 decidable without a catch-all `absurd` (`decEqViaTag`). `allCladeKinds`
 lists every kind (`cladeKindExhaustive`) and has length `cladeKindCount`.
-A `Handle` is never null and a `CladeId` is never empty, by construction.
+Each tag is written twice, as a `Nat` for decidable equality and as a
+`Bits32` for the C encoding, and the two give the same number
+(`resultTagsAgree`, `cladeKindTagsAgree`), so the tables cannot drift
+apart. A `Handle` is never null and a `CladeId` is never empty, by
+construction.
 
 |`Layout.idr`
-|Rounding up to an alignment lands on a multiple of it (`alignUpCorrect`).
-Every computed struct size is a multiple of its alignment
-(`calcStructSizeAligned`). Field alignment is decided by an equation on
-`Nat` (`decDivides`, `proveFieldsAligned`), not by a Boolean test.
+|`PROVEN`
+|Rounding up to an alignment `a ≥ 1` is tight: the result is a multiple
+of `a` (`alignUpCorrect`), at or above the size (`alignUpCovers`) and
+below size plus `a` (`alignUpTight`). A computed struct size is a
+multiple of its alignment (`calcStructSizeAligned`) and covers every field
+(`calcStructSizeCovers`, `fieldWithinEnd`, `fieldWithinStruct`), so
+`verifyLayout` has no run-time size check and refuses only an alignment of
+0. `CABICompliant` evidence carries every offset as a multiple of its
+alignment (`FieldsAligned`), at least one field with the first at
+offset 0, since C requires a member and allows no padding before the
+first (`FirstAtZero`), the fields in order with each
+starting at or after the previous one's end (`FieldsOrdered`; no two
+overlap, since the chain is ordered), every alignment a power of two (`AlignmentsPow2`), and
+the struct aligned to its largest field alignment (`maxAlignment`). Each
+part is decided by an equation or an `LTE` proof (`decDivides`,
+`isLTE`, `decPow2`, `decEq`), not by a Boolean test.
 
 |`Grades.idr`
+|`PROVEN`
 |Clade resource contracts are graded in typed-wasm's kernel (transcribed
 from hyperpolymath/resource-algebra), not re-declared. Occupancy composes
 within a bound (`phasesWithin`). Loss adds across two crossings
@@ -61,28 +158,33 @@ within a bound (`phasesWithin`). Loss adds across two crossings
 bound (`betterOfTwo`). Occupancy and cost are kept apart
 (`panelPhasesOccupancy` vs `panelPhasesCost`). The neurosym-bridge
 contract typechecks against its declared budget
-(`neurosymBridgeContract`).
-
-|`Budgets.idr`
-|Generated from the clades' `config.k9.ncl` resource blocks. It proves
-nothing itself; it is the input `Grades.idr` checks against. Only
-neurosym-bridge declares a budget so far.
+(`neurosymBridgeContract`). The kernel is in the checked import cone, so
+it is not an assumption; whether its definitions match resource-algebra's
+is #143.
 
-|`Foreign.idr`
-|Typechecks only. It declares the Zig FFI surface; it proves nothing.
 |===
 
-The reject fixtures pin down what the types refuse: `BudgetTooSmall`,
-`CollapseWithinTolerance`, `MisalignedField`, `NullHandle`, `OverBudget`
+Two modules carry no obligation and are not in the table.
+`Budgets.idr` is generated from the clades' `config.k9.ncl` resource
+blocks; it is the input `Grades.idr` checks against. Only neurosym-bridge
+declares a budget so far, and the budgets are DESIGNED values, not
+measurements. `Foreign.idr` declares the Zig FFI surface and only
+typechecks.
+
+The reject fixtures pin down what the types and the decision procedures
+refuse: `AlignmentNotPow2`, `BudgetTooSmall`,
+`CollapseWithinTolerance`, `MisalignedField`, `NullHandle`, `OverBudget`,
+`OverlappingFields`, `StructUnderAligned`
 and `WasmPointerIsEightBytes`.
 
 === What is not proved
 
 These limits are stated in the modules themselves.
 
-* *Struct size covers the last field.* `Layout.idr` does not prove that a
-  computed size is at least the end of the last field; `verifyLayout`
-  checks it at run time and refuses a layout that fails.
+* *The decision procedures are complete.* `decDivides`, `decPow2` and
+  `checkCABI` are sound: every `Just` or `Right` carries real evidence. A
+  `Nothing` or `Left` means only "not shown"; that the property is then
+  false is not proved.
 * *The Zig side matches.* Nothing checks that `panel-clades/ffi/zig/`
   exports the symbols `Foreign.idr` declares, with those types, or uses
   the sizes and tags `Types.idr` proves. `ffi/zig/src/main.zig` restates
@@ -93,54 +195,64 @@ These limits are stated in the modules themselves.
 
 == What needs proving
 
-[cols="2,3,2,1",options="header"]
-|===
-|Item |What |Status |Tracked
+Status is the PROOF-POLICY §5 token. The note says why, and what comes next.
 
-|Struct size lower bound
-|Prove `calcStructSize` is at least the end of the last field, and drop
-the run-time check in `verifyLayout`.
-|Not started. Induction over the field list plus a lemma about rounding
-up.
-|—
+[cols="2,3,1,2,1",options="header"]
+|===
+|Item |What |Status |Note |Tracked
 
 |Safe callback registration
 |A safe wrapper for `prim__registerCallback` in `Foreign.idr`, using
 Idris2's FFI callback mechanism (`cast` is banned).
+|`OPEN`
 |Not started.
 |#149
 
 |Zig/Idris FFI agreement
 |Check that the Zig exports match `Foreign.idr` and the proven sizes and
-tags. This is a CI check, not a proof.
-|Not started.
+tags.
+|`OPEN`
+|Not started. A CI check, not a proof; once it runs it is `TESTED`
+evidence, not `PROVEN`.
 |—
 
 |Grade kernel identity
 |Confirm typed-wasm's transcription matches resource-algebra's Agda
 `MaxPlus` kernel, which is now the family instance.
-|Open question; PanLL already imports the kernel through typed-wasm.
+|`OPEN`
+|PanLL already imports the kernel through typed-wasm; the question is
+whether the Idris2 and Agda statements are the same.
 |#143
 
 |More clade budgets
 |As clade configs declare resource blocks, `gen-budgets.sh` emits them
 and their contracts need to typecheck.
-|One clade so far (neurosym-bridge).
+|`OPEN`
+|One clade so far (neurosym-bridge, `PROVEN` against its declared
+budget).
 |—
 
-|IPC dispatch is total
-|Every command the frontend invokes has a registered handler.
-|Backend side covered by tests in `src-gossamer/src/ipc.rs`:
+|IPC dispatch is total: backend side
+|Every public handler in a backend command module is registered, once.
+|`TESTED`
+|Tests in `src-gossamer/src/ipc.rs`:
 `every_backend_command_is_registered` fails if a public handler in a
 command module is reachable from neither the table nor `main.rs`, and
-the table and `main.rs` never register the same name twice. Checking the
-frontend side needs its `invoke` names, which wait on the AffineScript
+the table and `main.rs` never register the same name twice. The Rust
+implementation obligation is in the next section.
+|#148
+
+|IPC dispatch is total: frontend side
+|Every command the frontend invokes has a registered handler.
+|`OPEN`
+|Needs the frontend's `invoke` names, which wait on the AffineScript
 port.
 |#148
 
 |PCC soundness
 |The PanLL Constraint Checker (`tools/pcc`) propagates constraints soundly
 and finds every violation.
+|`OPEN`
 |Blocked: `tools/pcc`'s ReScript scanner is retired, because #107 removed
 the `.res` sources it read. Its frontend-wiring checks now report
 "retired" until an AffineScript scanner replaces them. The propagator
@@ -150,6 +262,7 @@ the AffineScript port, and it needs a written specification first.
 
 |Verification Dashboard accuracy
 |The dashboard reports the real proof state of the repos it inspects.
+|`OPEN`
 |Better served by fixture tests than by proof. Waits on the frontend
 port.
 |#148
@@ -157,27 +270,38 @@ port.
 |Provenance engine
 |Provenance tracking is complete (every action is recorded) and
 unforgeable. Owner decision (2026-11-05): "unforgeable" means each
-provenance record follows `EXHIBIT-B-QUANTUM-SAFE.txt`. The record holds
-the author identity, a timestamp, a SHA3-256 content hash and, optionally,
-a parent hash. It is serialised as canonical JSON, signed with ML-DSA-65
-and witnessed, and verifies against keys published under
-`.well-known/keys/`. Today's engine (git blame plus Co-Authored-By
+provenance record follows PanLL's profile of `EXHIBIT-B-QUANTUM-SAFE.txt`.
+The record holds the author identity, a timestamp, a SHA3-256 content hash
+and, optionally, a parent hash, serialised as canonical JSON. The profile
+is narrower than Exhibit B: ML-DSA-65 only (Exhibit B §2.1 and §4.1 also
+allow ML-DSA-87, SLH-DSA, FALCON or another approved alternative); at
+least one independent witness is required for `verified` (witnesses are
+optional in Exhibit B §3.2); and keys come only from the verifier's
+approved `.well-known/keys/` registry (Exhibit B §5.1 also lists OpenPGP
+keyservers and personal websites). Every record PanLL verifies therefore
+satisfies Exhibit B; some Exhibit B records verify only as `claimed`. Today's engine (git blame plus Co-Authored-By
 trailers) is forgeable, so its output counts only as "claimed".
+|`TESTED`
 |Implemented in `crates/provenance`: JCS records, ML-DSA-65 signing,
 approved public-key registry, independent witnesses, timestamp/content/chain
-verification and mutation/property tests. Symbolic binding model:
-`docs/models/Provenance.tla`; protocol and limits:
-`docs/PROVENANCE-EXHIBIT-B.adoc`. This does not prove every action is recorded,
-prevent tail truncation without a checkpoint, or prove cryptographic hardness.
+verification and mutation/property tests (the `TESTED` evidence).
+Symbolic binding model: `docs/models/Provenance.tla`, `TESTED` in CI, a §4 exception
+whose record is below; protocol and limits:
+`docs/PROVENANCE-EXHIBIT-B.adoc`. This does not prove every action is
+recorded, prevent tail truncation without a checkpoint, or prove
+cryptographic hardness. The implementation proofs are `OPEN`, in the
+next section.
 |#173
 
 |Cartridge schema validation
 |Loading a cartridge validates it against `src/abi/cartridge-schema.json`.
+|`OPEN`
 |Schema only; no validator to prove against yet.
 |—
 
 |Wiring Inspector
 |Wiring analysis finds every panel connection.
+|`OPEN`
 |Waits on the frontend port.
 |#148
 |===
@@ -221,8 +345,11 @@ to the shipped functions. No separate model counts as a proof of them.
 canonicalisation of `content_hash` and the fields bound by signatures and
 attestations. Allocate the obligations against the shipped functions.
 |Only third-party JCS, SHA3-256, ML-DSA-65, entropy and time-parsing primitives
-and their specified behaviour are ASSUMED. Record exact locked versions and
-extern contracts when proofs are introduced; cryptographic hardness, civil
+and their specified behaviour are ASSUMED, at the versions `Cargo.lock` pins
+today: `fips204` 0.5.0 (ML-DSA-65; exact pin `=0.5.0` in
+`crates/provenance/Cargo.toml`), `sha3` 0.10.9, `serde_jcs` 0.2.0, `chrono`
+0.4.45 and `base64` 0.22.1. Record extern contracts when proofs are
+introduced; cryptographic hardness, civil
 identity approval and independent witness judgment are outside these proofs.
 |`src-gossamer/src/ipc.rs` dispatch and `tools/pcc` propagation
 |Creusot / Pearlite and Verus: OPEN
@@ -230,6 +357,16 @@ identity approval and independent witness judgment are outside these proofs.
 specifications; retain current tests as TESTED evidence only.
 |PCC frontend scanning remains blocked on the AffineScript port. Neither
 verifier is silently excluded because that separate dependency is unfinished.
+|Every `unsafe` block and FFI seam in `src-gossamer/`: the `libloading`
+coprocessor calls, the Gossamer and GLib calls in `main.rs`'s event pump,
+`gossamer_tray_destroy`, and the `libc::kill` / `libc::statvfs` calls
+|Kani (PROOF-POLICY §4.1), alongside Creusot / Pearlite and Verus: OPEN
+|Harnesses for each seam's stated `SAFETY` conditions (live handle,
+NUL-terminated strings, matching foreign signatures, valid pid).
+|Reported `TESTED` with unwinding and size bounds when run, never `PROVEN`.
+The foreign side (Zig coprocessor, Gossamer, GLib, libc) is `ASSUMED` at
+its declared signature. The sites, and their debt disposition, are listed
+in link:docs/proof-debt.adoc[`docs/proof-debt.adoc`] (d).
 |===
 
 Any future proof receipt must name source/tool/solver versions, invocation,
@@ -237,11 +374,83 @@ discharged obligations and assumptions. Shared SMT solvers or specifications
 do not establish independent witnesses. Approved contributor keys, independent
 witnesses and trusted checkpoints remain separate operational requirements.
 
+== Exceptions (PROOF-POLICY §4)
+
+=== TLA+ model of provenance binding
+
+[cols="1,3",options="header"]
+|===
+|Field |Record
+
+|Artefact
+|`docs/models/Provenance.tla`, with three TLC configurations:
+`Provenance.cfg` (author key leaked), `ProvenanceWitnessLeak.cfg`
+(witness key leaked) and `ProvenanceBothLeak.cfg` (both leaked). They are
+run by `scripts/check-provenance-model.sh` in the `provenance-model` job of
+`.github/workflows/build-validation.yml`.
+
+|Obligation
+|A chain is verified only if it is exactly the genuine chain, in order and
+with its genuine content, while at least one of the two signing keys
+(author, independent witness) is uncompromised. `Valid` mirrors what
+`crates/provenance` `verify_chain` checks: an author signature and a
+witness attestation on every record, content matching its digest, and each
+record naming its predecessor (the first naming none). The property
+`Genuine` refers to the genuine chain, which the verifier never sees, so it
+is not `Valid` restated.
+
+|Tool
+|TLA+, checked with TLC (`TLC2 Version 2.19 of 08 August 2024`, from
+tla2tools v1.7.4)
+
+|Why not the mapped verifier
+|The statement is about the protocol, symbolically, with signatures as
+sets that only a key holder can add to. The mapped verifiers for the shipped Rust are Creusot /
+Pearlite and Verus. They are planned, not yet run: the `verify_entry` /
+`verify_witnesses` row above is `OPEN`, and this model does not discharge
+it.
+
+|Status
+|`TESTED`, with bounds: two field/digest values (`A`, `B`) plus `None`
+for the genesis parent, so 12 possible payloads; chains of exactly two
+records; any subset of payloads forged under a leaked key. Checked both
+ways. With one leaked key, either one, `Genuine` holds over all 591,872
+distinct reachable states (depth 13). With both keys leaked, TLC must find
+the forgery and does, so the property is not vacuous. Each single-key run
+must also exercise its leak: `check-provenance-model.sh` fails unless TLC's
+coverage report shows the leaked key's forge action reaching a state and
+the other forge action none, so a configuration that leaks no key cannot
+pass. A mutation run that
+dropped the witness check from `Valid` was caught too: one leaked author
+key then forges a chain. Local run on 2026-11-09, about 7 minutes; the
+`provenance-model` job's run on `main` is the receipt.
+
+|Assumed
+|Signatures cannot be produced without the key (ML-DSA-65 unforgeability),
+and the witness attests only genuine records. Timestamps, key
+registration, chains longer than two and tail truncation are not modelled.
+
+|Deviation (PROOF-POLICY §6)
+|*Leg:* this model check. *Tool:* tla2tools.jar v1.7.4, the
+tlaplus/tlaplus GitHub release asset, SHA-256
+`936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88`; TLC
+reports `TLC2 Version 2.19 of 08 August 2024`. *Why:* PanLL has no Guix
+manifest or proof container that provides TLC, so the job fetches the
+release asset, checks it against the digest pinned in the workflow, and
+the script fails on any other TLC version. The digest was taken from the
+asset as downloaded over TLS on 2026-11-09; tlaplus publishes no checksum
+file to compare it with. Java is the runner image's. *State:* `open`,
+until TLC comes from a Guix manifest or a pinned container.
+|===
+
 == Priority
 
-. Struct size lower bound and the safe callback wrapper (#149): small,
-  local, and they close the two gaps the modules admit to.
+. The safe callback wrapper (#149): small and local, and the last gap
+  `Foreign.idr` admits to.
 . Zig/Idris FFI agreement check: cheap, and it removes the largest
   unchecked assumption under the proofs.
 . PCC soundness: the highest-value proof, but only after the AffineScript
   port (#148) gives it something to check.
+. The provenance implementation proofs (Creusot / Pearlite and Verus on
+  `verify_entry`, `verify_witnesses`, `verify_chain`): the TLA+ model now
+  says what the protocol is worth, but not that the Rust implements it.
diff --git a/docs/PROVENANCE-EXHIBIT-B.adoc b/docs/PROVENANCE-EXHIBIT-B.adoc
index a364e1ce..fec25f57 100644
--- a/docs/PROVENANCE-EXHIBIT-B.adoc
+++ b/docs/PROVENANCE-EXHIBIT-B.adoc
@@ -102,8 +102,17 @@ real ML-DSA signatures, every metadata field, content mutations, witness
 tampering, identity binding, validity/revocation and chain deletion/splicing.
 Property tests generate arbitrary content, metadata and parent-hash mutations.
 `docs/models/Provenance.tla` models signature binding and chain verification
-symbolically. Its invariant is not a cryptographic proof of ML-DSA or SHA3,
-nor a proof of all implementation paths. Production adoption requires an
+symbolically, with an adversary that can sign under a leaked key. Its
+invariant `Genuine` says a verified chain is exactly the genuine one while
+either the author key or the witness key is uncompromised. It assumes that
+signatures cannot be made without the key and that the witness attests only
+genuine records: a witness persuaded to sign a forged record is outside the
+model. TLC checks it in CI (`provenance-model` job) with each single key
+leaked, and must find the forgery when both are. The check is bounded:
+two-record chains, built from 12 symbolic payloads (two field
+and digest values, and a parent that is one of them or `None`). Longer
+chains and larger domains are not checked. It is not a cryptographic proof of ML-DSA or SHA3,
+nor a proof of any implementation path (PROOF-NEEDS.adoc, "Exceptions"). Production adoption requires an
 approved contributor key and independent witness; historical records are
 never silently re-signed.
 
@@ -130,3 +139,6 @@ distinct states, no invariant violation. SHA-256 of the checked model:
 `c379ece2393e2cacfffccd6bb0360184ad179c77ae72dc875948a022d123444a`.
 The model assumes signature/hash binding; it is not an implementation
 correspondence proof or a cryptographic hardness proof.
+This receipt is superseded (2026-11-09): that model's invariant held by
+construction and it had no forging action. The rewritten model and its CI
+run replace it; see PROOF-NEEDS.adoc.
diff --git a/docs/models/Provenance.cfg b/docs/models/Provenance.cfg
index a67c6463..7d882d06 100644
--- a/docs/models/Provenance.cfg
+++ b/docs/models/Provenance.cfg
@@ -1,3 +1,12 @@
+\* SPDX-License-Identifier: MPL-2.0
+\* Provenance: AuthorKeyLeaked = TRUE, WitnessKeyLeaked = FALSE (see Provenance.tla).
 SPECIFICATION Spec
-CONSTANT Values = {a, b}
-INVARIANT Binding
+CONSTANTS
+  A = A
+  B = B
+  None = None
+  AuthorKeyLeaked = TRUE
+  WitnessKeyLeaked = FALSE
+INVARIANTS
+  TypeOK
+  Genuine
diff --git a/docs/models/Provenance.tla b/docs/models/Provenance.tla
index 6ac5f4e1..ebb8e59a 100644
--- a/docs/models/Provenance.tla
+++ b/docs/models/Provenance.tla
@@ -1,31 +1,107 @@
 --------------------------- MODULE Provenance ---------------------------
-EXTENDS Naturals, Sequences, FiniteSets
 \* SPDX-License-Identifier: MPL-2.0
-\* Symbolic unforgeability: an attacker may change fields/content/links or
-\* remove signatures, but cannot add a signature for a payload not signed.
-CONSTANT Values
-VARIABLES chain, authorSigned, witnessSigned, content, verified
-vars == <<chain, authorSigned, witnessSigned, content, verified>>
-Payloads == [field: Values, digest: Values, parent: Values]
-Init == /\ chain = <<>> /\ authorSigned = {} /\ witnessSigned = {}
-        /\ content = <<>> /\ verified = FALSE
-Sign == \E p \in Payloads:
-          /\ authorSigned' = authorSigned \cup {p}
-          /\ witnessSigned' = witnessSigned \cup {p}
-          /\ UNCHANGED <<chain, content, verified>>
-\* Any ordered pair, including a splice or substituted contribution.
-Supply == \E a,b \in Payloads, x,y \in Values:
-            /\ chain' = <<a,b>> /\ content' = <<x,y>>
-            /\ verified' = FALSE
-            /\ UNCHANGED <<authorSigned, witnessSigned>>
-Valid == /\ Len(chain) = 2
-         /\ \A i \in 1..2: /\ chain[i] \in authorSigned
-                             /\ chain[i] \in witnessSigned
-                             /\ chain[i].digest = content[i]
-         /\ chain[2].parent = chain[1].field
-Check == /\ verified' = Valid
-         /\ UNCHANGED <<chain, content, authorSigned, witnessSigned>>
-Next == Sign \/ Supply \/ Check
+\*
+\* Symbolic model of witnessed provenance records (EXHIBIT-B-QUANTUM-SAFE.txt,
+\* docs/PROVENANCE-EXHIBIT-B.adoc). Each record is signed by its author and
+\* attested by an independent witness. The claim checked here: a chain that
+\* verifies is exactly the genuine chain, in order, unless BOTH the author
+\* key and the witness key have leaked. One leaked key is not enough.
+\*
+\* PROOF-POLICY §4 exception (standards 3-practice/PROOF-POLICY.adoc). Full
+\* record: PROOF-NEEDS.adoc, "Exceptions", "TLA+ model of provenance binding".
+\*   Obligation: verification accepts only the genuine chain while at least
+\*     one of the two signing keys is uncompromised.
+\*   Tool: TLA+ / TLC. Why: a symbolic protocol statement. The shipped Rust is
+\*     for Creusot/Pearlite and Verus, planned and still OPEN; this model
+\*     discharges none of it.
+\*   Status: TESTED (bounded: two values, chains of two), from the
+\*     provenance-model job in build-validation.yml; see PROOF-NEEDS.adoc.
+\*   Assumed: signatures cannot be made without the key (ML-DSA-65
+\*     unforgeability), and the witness attests only genuine records.
+\*
+\* Configurations (all run in CI):
+\*   Provenance.cfg            author key leaked   -> invariants hold
+\*   ProvenanceWitnessLeak.cfg witness key leaked  -> invariants hold
+\*   ProvenanceBothLeak.cfg    both keys leaked    -> Genuine MUST be violated
+\* The third is the check that the property is not vacuous: with both keys,
+\* a forger does get a forged chain verified, and TLC must find it.
+EXTENDS Naturals, Sequences
+
+CONSTANTS A, B, None,          \* model values
+          AuthorKeyLeaked,     \* BOOLEAN
+          WitnessKeyLeaked     \* BOOLEAN
+
+Values   == {A, B}
+Payloads == [field: Values, digest: Values, parent: Values \cup {None}]
+
+\* The genuine chain: a genesis record and one record that names it.
+R1 == [field |-> A, digest |-> A, parent |-> None]
+R2 == [field |-> B, digest |-> B, parent |-> A]
+Genuine2 == <<R1, R2>>
+Intended == {R1, R2}
+
+VARIABLES chain,          \* the records presented for verification
+          content,        \* the bytes presented beside each record
+          authorSigned,   \* payloads carrying an author signature
+          witnessSigned,  \* payloads carrying a witness attestation
+          verified        \* the verifier's last verdict on (chain, content)
+vars == <<chain, content, authorSigned, witnessSigned, verified>>
+
+TypeOK ==
+  /\ chain \in Seq(Payloads) /\ Len(chain) <= 2
+  /\ content \in Seq(Values) /\ Len(content) <= 2
+  /\ authorSigned \subseteq Payloads
+  /\ witnessSigned \subseteq Payloads
+  /\ verified \in BOOLEAN
+
+\* The honest author signed the genuine records and the witness attested
+\* them; nothing else carries a signature yet.
+Init ==
+  /\ chain = <<>> /\ content = <<>>
+  /\ authorSigned = Intended
+  /\ witnessSigned = Intended
+  /\ verified = FALSE
+
+\* With a leaked key the adversary can sign any payload under it.
+ForgeAuthor ==
+  /\ AuthorKeyLeaked
+  /\ \E p \in Payloads : authorSigned' = authorSigned \cup {p}
+  /\ UNCHANGED <<chain, content, witnessSigned, verified>>
+
+ForgeWitness ==
+  /\ WitnessKeyLeaked
+  /\ \E p \in Payloads : witnessSigned' = witnessSigned \cup {p}
+  /\ UNCHANGED <<chain, content, authorSigned, verified>>
+
+\* The adversary presents any two records with any content: a splice, a
+\* reorder, a replay, a substituted contribution or a forgery.
+Supply ==
+  /\ \E r1, r2 \in Payloads, x, y \in Values :
+       /\ chain' = <<r1, r2>>
+       /\ content' = <<x, y>>
+  /\ verified' = FALSE
+  /\ UNCHANGED <<authorSigned, witnessSigned>>
+
+\* What the verifier checks (crates/provenance verify_chain): every record
+\* author-signed and witnessed, content matching its digest, and each
+\* record naming its predecessor (the first naming none).
+Valid ==
+  /\ Len(chain) = 2 /\ Len(content) = 2
+  /\ \A i \in 1..2 : /\ chain[i] \in authorSigned
+                       /\ chain[i] \in witnessSigned
+                       /\ chain[i].digest = content[i]
+  /\ chain[1].parent = None
+  /\ chain[2].parent = chain[1].field
+
+Check ==
+  /\ verified' = Valid
+  /\ UNCHANGED <<chain, content, authorSigned, witnessSigned>>
+
+Next == ForgeAuthor \/ ForgeWitness \/ Supply \/ Check
 Spec == Init /\ [][Next]_vars
-Binding == verified => Valid
+
+\* The property. It mentions the genuine chain, which the verifier never
+\* sees, so it is not the definition of Valid restated: it says what Valid
+\* is worth.
+Genuine == verified => (chain = Genuine2 /\ content = <<R1.digest, R2.digest>>)
 =============================================================================
diff --git a/docs/models/ProvenanceBothLeak.cfg b/docs/models/ProvenanceBothLeak.cfg
new file mode 100644
index 00000000..90fbf6b3
--- /dev/null
+++ b/docs/models/ProvenanceBothLeak.cfg
@@ -0,0 +1,12 @@
+\* SPDX-License-Identifier: MPL-2.0
+\* ProvenanceBothLeak: AuthorKeyLeaked = TRUE, WitnessKeyLeaked = TRUE (see Provenance.tla).
+SPECIFICATION Spec
+CONSTANTS
+  A = A
+  B = B
+  None = None
+  AuthorKeyLeaked = TRUE
+  WitnessKeyLeaked = TRUE
+INVARIANTS
+  TypeOK
+  Genuine
diff --git a/docs/models/ProvenanceWitnessLeak.cfg b/docs/models/ProvenanceWitnessLeak.cfg
new file mode 100644
index 00000000..c9631cee
--- /dev/null
+++ b/docs/models/ProvenanceWitnessLeak.cfg
@@ -0,0 +1,12 @@
+\* SPDX-License-Identifier: MPL-2.0
+\* ProvenanceWitnessLeak: AuthorKeyLeaked = FALSE, WitnessKeyLeaked = TRUE (see Provenance.tla).
+SPECIFICATION Spec
+CONSTANTS
+  A = A
+  B = B
+  None = None
+  AuthorKeyLeaked = FALSE
+  WitnessKeyLeaked = TRUE
+INVARIANTS
+  TypeOK
+  Genuine
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index a639b84e..597ae4ea 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -6,12 +6,14 @@ Schema: hyperpolymath/standards
 soundness-relevant escape hatch and its disposition. What PanLL proves, and
 what it still needs to prove, is in link:../PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`].
 
-Last reconciled: 2026-10-26 (`main` at `1937c6b`).
+Last reconciled: 2026-11-09 (`main` at `7d1feaa`).
 
 * *Idris2* (`panel-clades/src/abi/`): no `believe_me`, `assert_total`,
-  `assert_smaller`, `idris_crash`, `unsafePerformIO`, `postulate` or holes,
-  measured on the date above. `check-abi.sh` fails CI if any of those six
-  keywords appears; it does not scan for holes.
+  `assert_smaller`, `idris_crash`, `unsafePerformIO`, `postulate`,
+  `partial`, `covering` or holes, measured on the date above. `check-abi.sh`
+  fails CI if any of them appears in code (comments and string literals set
+  aside, string interpolations scanned) or a module lacks `%default total` before its first declaration, in PanLL's modules and in the
+  typed-wasm modules they import (the import cone).
 * *Estate check*: standards' `scripts/check-trusted-base.sh` finds 2
   escape-hatch signatures, both documented below as not proof debt.
 * *Rust*: the estate check does not scan Rust. The `unsafe` blocks and
@@ -38,6 +40,10 @@ declaration, at an FFI or system-call boundary. None is annotated with
 `// TRUSTED:`, and none has a stated test budget, so none qualifies as (b)
 yet.
 
+The verifier for these seams is Kani, under PROOF-POLICY §4.1, alongside
+Creusot / Pearlite and Verus. The obligations are listed in
+link:../PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`]; none has been run.
+
 *Owner*: @hyperpolymath. *Deadline*: INDEFINITE — the disposition of each
 group (annotate and budget as (b), or remove the `unsafe`) is an owner
 decision. *Plan* for each: add a `// TRUSTED: <kind>; <budget>` annotation
@@ -53,6 +59,12 @@ and the test that sets the budget, then move the entry to (b).
 * `src-gossamer/src/coprocessor/mod.rs:114`, `:117`, `:120`, `:123` — the
   `unsafe extern "C" fn` types for those symbols. These are declarations;
   they share the entry above.
+* `src-gossamer/src/main.rs:203`, `:209` — the event pump: `gossamer_emit`
+  delivers queued backend events to the webview, and `g_timeout_add`
+  schedules the pump on the GTK main loop. The `extern "C"` declarations
+  they call are at `:175` and `:177`.
+** *Kind*: extraction boundary (Rust → Gossamer C ABI, and GLib). Both have
+   a `SAFETY` comment. Added by #164.
 * `src-gossamer/src/llm_coding/commands.rs:197`, `:217`, `:237` —
   `libc::kill` sending `SIGSTOP` / `SIGCONT` / `SIGTERM` to a session's
   process.
diff --git a/panel-clades/scripts/abi-scan-lib.sh b/panel-clades/scripts/abi-scan-lib.sh
new file mode 100644
index 00000000..9e528790
--- /dev/null
+++ b/panel-clades/scripts/abi-scan-lib.sh
@@ -0,0 +1,129 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# abi-scan-lib.sh — the source scans behind check-abi.sh, sourced by it and
+# by tests/scan/test-abi-scan.sh.  Every scan reads code only: comments and
+# string literals are set aside first, so prose such as "NO believe_me" does
+# not trip a scan, and a directive or import inside a comment does not count.
+
+# Print each .idr file's code with comments and string literals blanked, as
+# FILE:LINE:TEXT.  Handles nested {- -} block comments, `--` line comments
+# (not operators such as -->), `|||` doc comments, "..." strings, raw
+# strings #"..."# (any number of #, where \ is not an escape), multi-line
+# """...""" strings, and character literals including escapes ('\'',
+# '\"', '\x41').  A primed identifier (f') does not open a literal.
+# Interpolations are code, not text: \{...} in a string (\#{...} in a raw
+# string opened with one #, and so on) is kept and scanned, to its
+# matching }, with strings nested inside it handled the same way.
+code_only() {
+  awk '
+    FNR == 1 { depth = 0; term = ""; ml = 0; sp = 0 }
+    {
+      line = $0; out = ""; i = 1; n = length(line)
+      if (depth == 0 && term == "" && sp == 0 && line ~ /^[[:space:]]*\|\|\|/) { print FILENAME ":" FNR ":"; next }
+      while (i <= n) {
+        if (term != "") {
+          if (substr(line, i, 1) == "\\" && substr(line, i + 1, length(hk) + 1) == hk "{") {
+            sp++; st[sp] = term; se[sp] = esc; sm[sp] = ml; sh[sp] = hk; sb[sp] = 0
+            term = ""; i += length(hk) + 2; out = out " "; continue
+          }
+          if (esc && substr(line, i, 1) == "\\") { i += 2; continue }
+          if (substr(line, i, length(term)) == term) { i += length(term); term = ""; ml = 0; continue }
+          i++; continue
+        }
+        two = substr(line, i, 2); c = substr(line, i, 1)
+        if (two == "{-") { depth++; i += 2; continue }
+        if (depth > 0) { if (two == "-}") { depth--; i += 2 } else i++; continue }
+        if (two == "--" && substr(line, i + 2, 1) !~ /[!#$%&*+.\/<=>?@\\^|~:-]/) break
+        k = 0; while (substr(line, i + k, 1) == "#") k++
+        if (substr(line, i + k, 1) == "\"") {
+          hk = substr(line, i, k)
+          if (substr(line, i + k, 3) == "\"\"\"") { term = "\"\"\"" hk; ml = 1; i += k + 3 }
+          else { term = "\"" hk; ml = 0; i += k + 1 }
+          esc = (k == 0); out = out "\"\""; continue
+        }
+        if (c == SQ && (i == 1 || substr(line, i - 1, 1) !~ /[A-Za-z0-9_]/ && substr(line, i - 1, 1) != SQ)) {
+          if (substr(line, i + 1, 1) == "\\") {
+            j = i + 3; while (j <= n && j < i + 12 && substr(line, j, 1) != SQ) j++
+            if (substr(line, j, 1) == SQ) { i = j + 1; out = out SQ SQ; continue }
+          } else if (substr(line, i + 2, 1) == SQ) { i += 3; out = out SQ SQ; continue }
+        }
+        if (sp > 0 && c == "{") { sb[sp]++; out = out c; i++; continue }
+        if (sp > 0 && c == "}") {
+          if (sb[sp] > 0) { sb[sp]--; out = out c; i++; continue }
+          term = st[sp]; esc = se[sp]; ml = sm[sp]; hk = sh[sp]; sp--; out = out " "; i++; continue
+        }
+        out = out c; i++
+      }
+      if (term != "" && !ml) term = ""
+      if (sp > 0 && !sm[1]) sp = 0
+      print FILENAME ":" FNR ":" out
+    }' SQ="'" "$@"
+}
+
+# Escape hatches and holes in code, plus any module whose code does not
+# declare `%default total` before its first declaration (Idris2's default is
+# `covering`, which does not check termination, and %default applies only
+# from where it appears; a directive inside a comment does not count).
+# Returns 0 and prints the offending lines if anything is found.
+#   believe_me assert_total assert_smaller idris_crash unsafePerformIO
+#   postulate             -- trust or totality escapes
+#   ?name                 -- a hole: idris2 --build accepts a module with holes
+#                            (a ? after an operator character is part of
+#                            that operator, as in a =?b, not a hole)
+#   partial / covering    -- a declaration opting out of %default total
+scan_escapes() {
+  local found=1 f
+  if code_only "$@" | grep -E \
+       -e ':[0-9]+:.*\b(believe_me|assert_total|assert_smaller|idris_crash|unsafePerformIO|postulate)\b' \
+       -e ':[0-9]+:(.*[^A-Za-z0-9_'"'"'?!#$%&*+./<=>@\^|~:-])?\?[A-Za-z_][A-Za-z0-9_'"'"']*' \
+       -e ':[0-9]+:.*\b(partial|covering)\b'; then
+    found=0
+  fi
+  # Only the module header, imports and other % directives may precede it.
+  # The awk reads to the end: exiting early would SIGPIPE code_only, which
+  # pipefail reads as a missing directive.
+  for f in "$@"; do
+    if ! code_only "$f" | awk '
+        done { next }
+        { t = $0; sub(/^[^:]*:[0-9]+:/, "", t) }
+        t ~ /^[[:space:]]*%default[[:space:]]+total[[:space:]]*$/ { ok = 1; done = 1; next }
+        t ~ /^[[:space:]]*$/ || t ~ /^[[:space:]]*(module|import)([[:space:]]|$)/ || t ~ /^[[:space:]]*%/ { next }
+        { done = 1 }
+        END { exit !ok }'; then
+      printf '%s: no %%default total before the first declaration\n' "$f"; found=0
+    fi
+  done
+  return "$found"
+}
+
+# import_cone BASE_FILE ROOT... -- FILE...
+# The modules the given files import, transitively, that resolve to a source
+# file under one of the roots, one path per line (the files themselves
+# first).  Imports are read from code only, at any indentation.  Imports
+# that resolve under no root are written as module names to BASE_FILE, which
+# is cleared first.  These may include Idris2's prelude/base/contrib modules.
+import_cone() {
+  local base="$1"; shift
+  local -a roots=() queue=() seen=()
+  while [[ $# -gt 0 && "$1" != "--" ]]; do roots+=("$1"); shift; done
+  [[ $# -gt 0 ]] && shift
+  queue=("$@")
+  local f m r p hit
+  : > "$base"
+  while [[ ${#queue[@]} -gt 0 ]]; do
+    f="${queue[0]}"; queue=("${queue[@]:1}")
+    case " ${seen[*]-} " in *" $f "*) continue ;; esac
+    seen+=("$f"); printf '%s\n' "$f"
+    while IFS= read -r m; do
+      hit=""
+      for r in "${roots[@]}"; do
+        p="$r/${m//.//}.idr"
+        if [[ -f "$p" ]]; then hit="$p"; break; fi
+      done
+      if [[ -n "$hit" ]]; then queue+=("$hit"); else printf '%s\n' "$m" >> "$base"; fi
+    done < <(code_only "$f" \
+      | sed -nE 's/^[^:]*:[0-9]+:[[:space:]]*import[[:space:]]+(public[[:space:]]+)?([A-Za-z0-9_.]+).*/\2/p')
+  done
+}
diff --git a/panel-clades/scripts/check-abi.sh b/panel-clades/scripts/check-abi.sh
index 9a189b21..f979a5bd 100755
--- a/panel-clades/scripts/check-abi.sh
+++ b/panel-clades/scripts/check-abi.sh
@@ -16,7 +16,10 @@
 #
 # A missing toolchain is a failure, never a skip.  Every module under
 # src/abi/PanelClades/ must be listed in the ipkg (an unlisted one would be
-# skipped silently), and none may use an escape hatch.
+# skipped silently), declare `%default total` before its first declaration
+# (the directive applies only from where it appears), and use no escape hatch and no
+# hole; the typed-wasm modules they import (the import cone) are held to the
+# same scan, and the cone is printed as the run's record of it.
 set -uo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 1
 ROOT="$(pwd)"
@@ -30,9 +33,14 @@ err()  { printf 'FAIL: %s\n' "$1"; fail=1; }
 # Print the supplied failure message and terminate the gate with exit status 1.
 die()  { printf 'FAIL: %s\n' "$1"; exit 1; }
 
+# The scans (code_only, scan_escapes, import_cone) live in abi-scan-lib.sh,
+# which tests/scan/test-abi-scan.sh exercises both ways.
+# shellcheck source=abi-scan-lib.sh
+. scripts/abi-scan-lib.sh
+
 command -v idris2 >/dev/null || die "idris2 not on PATH (a gate that cannot run must not report OK)"
 iv="$(idris2 --version)"; echo "$iv"
-case "$iv" in *"version 0.8.0"*) ;; *) [ -n "${ALLOW_ANY_IDRIS2:-}" ] || die "Idris2 0.8.0 required (set ALLOW_ANY_IDRIS2=1 to try another)" ;; esac
+case "$iv" in *"version 0.8.0"*) ;; *) [[ -n "${ALLOW_ANY_IDRIS2:-}" ]] || die "Idris2 0.8.0 required (set ALLOW_ANY_IDRIS2=1 to try another)" ;; esac
 rm -rf "$OUT"; mkdir -p "$OUT"
 
 IPKG="src/abi/panel-clades-grades.ipkg"
@@ -41,16 +49,16 @@ abi_list="$OUT/abi-files"
 find src/abi/PanelClades -type f -name '*.idr' -print0 > "$abi_list" \
   || die "could not enumerate .idr files under src/abi/PanelClades"
 mapfile -d '' -t abi_files < "$abi_list"
-[ "${#abi_files[@]}" -gt 0 ] || die "no .idr files found under src/abi/PanelClades"
+[[ "${#abi_files[@]}" -gt 0 ]] || die "no .idr files found under src/abi/PanelClades"
 for f in "${abi_files[@]}"; do
   mod="$(printf '%s' "${f#src/abi/}" | sed 's|\.idr$||; s|/|.|g')"
   grep -qE "^[[:space:]]*(modules[[:space:]]*=|,)[[:space:]]*${mod//./\\.}[[:space:]]*$" "$IPKG" \
     || err "$mod is not listed in $IPKG (it would never be checked)"
 done
-if grep -nE '\b(believe_me|assert_total|assert_smaller|idris_crash|unsafePerformIO|postulate)\b' "${abi_files[@]}"; then
+if scan_escapes "${abi_files[@]}"; then
   err "escape hatch in src/abi/PanelClades (lines above)"
 fi
-[ "$fail" -eq 0 ] && pass "every PanelClades module is listed in the ipkg; no escape hatches"
+[[ "$fail" -eq 0 ]] && pass "every PanelClades module is listed in the ipkg, declares %default total, and has no escape hatch or hole"
 if bash scripts/gen-budgets.sh --check; then
   pass "Budgets.idr is current with the clade configs"
 else
@@ -68,10 +76,23 @@ fi
 pass "typed-wasm grade kernel built at $(git -C _build/dependencies/typed-wasm rev-parse --short HEAD)"
 KTTC="$ROOT/$TW/build/ttc"
 
+# The import cone (standards PROOF-POLICY §1.1): every first-party module the
+# proofs rest on, PanelClades and typed-wasm alike, is held to the same scan.
+# A kernel module with a hole or an escape hatch would be trusted silently.
+import_cone "$OUT/import-base" src/abi "$TW" -- "${abi_files[@]}" > "$OUT/import-cone"
+mapfile -t cone < <(grep -v '^src/abi/PanelClades/' "$OUT/import-cone")
+[[ "${#cone[@]}" -gt 0 ]] || die "import cone has no typed-wasm module; Grades.idr imports the kernel"
+if scan_escapes "${cone[@]}"; then
+  err "escape hatch or hole in the typed-wasm import cone (lines above)"
+else
+  pass "import cone: ${#cone[@]} typed-wasm module(s), no escape hatch or hole; base: $(sort -u "$OUT/import-base" | tr '\n' ' ')"
+fi
+sed 's/^/  cone: /' "$OUT/import-cone"
+
 rm -rf src/abi/build
 (cd src/abi && IDRIS2_PATH="$KTTC" idris2 --build panel-clades-grades.ipkg) > "$OUT/grades.log" 2>&1
 st=$?
-if [ "$st" -eq 0 ] && ! grep -q '^Error' "$OUT/grades.log"; then
+if [[ "$st" -eq 0 ]] && ! grep -q '^Error' "$OUT/grades.log"; then
   pass "panel-clades-grades.ipkg builds against the kernel ($(grep -c ': Building ' "$OUT/grades.log") module(s), 0 errors)"
 else
   { grep -A12 '^Error' "$OUT/grades.log" || tail -40 "$OUT/grades.log"; } | head -40
@@ -81,21 +102,21 @@ PTTC="$ROOT/src/abi/build/ttc"
 
 n=0
 for f in tests/reject/*.idr; do
-  [ -e "$f" ] || { err "no tests/reject/*.idr fixtures"; break; }
+  [[ -e "$f" ]] || { err "no tests/reject/*.idr fixtures"; break; }
   n=$((n + 1)); name="$(basename "$f" .idr)"
   expect="$(sed -n 's/^-- EXPECT: //p' "$f" | head -1)"
   decl="$(grep -nE '^invalid[[:space:]]*:' "$f" | head -1 | cut -d: -f1)"
   log="$OUT/reject-$name.log"
   (cd tests/reject && IDRIS2_PATH="$KTTC:$PTTC" idris2 --build-dir "$ROOT/$OUT/reject-build" --check "$name.idr") > "$log" 2>&1
   loc="$(grep -oE "^${name}:[0-9]+:" "$log" | head -1 | cut -d: -f2)"
-  if [ -z "$expect" ] || [ -z "$decl" ]; then err "reject $name: no '-- EXPECT:' line or 'invalid :' declaration"
+  if [[ -z "$expect" ]] || [[ -z "$decl" ]]; then err "reject $name: no '-- EXPECT:' line or 'invalid :' declaration"
   elif ! grep -q '^Error' "$log"; then cat "$log"; err "reject $name: ACCEPTED"
   elif grep -qE "$WRONG_REASON" "$log"; then cat "$log"; err "reject $name: refused for the WRONG reason"
-  elif [ -z "$loc" ] || [ "$loc" -lt "$decl" ]; then cat "$log"; err "reject $name: error not at its invalid declaration"
+  elif [[ -z "$loc" ]] || [[ "$loc" -lt "$decl" ]]; then cat "$log"; err "reject $name: error not at its invalid declaration"
   elif ! grep -qE -- "$expect" "$log"; then cat "$log"; err "reject $name: not refused with: $expect"
   else pass "rejected $name at line $loc ($expect)"; fi
 done
 
 echo
-[ "$fail" -eq 0 ] || { echo "PANEL-CLADES ABI CHECK FAILED"; exit 1; }
+[[ "$fail" -eq 0 ]] || { echo "PANEL-CLADES ABI CHECK FAILED"; exit 1; }
 echo "OK: panel-clades ABI — builds against the kernel, ${n} rejection(s)"
diff --git a/panel-clades/src/abi/PanelClades/ABI/Layout.idr b/panel-clades/src/abi/PanelClades/ABI/Layout.idr
index 0163ea50..f0858de3 100644
--- a/panel-clades/src/abi/PanelClades/ABI/Layout.idr
+++ b/panel-clades/src/abi/PanelClades/ABI/Layout.idr
@@ -6,28 +6,90 @@
 ||| Alignment and struct layout for the C-compatible structs of the
 ||| panel-clades ABI.
 |||
-||| What is proved: rounding up to an alignment always lands on a multiple
-||| of it (`alignUpCorrect`, by construction), every computed struct size
-||| is a multiple of its alignment (`calcStructSizeAligned`), and every
-||| `Divides` / `FieldsAligned` witness is a real equation.  Field
-||| alignment is decided by an equation on Nat (`decDivides`), not by a
-||| Boolean test followed by an unproved `Refl`.
+||| What is proved:
 |||
-||| What is NOT proved: that a computed size is at least the end of the
-||| last field.  `verifyLayout` checks that at run time, and refuses a
-||| layout that fails it.
+|||   * rounding up to an alignment a ≥ 1 is tight: it lands on a multiple
+|||     of a (`alignUpCorrect`), at or above the size (`alignUpCovers`) and
+|||     below size + a (`alignUpTight`);
+|||   * a computed struct size is a multiple of its alignment
+|||     (`calcStructSizeAligned`) and covers every field
+|||     (`calcStructSizeCovers`, `fieldWithinStruct`), so `verifyLayout`
+|||     needs no run-time size check;
+|||   * C layout evidence (`CABICompliant`) carries, for every field, an
+|||     offset that is a multiple of its alignment (`FieldsAligned`), at
+|||     least one field, the first at offset 0 (`FirstAtZero`), fields in
+|||     order and not overlapping (`FieldsOrdered`), alignments that are
+|||     powers of two (`AlignmentsPow2`), and a struct alignment equal to
+|||     the largest field alignment (`maxAlignment`).  Each is decided by an
+|||     equation or an `LTE` proof, never by a Boolean test followed by an
+|||     unproved `Refl`.
+|||
+||| What is NOT proved: that a Zig or C compiler lays a struct out this way.
+||| The evidence says a layout follows the C rules; matching the Zig side is
+||| a separate check (PROOF-NEEDS.adoc, "Zig/Idris FFI agreement").
 |||
 ||| @see https://en.wikipedia.org/wiki/Data_structure_alignment
 
 module PanelClades.ABI.Layout
 
 import PanelClades.ABI.Types
+import Data.Either
 import Data.List
+import Data.List.Elem
+import Data.Nat
 import Data.So
 import Decidable.Equality
 
 %default total
 
+--------------------------------------------------------------------------------
+-- Nat lemmas (local, so this module imports nothing beyond base)
+--------------------------------------------------------------------------------
+
+||| Every natural number is less than or equal to itself.
+lteR : (n : Nat) -> LTE n n
+lteR Z     = LTEZero
+lteR (S n) = LTESucc (lteR n)
+
+||| Compose two less-than-or-equal proofs.
+lteT : LTE a b -> LTE b c -> LTE a c
+lteT LTEZero     _           = LTEZero
+lteT (LTESucc p) (LTESucc q) = LTESucc (lteT p q)
+
+||| Substitute an equal lower bound in a less-than-or-equal proof.
+lteEqL : a = b -> LTE b c -> LTE a c
+lteEqL Refl p = p
+
+||| Substitute an equal upper bound in a less-than-or-equal proof.
+lteEqR : LTE a b -> b = c -> LTE a c
+lteEqR p Refl = p
+
+||| k - u never exceeds k.
+minusLteSelf : (k, u : Nat) -> LTE (k `minus` u) k
+minusLteSelf Z     _     = LTEZero
+minusLteSelf (S k) Z     = lteR (S k)
+minusLteSelf (S k) (S u) = lteSuccRight (minusLteSelf k u)
+
+||| k fits in u plus what k has left over u.
+lteMinusPlus : (k, u : Nat) -> LTE k (u + (k `minus` u))
+lteMinusPlus Z     _     = LTEZero
+lteMinusPlus (S k) Z     = lteR (S k)
+lteMinusPlus (S k) (S u) = LTESucc (lteMinusPlus k u)
+
+||| When k ≤ u, k - u is 0.
+minusLteZero : (k, u : Nat) -> LTE k u -> k `minus` u = Z
+minusLteZero Z     _     _           = Refl
+minusLteZero (S k) (S u) (LTESucc p) = minusLteZero k u p
+minusLteZero (S _) Z     LTEZero impossible
+
+||| Adding back what was taken off.
+addBack : (u, k, t : Nat) -> LTE u k -> u + ((k `minus` u) + t) = k + t
+addBack u k t le =
+  rewrite plusAssociative u (k `minus` u) t in
+  rewrite plusCommutative u (k `minus` u) in
+  rewrite plusMinusLte u k le in
+  Refl
+
 --------------------------------------------------------------------------------
 -- Alignment Utilities
 --------------------------------------------------------------------------------
@@ -69,11 +131,54 @@ paddingFor offset alignment = alignUp offset alignment `minus` offset
 
 ||| `alignUp` always produces a multiple of the alignment.  This holds by
 ||| construction (alignUp is defined as units × alignment), for every
-||| alignment including 0.
+||| alignment including 0.  `alignUpCovers` and `alignUpTight` are the
+||| properties that carry weight.
 public export
 alignUpCorrect : (size : Nat) -> (align : Nat) -> Divides align (alignUp size align)
 alignUpCorrect size align = DivideBy (alignUnits size align) Refl
 
+||| With enough fuel, the units cover the size.
+unitsCover : (fuel, size, u : Nat) -> LTE size fuel
+          -> LTE size (unitsFor fuel size (S u) * S u)
+unitsCover _     Z     _ _   = LTEZero
+unitsCover Z     (S k) _ prf = void (succNotLTEzero prf)
+unitsCover (S f) (S k) u prf =
+  let ih = unitsCover f (k `minus` u) u (lteT (minusLteSelf k u) (fromLteSucc prf))
+  in LTESucc (lteT (lteMinusPlus k u) (plusLteMonotoneLeft u _ _ ih))
+
+||| Units for nothing are none, whatever the fuel.
+unitsZero : (fuel, unit : Nat) -> unitsFor fuel Z unit = Z
+unitsZero Z     _ = Refl
+unitsZero (S _) _ = Refl
+
+||| With enough fuel, the units overshoot the size by less than one unit.
+unitsTight : (fuel, size, u : Nat) -> LTE size fuel
+          -> LT (unitsFor fuel size (S u) * S u) (size + S u)
+unitsTight Z     Z     _ _   = LTESucc LTEZero
+unitsTight (S _) Z     _ _   = LTESucc LTEZero
+unitsTight Z     (S k) _ prf = void (succNotLTEzero prf)
+unitsTight (S f) (S k) u prf with (isLTE u k)
+  _ | Yes le =
+    let ih   = unitsTight f (k `minus` u) u (lteT (minusLteSelf k u) (fromLteSucc prf))
+        step = plusLteMonotoneLeft u _ _ ih
+    in LTESucc (lteEqL (plusSuccRightSucc u _) (lteEqR step (addBack u k (S u) le)))
+  _ | No gt =
+    rewrite minusLteZero k u (lteSuccLeft (notLTEImpliesGT gt)) in
+    rewrite unitsZero f (S u) in
+    LTESucc (lteEqL (cong S (plusZeroRightNeutral u))
+                    (lteEqR (lteAddRight (S u)) (plusCommutative (S u) k)))
+
+||| Rounding up to an alignment of at least 1 never lands below the size.
+export
+alignUpCovers : (size, u : Nat) -> LTE size (alignUp size (S u))
+alignUpCovers size u = unitsCover size size u (lteR size)
+
+||| Rounding up to an alignment a ≥ 1 adds less than a: it is the least
+||| multiple of a at or above the size.
+export
+alignUpTight : (size, u : Nat) -> LT (alignUp size (S u)) (size + S u)
+alignUpTight size u = unitsTight size size u (lteR size)
+
 ||| Decide whether n divides m, returning the witness when it does.  The
 ||| candidate quotient is the ceiling quotient (equal to the exact one
 ||| whenever n divides m), then the equation is checked with Nat's
@@ -86,6 +191,25 @@ decDivides n m =
     Yes prf => Just (DivideBy (alignUnits m n) prf)
     No _    => Nothing
 
+||| `n` is a power of two: 1, or twice a power of two.
+public export
+data IsPow2 : Nat -> Type where
+  Pow2One    : IsPow2 1
+  Pow2Double : IsPow2 n -> IsPow2 (n + n)
+
+||| Decide whether n is a power of two by doubling from 1.  A `Just`
+||| always carries a real `IsPow2` witness; `Nothing` means "not shown".
+||| n + 1 doublings are more than enough fuel.
+public export
+decPow2 : (n : Nat) -> Maybe (IsPow2 n)
+decPow2 n = go (S n) 1 Pow2One
+  where
+    go : (fuel : Nat) -> (p : Nat) -> IsPow2 p -> Maybe (IsPow2 n)
+    go Z     _ _  = Nothing
+    go (S f) p pf = case decEq p n of
+      Yes same => Just (replace {p = IsPow2} same pf)
+      No _     => if lte p n then go f (p + p) (Pow2Double pf) else Nothing
+
 --------------------------------------------------------------------------------
 -- Struct Field Layout
 --------------------------------------------------------------------------------
@@ -110,9 +234,19 @@ nextFieldOffset : Field -> Nat
 nextFieldOffset f = alignUp (fieldEnd f) f.alignment
 
 ||| The greatest field end offset in bytes, or 0 for an empty list.
+||| (Structural, with Data.Nat's `maximum`, so the lemmas below can reason
+||| about it; it computes the same value as the earlier `max` fold.)
 public export
 structEnd : List Field -> Nat
-structEnd = foldr (\f, acc => max (fieldEnd f) acc) 0
+structEnd []        = 0
+structEnd (f :: fs) = maximum (fieldEnd f) (structEnd fs)
+
+||| Every field ends at or before the struct's last field end.
+export
+fieldWithinEnd : (fs : List Field) -> Elem f fs -> LTE (fieldEnd f) (structEnd fs)
+fieldWithinEnd (f :: fs) Here      = maximumLeftUpperBound (fieldEnd f) (structEnd fs)
+fieldWithinEnd (g :: fs) (There e) =
+  lteT (fieldWithinEnd fs e) (maximumRightUpperBound (fieldEnd g) (structEnd fs))
 
 ||| Total struct size: the furthest field end, rounded up to the struct's
 ||| alignment.  (Fields carry explicit offsets, so this is the C rule; the
@@ -129,7 +263,14 @@ calcStructSizeAligned : (fields : List Field) -> (align : Nat)
                      -> Divides align (calcStructSize fields align)
 calcStructSizeAligned fields align = alignUpCorrect (structEnd fields) align
 
-||| A struct layout: its fields, its size and alignment, a check that the
+||| With an alignment of at least 1, the computed struct size covers every
+||| field.
+export
+calcStructSizeCovers : (fields : List Field) -> (u : Nat)
+                    -> LTE (structEnd fields) (calcStructSize fields (S u))
+calcStructSizeCovers fields u = alignUpCovers (structEnd fields) u
+
+||| A struct layout: its fields, its size and alignment, a proof that the
 ||| size covers the fields, and a proof that the size is a multiple of the
 ||| alignment.
 public export
@@ -138,9 +279,15 @@ record StructLayout where
   fields : List Field
   totalSize : Nat
   alignment : Nat
-  {auto 0 sizeCorrect : So (totalSize >= structEnd fields)}
+  0 covers : LTE (structEnd fields) totalSize
   0 aligned : Divides alignment totalSize
 
+||| Every field of a layout lies within its total size.
+export
+0 fieldWithinStruct : (layout : StructLayout) -> Elem f layout.fields
+                   -> LTE (fieldEnd f) layout.totalSize
+fieldWithinStruct layout e = lteT (fieldWithinEnd layout.fields e) layout.covers
+
 ||| Proof that every field's offset is a multiple of its alignment
 public export
 data FieldsAligned : List Field -> Type where
@@ -152,29 +299,66 @@ data FieldsAligned : List Field -> Type where
     FieldsAligned rest ->
     FieldsAligned (f :: rest)
 
-||| Build a layout whose size is computed from its fields; refused when
-||| the computed size does not cover them.
-||| Returns Right with the layout, or Left "Invalid struct size".
-||| Field offsets are checked separately by `checkCABI`.
+||| Build a layout whose size is computed from its fields.  The size is
+||| proved to cover the fields and to be a multiple of the alignment, so
+||| the only refusal is an alignment of 0, which no C type has.
+||| Field offsets and the C rules are checked separately by `checkCABI`.
 public export
 verifyLayout : (fields : List Field) -> (align : Nat) -> Either String StructLayout
-verifyLayout fields align =
-  case choose (calcStructSize fields align >= structEnd fields) of
-    Left covers =>
-      Right (MkStructLayout fields (calcStructSize fields align) align
-               {sizeCorrect = covers} (calcStructSizeAligned fields align))
-    Right _ => Left "Invalid struct size"
+verifyLayout _      Z     = Left "Alignment 0 is not a C alignment"
+verifyLayout fields (S u) =
+  Right (MkStructLayout fields (calcStructSize fields (S u)) (S u)
+           (calcStructSizeCovers fields u) (calcStructSizeAligned fields (S u)))
 
 --------------------------------------------------------------------------------
 -- C ABI Compatibility
 --------------------------------------------------------------------------------
 
-||| Proof that a struct follows C ABI rules (every field aligned)
+||| The struct has at least one field, and the first starts at offset 0.
+||| A C struct needs a member (C11 6.7.2.1p8: one with no named member is
+||| undefined), and C allows padding between members and after the last,
+||| never before the first (6.7.2.1p15).  There is no evidence for `[]`.
+public export
+data FirstAtZero : List Field -> Type where
+  ZeroHead : f.offset = 0 -> FirstAtZero (f :: rest)
+
+||| Fields in declaration order, each starting at or after the end of the
+||| one before, so no two overlap.
+public export
+data FieldsOrdered : List Field -> Type where
+  OrdNil  : FieldsOrdered []
+  OrdOne  : FieldsOrdered [f]
+  OrdCons : LTE (fieldEnd f) g.offset -> FieldsOrdered (g :: rest)
+         -> FieldsOrdered (f :: g :: rest)
+
+||| Every field's alignment is a power of two.
+public export
+data AlignmentsPow2 : List Field -> Type where
+  Pow2Nil  : AlignmentsPow2 []
+  Pow2Cons : IsPow2 f.alignment -> AlignmentsPow2 rest -> AlignmentsPow2 (f :: rest)
+
+||| The largest field alignment in bytes, with a minimum of 1 (also for an
+||| empty list or fields whose alignments are all 0).
+public export
+maxAlignment : List Field -> Nat
+maxAlignment []        = 1
+maxAlignment (f :: fs) = maximum f.alignment (maxAlignment fs)
+
+||| Proof that a struct follows the C layout rules: every field offset is
+||| a multiple of its alignment, there is a field and the first is at
+||| offset 0, the fields are in order and do not overlap, every alignment is
+||| a power of two, and the struct is aligned to its largest field
+||| alignment.  (Size covering the fields, and being a
+||| multiple of the alignment, are carried by `StructLayout` itself.)
 public export
 data CABICompliant : StructLayout -> Type where
   CABIOk :
     (layout : StructLayout) ->
     FieldsAligned layout.fields ->
+    FirstAtZero layout.fields ->
+    FieldsOrdered layout.fields ->
+    AlignmentsPow2 layout.fields ->
+    layout.alignment = maxAlignment layout.fields ->
     CABICompliant layout
 
 ||| Attempt to prove all fields are correctly aligned.  Returns `Left`
@@ -192,14 +376,63 @@ proveFieldsAligned (f :: rest) =
         Left err => Left err
         Right restProof => Right (ConsField f rest here restProof)
 
-||| Return a proof that every field offset is a multiple of its alignment,
-||| or propagate the first field-alignment error from `proveFieldsAligned`.
+||| Attempt to prove there is a field and the first is at offset 0.
+||| Returns `Left` for an empty list or a non-zero first offset.
+public export
+proveFirstAtZero : (fields : List Field) -> Either String (FirstAtZero fields)
+proveFirstAtZero []       = Left "A C struct needs at least one member"
+proveFirstAtZero (f :: _) =
+  case decEq f.offset 0 of
+    No _    => Left ("First field " ++ f.name ++ " is at offset "
+                     ++ show f.offset ++ ", not 0")
+    Yes zero => Right (ZeroHead zero)
+
+||| Attempt to prove the fields are in order and do not overlap.  Returns
+||| `Left` naming the first field that starts before the previous one ends.
+public export
+proveFieldsOrdered : (fields : List Field) -> Either String (FieldsOrdered fields)
+proveFieldsOrdered []  = Right OrdNil
+proveFieldsOrdered [_] = Right OrdOne
+proveFieldsOrdered (f :: g :: rest) =
+  case isLTE (fieldEnd f) g.offset of
+    No _    => Left ("Field " ++ g.name ++ " at offset " ++ show g.offset
+                     ++ " overlaps " ++ f.name ++ ", which ends at "
+                     ++ show (fieldEnd f))
+    Yes fit =>
+      case proveFieldsOrdered (g :: rest) of
+        Left err => Left err
+        Right restProof => Right (OrdCons fit restProof)
+
+||| Attempt to prove every field alignment is a power of two.  Returns
+||| `Left` naming the first field whose alignment is not shown to be one.
+public export
+proveAlignmentsPow2 : (fields : List Field) -> Either String (AlignmentsPow2 fields)
+proveAlignmentsPow2 [] = Right Pow2Nil
+proveAlignmentsPow2 (f :: rest) =
+  case decPow2 f.alignment of
+    Nothing => Left ("Field " ++ f.name ++ " has alignment "
+                     ++ show f.alignment ++ ", not a power of two")
+    Just p =>
+      case proveAlignmentsPow2 rest of
+        Left err => Left err
+        Right restProof => Right (Pow2Cons p restProof)
+
+||| Return C layout evidence, or the first error encountered while checking
+||| field alignment, the first offset, field order, power-of-two alignments
+||| and struct alignment, in that order.  A field alignment error means the
+||| required evidence was not found.
 public export
 checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
-checkCABI layout =
-  case proveFieldsAligned layout.fields of
-    Right prf => Right (CABIOk layout prf)
-    Left err => Left err
+checkCABI layout = do
+  aligned <- proveFieldsAligned layout.fields
+  first   <- proveFirstAtZero layout.fields
+  ordered <- proveFieldsOrdered layout.fields
+  pow2    <- proveAlignmentsPow2 layout.fields
+  case decEq layout.alignment (maxAlignment layout.fields) of
+    No _ => Left ("Struct alignment " ++ show layout.alignment
+                  ++ " is not the largest field alignment "
+                  ++ show (maxAlignment layout.fields))
+    Yes same => Right (CABIOk layout aligned first ordered pow2 same)
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -219,7 +452,7 @@ verifyAllPlatforms :
   Either String ()
 verifyAllPlatforms layouts = go allPlatforms
   where
-    ||| Check the remaining platforms, stopping at the first alignment error.
+    ||| Check the remaining platforms, stopping at the first C-rule error.
     go : List Platform -> Either String ()
     go [] = Right ()
     go (p :: ps) = case checkCABI (layouts p) of
@@ -230,6 +463,13 @@ verifyAllPlatforms layouts = go allPlatforms
 -- Example Layouts
 --------------------------------------------------------------------------------
 
+||| An LTE proof found by evaluation, for closed numbers: `lte m n`
+||| reduces, so the `So` is found automatically, and numbers that do not
+||| fit have no `So True` and fail the typecheck at the use site.
+public export
+fitsIn : (m, n : Nat) -> {auto ok : So (lte m n)} -> LTE m n
+fitsIn m n {ok} = lteReflectsLTE m n (soToEq ok)
+
 ||| The example struct's fields: a u32, then a u64 and a double, each on
 ||| its natural boundary (4 bytes of padding after x).
 public export
@@ -240,10 +480,11 @@ exampleFields =
   , MkField "z" 16 8 8    -- Double at offset 16
   ]
 
-||| Example: simple struct layout, 24 bytes, 8-byte aligned (24 = 3 × 8).
+||| Example: simple struct layout, 24 bytes, 8-byte aligned (24 = 3 × 8),
+||| covering its last field end (16 + 8 = 24).
 public export
 exampleLayout : StructLayout
-exampleLayout = MkStructLayout exampleFields 24 8 (DivideBy 3 Refl)
+exampleLayout = MkStructLayout exampleFields 24 8 (fitsIn 24 24) (DivideBy 3 Refl)
 
 ||| The computed size agrees with the declared one.
 export
@@ -263,10 +504,34 @@ exampleFieldsAligned =
         (DivideBy 2 Refl)
         NoFields))
 
-||| Prove that every field in the example layout is correctly aligned.
+||| The example's fields are in order: x ends at 4 ≤ 8, y ends at 16 ≤ 16.
+export
+exampleFieldsOrdered : FieldsOrdered PanelClades.ABI.Layout.exampleFields
+exampleFieldsOrdered = OrdCons (fitsIn 4 8) (OrdCons (fitsIn 16 16) OrdOne)
+
+||| The example's alignments are 4 = 2 × 2 and 8 = 2 × 4.
+export
+exampleAlignmentsPow2 : AlignmentsPow2 PanelClades.ABI.Layout.exampleFields
+exampleAlignmentsPow2 = Pow2Cons four (Pow2Cons eight (Pow2Cons eight Pow2Nil))
+  where
+    four : IsPow2 4
+    four = Pow2Double (Pow2Double Pow2One)
+    eight : IsPow2 8
+    eight = Pow2Double four
+
+||| The example layout follows the C rules: aligned, first field at 0,
+||| ordered, power-of-two
+||| alignments, and struct alignment 8, its largest field alignment.
 export
 exampleLayoutValid : CABICompliant PanelClades.ABI.Layout.exampleLayout
-exampleLayoutValid = CABIOk exampleLayout exampleFieldsAligned
+exampleLayoutValid =
+  CABIOk exampleLayout exampleFieldsAligned (ZeroHead Refl)
+         exampleFieldsOrdered exampleAlignmentsPow2 Refl
+
+||| The decision procedure agrees on the example.
+export
+exampleCheckPasses : isRight (checkCABI PanelClades.ABI.Layout.exampleLayout) = True
+exampleCheckPasses = Refl
 
 --------------------------------------------------------------------------------
 -- Field lookup
@@ -279,7 +544,8 @@ lookupField : (layout : StructLayout) -> (fieldName : String) -> Maybe Field
 lookupField layout name = find (\f => f.name == name) layout.fields
 
 ||| Run-time check that a field's span `[offset, offset+size)` fits inside
-||| the struct.
+||| the struct.  For a field of the layout this always holds
+||| (`fieldWithinStruct`); it remains for fields from elsewhere.
 public export
 offsetInBounds : (layout : StructLayout) -> (f : Field) -> Bool
 offsetInBounds layout f = fieldEnd f <= layout.totalSize
diff --git a/panel-clades/src/abi/PanelClades/ABI/Types.idr b/panel-clades/src/abi/PanelClades/ABI/Types.idr
index c91db0f5..22a0eb90 100644
--- a/panel-clades/src/abi/PanelClades/ABI/Types.idr
+++ b/panel-clades/src/abi/PanelClades/ABI/Types.idr
@@ -144,6 +144,17 @@ public export
 DecEq Result where
   decEq = decEqViaTag resultTag resultFromTag resultTagRetract
 
+||| The C encoding of a `Result` is its decidable-equality tag, as a
+||| `Bits32`.  The two tables are written out separately; this keeps them
+||| from drifting apart.
+export
+resultTagsAgree : (r : Result) -> resultToInt r = cast (resultTag r)
+resultTagsAgree Ok           = Refl
+resultTagsAgree Error        = Refl
+resultTagsAgree InvalidParam = Refl
+resultTagsAgree OutOfMemory  = Refl
+resultTagsAgree NullPointer  = Refl
+
 --------------------------------------------------------------------------------
 -- Opaque Handles
 --------------------------------------------------------------------------------
@@ -401,6 +412,24 @@ public export
 DecEq CladeKind where
   decEq = decEqViaTag cladeKindTag cladeKindFromTag cladeKindTagRetract
 
+||| The C encoding of a `CladeKind` is its decidable-equality tag, as a
+||| `Bits32`, so the two tables cannot drift apart.
+export
+cladeKindTagsAgree : (k : CladeKind) -> cladeKindToInt k = cast (cladeKindTag k)
+cladeKindTagsAgree Directive  = Refl
+cladeKindTagsAgree Scanner    = Refl
+cladeKindTagsAgree Builder    = Refl
+cladeKindTagsAgree Database   = Refl
+cladeKindTagsAgree Network    = Refl
+cladeKindTagsAgree Viewer     = Refl
+cladeKindTagsAgree Ai         = Refl
+cladeKindTagsAgree Loader     = Refl
+cladeKindTagsAgree Meta       = Refl
+cladeKindTagsAgree Service    = Refl
+cladeKindTagsAgree Inspector  = Refl
+cladeKindTagsAgree Bridge     = Refl
+cladeKindTagsAgree Terminal   = Refl
+
 ||| The total number of clade kinds.
 public export
 cladeKindCount : Nat
diff --git a/panel-clades/src/abi/README.adoc b/panel-clades/src/abi/README.adoc
index 854b8d10..b0177312 100644
--- a/panel-clades/src/abi/README.adoc
+++ b/panel-clades/src/abi/README.adoc
@@ -31,7 +31,8 @@ Handle, the C type universe (`+CType+`, `+cSizeOf+`, `+HasSize+`),
 CladeId, CladeKind
 
 |`+PanelClades/ABI/Layout.idr+` |Alignment and struct layout: `+Divides+`,
-`+alignUp+`, `+FieldsAligned+`, `+CABICompliant+`
+`+alignUp+` and its bounds, `+FieldsAligned+`, `+FirstAtZero+`, `+FieldsOrdered+`,
+`+AlignmentsPow2+`, `+CABICompliant+`
 
 |`+PanelClades/ABI/Foreign.idr+` |FFI function declarations and their safe
 wrappers
@@ -49,10 +50,10 @@ against the clade's declared budget
 (all five modules)
 |===
 
-=== Check status (2026-10-14)
+=== Check status (2026-11-09)
 
 All five modules *typecheck* under Idris2 0.8.0
-(`+bash panel-clades/scripts/check-abi.sh+`), with six expected
+(`+bash panel-clades/scripts/check-abi.sh+`), with eleven expected
 rejections in `+tests/reject/+`.
 
 Before 2026-10-14, `+Types.idr+`, `+Layout.idr+` and `+Foreign.idr+` had
@@ -104,9 +105,12 @@ says so.
 |`+HasSize+` admits only `+cSizeOf+`; C int is 4 bytes everywhere; pointers are 8 bytes on Linux and 4 on WASM; size_t is pointer-sized |`+Verify.*+`; `+tests/reject/WasmPointerIsEightBytes.idr+` |PROVEN / TESTED
 |`+alignUp+` gives a multiple of the alignment; every computed struct size is a multiple of its alignment |`+alignUpCorrect+`, `+calcStructSizeAligned+` |PROVEN
 |`+Divides+` witnesses are equations |`+tests/reject/MisalignedField.idr+` |TESTED
-|The example layout is C-ABI compliant and its computed size is 24 |`+exampleLayoutValid+`, `+exampleSizeComputed+` |PROVEN
-|A computed struct size covers every field |`+verifyLayout+` checks at run time |ASSUMED (not proved)
-|`+decDivides+` returns `+Nothing+` only when the divisor does not divide |— |ASSUMED (not proved)
+|Rounding up to an alignment a ≥ 1 is at or above the size and below size + a |`+alignUpCovers+`, `+alignUpTight+` |PROVEN
+|A computed struct size covers every field, so every field of a layout lies within its total size |`+calcStructSizeCovers+`, `+fieldWithinEnd+`, `+fieldWithinStruct+` |PROVEN
+|`+CABICompliant+` evidence: offsets aligned, at least one field with the first at offset 0, fields in order without overlap, power-of-two alignments, struct alignment = largest field alignment |`+FieldsAligned+`, `+FirstAtZero+`, `+FieldsOrdered+`, `+AlignmentsPow2+`, `+maxAlignment+`; `+tests/reject/EmptyStruct.idr+`, `+FirstFieldNotAtZero.idr+`, `+OverlappingFields.idr+`, `+AlignmentNotPow2.idr+`, `+StructUnderAligned.idr+` |PROVEN / TESTED
+|The example layout is C-ABI compliant and its computed size is 24 |`+exampleLayoutValid+`, `+exampleSizeComputed+`, `+exampleCheckPasses+` |PROVEN
+|The `+Nat+` and `+Bits32+` tag tables agree |`+resultTagsAgree+`, `+cladeKindTagsAgree+` |PROVEN
+|`+decDivides+` returns `+Nothing+` only when the divisor does not divide; `+decPow2+` returns `+Nothing+` only for a non-power of two |— |ASSUMED (not proved)
 |A clade contract typechecks only if its config's declared peak fits its declared budget and its declared loss its tolerance |`+declaredContract+`; `+tests/reject/BudgetTooSmall.idr+`; `+gen-budgets.sh --check+` |PROVEN / TESTED
 |The neurosym-bridge budgets (peak 48, drift 16, budget 64; loss 2, tolerance 3) describe the panel |declared in `+clades/neurosym-bridge/config.k9.ncl+` |DESIGNED (declared, not measured)
 |The Zig FFI uses these tags, sizes and symbols |hand-restated in `+ffi/zig/src/main.zig+` |OPEN (no check)
@@ -114,7 +118,7 @@ says so.
 
 === Invariants
 
-* `+%default total+` in every module.
+* `+%default total+` in every module, before its first declaration.
 * No `+believe_me+`, `+assert_total+`, `+assert_smaller+`, `+idris_crash+`
 or `+unsafePerformIO+`. `+scripts/check-abi.sh+` greps for them and fails.
 
diff --git a/panel-clades/tests/reject/AlignmentNotPow2.idr b/panel-clades/tests/reject/AlignmentNotPow2.idr
new file mode 100644
index 00000000..6e397717
--- /dev/null
+++ b/panel-clades/tests/reject/AlignmentNotPow2.idr
@@ -0,0 +1,19 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- C alignments are powers of two.  decPow2 refuses 12, so a field aligned
+-- to 12 has no AlignmentsPow2 evidence and checkCABI refuses its layout.
+-- EXPECT: Mismatch between: True and False
+module AlignmentNotPow2
+
+import Data.Maybe
+import Data.Nat
+import Decidable.Equality
+import PanelClades.ABI.Layout
+
+%default total
+
+invalid : isJust (decPow2 12) = True
+invalid = Refl
diff --git a/panel-clades/tests/reject/EmptyStruct.idr b/panel-clades/tests/reject/EmptyStruct.idr
new file mode 100644
index 00000000..2b6738c7
--- /dev/null
+++ b/panel-clades/tests/reject/EmptyStruct.idr
@@ -0,0 +1,25 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- A C struct needs at least one member (C11 6.7.2.1p8).  This layout has
+-- none: size 0 covers its (no) fields and is a multiple of its alignment 1,
+-- which is the largest field alignment of an empty list, so only the
+-- member rule refuses it in checkCABI.
+-- EXPECT: Mismatch between: True and False
+module EmptyStruct
+
+import Data.Either
+import Data.So
+import Data.Nat
+import Decidable.Equality
+import PanelClades.ABI.Layout
+
+%default total
+
+empty : StructLayout
+empty = MkStructLayout [] 0 1 (fitsIn 0 0) (DivideBy 0 Refl)
+
+invalid : isRight (checkCABI EmptyStruct.empty) = True
+invalid = Refl
diff --git a/panel-clades/tests/reject/FirstFieldNotAtZero.idr b/panel-clades/tests/reject/FirstFieldNotAtZero.idr
new file mode 100644
index 00000000..180d822f
--- /dev/null
+++ b/panel-clades/tests/reject/FirstFieldNotAtZero.idr
@@ -0,0 +1,25 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- C allows no padding before the first member, so a struct whose only
+-- field sits at offset 8 has no C layout.  The field is aligned, the
+-- struct covers it and is aligned to 4: refused by checkCABI because the
+-- first field is not at offset 0.
+-- EXPECT: Mismatch between: True and False
+module FirstFieldNotAtZero
+
+import Data.Either
+import Data.So
+import Data.Nat
+import Decidable.Equality
+import PanelClades.ABI.Layout
+
+%default total
+
+padded : StructLayout
+padded = MkStructLayout [MkField "x" 8 4 4] 12 4 (fitsIn 12 12) (DivideBy 3 Refl)
+
+invalid : isRight (checkCABI FirstFieldNotAtZero.padded) = True
+invalid = Refl
diff --git a/panel-clades/tests/reject/OverlappingFields.idr b/panel-clades/tests/reject/OverlappingFields.idr
new file mode 100644
index 00000000..23c94f17
--- /dev/null
+++ b/panel-clades/tests/reject/OverlappingFields.idr
@@ -0,0 +1,18 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- Fields must be in order and must not overlap: b starts at 4, inside a,
+-- which ends at 8, so no FieldsOrdered evidence exists for them.
+-- EXPECT: Can't find an implementation for So False
+module OverlappingFields
+
+import Data.So
+import Data.Nat
+import PanelClades.ABI.Layout
+
+%default total
+
+invalid : FieldsOrdered [MkField "a" 0 8 8, MkField "b" 4 4 4]
+invalid = OrdCons (fitsIn 8 4) OrdOne
diff --git a/panel-clades/tests/reject/StructUnderAligned.idr b/panel-clades/tests/reject/StructUnderAligned.idr
new file mode 100644
index 00000000..ef2637ae
--- /dev/null
+++ b/panel-clades/tests/reject/StructUnderAligned.idr
@@ -0,0 +1,24 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- A struct is aligned to its largest field alignment.  This one declares
+-- 4 while its field needs 8: aligned, ordered, power-of-two, and still
+-- refused by checkCABI.
+-- EXPECT: Mismatch between: True and False
+module StructUnderAligned
+
+import Data.Either
+import Data.So
+import Data.Nat
+import Decidable.Equality
+import PanelClades.ABI.Layout
+
+%default total
+
+underAligned : StructLayout
+underAligned = MkStructLayout [MkField "y" 0 8 8] 8 4 (fitsIn 8 8) (DivideBy 2 Refl)
+
+invalid : isRight (checkCABI StructUnderAligned.underAligned) = True
+invalid = Refl
diff --git a/panel-clades/tests/scan/test-abi-scan.sh b/panel-clades/tests/scan/test-abi-scan.sh
new file mode 100755
index 00000000..4225dfba
--- /dev/null
+++ b/panel-clades/tests/scan/test-abi-scan.sh
@@ -0,0 +1,119 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# test-abi-scan.sh — regression tests for scripts/abi-scan-lib.sh, the scans
+# behind check-abi.sh.  Both ways: each planted escape, hole, missing
+# directive or commented-out import must be caught or ignored as stated, and
+# the same words in comments or strings must not trip a scan.  Needs only
+# bash and awk; it runs before the Idris2 build in CI.
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." || exit 1
+# shellcheck source=../../scripts/abi-scan-lib.sh
+. scripts/abi-scan-lib.sh
+
+work="$(mktemp -d)"; trap 'rm -rf "$work"' EXIT
+fail=0; n=0
+
+# mod BODY... : write a module T.idr whose lines are BODY (no %default added).
+mod() { printf '%s\n' "module T" "$@" > "$work/T.idr"; }
+
+# expect found|clean DESCRIPTION BODY... : scan_escapes on a module with
+# `%default total` plus BODY.
+expect() {
+  local want="$1" what="$2"; shift 2
+  mod "%default total" "$@"
+  local got=clean
+  if scan_escapes "$work/T.idr" > /dev/null; then got=found; fi
+  n=$((n + 1))
+  if [[ "$got" == "$want" ]]; then echo "ok   $want: $what"; else echo "FAIL got $got, want $want: $what"; fail=1; fi
+}
+
+expect found "hole"                       'f : Nat' 'f = ?todo'
+expect found "hole as an argument"        'f : Nat -> Nat' 'f x = plus x ?hole_1'
+expect found "believe_me"                 'f = believe_me 1'
+expect found "idris_crash"                'g = idris_crash ""'
+expect found "assert_total"               'g = assert_total (f 1)'
+expect found "assert_smaller"             'g = assert_smaller x y'
+expect found "unsafePerformIO"            'g = unsafePerformIO action'
+expect found "postulate"                  'postulate p : Nat'
+expect found "partial declaration"        'partial' 'f : Nat'
+expect found "export partial"             'export partial' 'f : Nat'
+expect found "covering declaration"       'covering' 'f : Nat'
+expect found "hole after an operator"     'x = a --> ?b'
+expect clean "words in a line comment"    '-- NO believe_me, NO postulate, ?hole here'
+expect clean "words in a doc comment"     '||| partial functions and ?holes are banned'
+expect clean "nested block comment"       '{- block' 'believe_me ?x' '{- nested -} still' '-}' 'f : Nat'
+expect clean "words in a string"          'msg = "is it ?ok to say believe_me"'
+expect clean "operator, not a comment"    'x = a --> b'
+expect clean "operator ending in ?, not a hole" 'x = a =?b'
+expect found "hole after an operator and a space" 'x = a =? ?b'
+expect clean "primed identifier"          "f' : Nat" "f' = 1"
+expect clean "identifier containing partial" 'partialSum : Nat'
+expect found "escape after an escaped-quote char literal" "f = ('\\\"', believe_me v)"
+expect found "escape after an escaped-apostrophe char"   "f = ('\\'', believe_me v)"
+expect found "escape after a quote char literal"         "f = ('\"', believe_me v)"
+expect found "escape after a hex char literal"           "f = ('\\x41', ?h)"
+expect found "escape after a raw string with a backslash" 'f = #"\"# ++ believe_me v'
+expect found "escape after a closed multi-line string"   's = """' 'text' '"""' 'g = believe_me 1'
+expect clean "words in a raw string"      'msg = #"say "believe_me" and ?ok"#'
+expect clean "words in a multi-line string" 's = """' 'believe_me ?x partial' '"""'
+expect clean "primed identifier then a char literal" "f' = g' 'a'"
+expect found "uppercase hole"             'f = ?Todo'
+expect found "escape inside an interpolation" 'bad = "\{believe_me {a=Nat} {b=String} 0}"'
+expect found "hole inside an interpolation"   'f = "x \{?h} y"'
+expect found "escape inside a raw-string interpolation" 'f = #"\#{believe_me v}"#'
+expect found "escape inside a multi-line interpolation" 's = """' '  \{believe_me v}' '"""'
+expect found "escape after nested braces in an interpolation" 'f = "\{g {x = 1} y}" ++ believe_me v'
+expect found "escape in a string nested in an interpolation, then code" 'f = "\{g "}" ++ believe_me v} z"'
+expect clean "words beside an interpolation" 'msg = "believe_me \{show n} partial"'
+expect clean "text after nested braces in an interpolation" 'f = "\{g {x = 1} y} believe_me"'
+expect clean "\\{ in a raw string is text"   'msg = #"\{believe_me}"#'
+
+# %default total: required in code, not in a comment.
+directive() { # directive found|clean DESCRIPTION BODY...
+  local want="$1" what="$2"; shift 2
+  mod "$@"
+  local got=clean
+  if scan_escapes "$work/T.idr" > /dev/null; then got=found; fi
+  n=$((n + 1))
+  if [[ "$got" == "$want" ]]; then echo "ok   $want: $what"; else echo "FAIL got $got, want $want: $what"; fail=1; fi
+}
+directive found "no %default total"            'f : Nat'
+directive found "%default total only in a block comment" '{-' '%default total' '-}' 'f : Nat'
+directive found "%default total only in a line comment"  '-- %default total' 'f : Nat'
+directive found "%default covering"            '%default covering' 'f : Nat'
+directive found "%default total only in a multi-line string" 's : String' 's = """' '%default total' '"""'
+directive clean "%default total in code"       '%default total' 'f : Nat'
+directive found "%default total after a declaration" 'loop : Nat -> Nat' 'loop n = loop n' '%default total'
+directive clean "imports and directives before %default total" 'import Data.Nat' '%hide Prelude.id' '%default total' 'f : Nat'
+# A long module: grep must read to the end, or SIGPIPE under pipefail reads
+# as a missing directive.
+mapfile -t long < <(for i in $(seq 1 20000); do printf 'v%d : Nat\n' "$i"; done)
+directive clean "%default total in a 20,000-line module" '%default total' "${long[@]}"
+
+# import_cone: commented-out imports are not dependencies; indented ones are.
+mkdir -p "$work/root/A" "$work/root/B"
+printf '%s\n' "module A.Real" "%default total" "import A.Deep" > "$work/root/A/Real.idr"
+printf '%s\n' "module A.Deep" "%default total" > "$work/root/A/Deep.idr"
+printf '%s\n' "module A.Indented" "%default total" > "$work/root/A/Indented.idr"
+printf '%s\n' "module B.Ghost" "%default total" > "$work/root/B/Ghost.idr"
+printf '%s\n' "module Top" "%default total" \
+  "import A.Real" "  import public A.Indented" "import Data.Nat" \
+  "{- import B.Ghost -}" "-- import B.Ghost" > "$work/Top.idr"
+cone="$(import_cone "$work/base" "$work/root" -- "$work/Top.idr")"
+check_cone() { # check_cone yes|no PATH DESCRIPTION
+  n=$((n + 1))
+  if grep -qxF "$2" <<< "$cone"; then got=yes; else got=no; fi
+  if [[ "$got" == "$1" ]]; then echo "ok   cone $1: $3"; else echo "FAIL cone got $got, want $1: $3"; fail=1; fi
+}
+check_cone yes "$work/root/A/Real.idr"     "an import"
+check_cone yes "$work/root/A/Deep.idr"     "a transitive import"
+check_cone yes "$work/root/A/Indented.idr" "an indented import public"
+check_cone no  "$work/root/B/Ghost.idr"    "imports inside comments"
+n=$((n + 1))
+if grep -qxF Data.Nat "$work/base"; then echo "ok   base: unresolved import listed"; else echo "FAIL base: Data.Nat not listed"; fail=1; fi
+
+echo
+[[ "$fail" -eq 0 ]] || { echo "ABI SCAN TESTS FAILED"; exit 1; }
+echo "OK: abi scan — $n cases"
diff --git a/scripts/check-provenance-model.sh b/scripts/check-provenance-model.sh
new file mode 100755
index 00000000..f189e624
--- /dev/null
+++ b/scripts/check-provenance-model.sh
@@ -0,0 +1,79 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-provenance-model.sh — model-check docs/models/Provenance.tla with TLC,
+# both ways:
+#
+#   Provenance.cfg            author key leaked   -> no error (must pass)
+#   ProvenanceWitnessLeak.cfg witness key leaked  -> no error (must pass)
+#   ProvenanceBothLeak.cfg    both keys leaked    -> invariant Genuine is
+#                                                    violated (must be found)
+#
+# The third run is what keeps the property honest: if TLC stopped finding
+# the both-keys forgery, the model would have become vacuous, and this
+# script fails.  A missing toolchain or an unexpected TLC version is a
+# failure, never a skip.
+#
+# Usage: check-provenance-model.sh /path/to/tla2tools.jar
+# The jar's version and digest are pinned in build-validation.yml
+# (provenance-model job); the deviation record is in PROOF-NEEDS.adoc.
+set -uo pipefail
+JAR="${1:?usage: check-provenance-model.sh /path/to/tla2tools.jar}"
+# Resolve a relative jar path before the cd below.
+case "$JAR" in /*) ;; *) JAR="$PWD/$JAR" ;; esac
+EXPECT_VERSION="TLC2 Version 2.19 of 08 August 2024"
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../docs/models" || exit 1
+command -v java >/dev/null || { echo "FAIL: java not on PATH"; exit 1; }
+[[ -f "$JAR" ]] || { echo "FAIL: $JAR not found"; exit 1; }
+
+work="$(mktemp -d)"; trap 'rm -rf "$work"' EXIT
+fail=0
+
+run() { # run <config> -> log in $work/<config>.log, exit status in $?
+  java -XX:+UseParallelGC -cp "$JAR" tlc2.TLC -workers auto -deadlock -coverage 600 \
+    -metadir "$work/$1.states" -config "$1.cfg" Provenance.tla > "$work/$1.log" 2>&1
+}
+
+# reached <log> <Action>: the distinct-state count TLC's coverage report
+# gives the action (-coverage prints it once, at the end of the run).
+reached() {
+  sed -nE "s/^<$2 line [0-9]+, col [0-9]+ to line [0-9]+, col [0-9]+ of module Provenance>: ([0-9]+):[0-9]+\$/\\1/p" "$1" | head -n 1
+}
+
+# Each single-key run must actually exercise its leak: the leaked key's
+# forge action reaches a state and the other forge action reaches none, so a
+# configuration that leaks no key (or the wrong one) cannot pass vacuously.
+for cfg in Provenance ProvenanceWitnessLeak; do
+  case "$cfg" in
+    Provenance)            leaked=ForgeAuthor  sound=ForgeWitness ;;
+    ProvenanceWitnessLeak) leaked=ForgeWitness sound=ForgeAuthor ;;
+  esac
+  run "$cfg"; st=$?
+  grep -qF "$EXPECT_VERSION" "$work/$cfg.log" \
+    || { echo "FAIL: $cfg: TLC is not '$EXPECT_VERSION'"; head -5 "$work/$cfg.log"; fail=1; continue; }
+  if [[ "$st" -eq 0 ]] && grep -q '^Model checking completed. No error has been found.' "$work/$cfg.log"; then
+    echo "PASS: $cfg — $(grep -E '^[0-9]+ states generated' "$work/$cfg.log")"
+  else
+    tail -40 "$work/$cfg.log"; echo "FAIL: $cfg (exit $st): expected no error"; fail=1
+  fi
+  n_leaked="$(reached "$work/$cfg.log" "$leaked")"; n_sound="$(reached "$work/$cfg.log" "$sound")"
+  if [[ "${n_leaked:-0}" -gt 0 && "$n_sound" == 0 ]]; then
+    echo "PASS: $cfg exercises its leak — $leaked reached $n_leaked distinct states, $sound none"
+  else
+    echo "FAIL: $cfg: expected $leaked > 0 and $sound = 0 distinct states, got $leaked=${n_leaked:-missing} $sound=${n_sound:-missing}"; fail=1
+  fi
+done
+
+cfg=ProvenanceBothLeak
+run "$cfg"; st=$?
+if ! grep -qF "$EXPECT_VERSION" "$work/$cfg.log"; then
+  echo "FAIL: $cfg: TLC is not '$EXPECT_VERSION'"; head -5 "$work/$cfg.log"; fail=1
+elif [[ "$st" -ne 0 ]] && grep -q '^Error: Invariant Genuine is violated' "$work/$cfg.log"; then
+  echo "PASS: $cfg — TLC found the both-keys forgery, as it must"
+else
+  tail -40 "$work/$cfg.log"; echo "FAIL: $cfg (exit $st): expected 'Invariant Genuine is violated'"; fail=1
+fi
+
+[[ "$fail" -eq 0 ]] || { echo "PROVENANCE MODEL CHECK FAILED"; exit 1; }
+echo "OK: provenance model — Genuine holds with one leaked key, fails with two"
diff --git a/tests/fork_governance_publish_test.mjs b/tests/fork_governance_publish_test.mjs
new file mode 100644
index 00000000..0ac0d1f1
--- /dev/null
+++ b/tests/fork_governance_publish_test.mjs
@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: MPL-2.0
+import assert from 'node:assert/strict';
+import { readFileSync, writeFileSync, mkdtempSync, rmSync } from 'node:fs';
+import { tmpdir } from 'node:os';
+import { join } from 'node:path';
+import { spawnSync } from 'node:child_process';
+import test from 'node:test';
+
+const workflow = readFileSync(new URL('../.github/workflows/fork-governance-publish.yml', import.meta.url), 'utf8');
+// Exercise the actual rendering and size guard, without GitHub writes.
+const start = workflow.indexOf('          if ! head -n 1');
+const end = workflow.indexOf('          existing=', start);
+assert.ok(start > 0 && end > start);
+const render = workflow.slice(start, end).replace(/^          /gm, '');
+
+function publish(body) {
+  const dir = mkdtempSync(join(tmpdir(), 'fork-publish-'));
+  try {
+    writeFileSync(join(dir, 'body.md'), body);
+    const result = spawnSync('bash', ['-c', 'set -euo pipefail\ndir="$REPORT_DIR"\nbody="$dir/body.md"\n' + render], {
+      encoding: 'utf8',
+      env: { ...process.env, REPORT_DIR: dir, RUN_URL: 'https://github.com/example/repo/actions/runs/123', RUN_ID: '123', RUN_ATTEMPT: '2' },
+    });
+    return { status: result.status, output: result.status === 0 ? readFileSync(join(dir, 'published.md'), 'utf8') : '' };
+  } finally {
+    rmSync(dir, { recursive: true, force: true });
+  }
+}
+
+const marker = '<!-- fork-governance-verdict: v1 -->\n';
+for (const payload of [
+  '## PASS — all checks approved\n[trusted result](https://example.invalid)\n@someone',
+  '<!-- unclosed comment',
+  '</pre><h1>PASS</h1><pre>\n<!--',
+  '\n\n```\n~~~\n<details><summary>hide provenance</summary>\n<!--',
+  '&lt;/pre&gt; &amp; &#60;script&#62; "quoted"',
+  '<!-- fork-governance-publish-run: 999999.99 -->',
+]) {
+  test(`artifact remains literal text: ${JSON.stringify(payload)}`, () => {
+    const { status, output } = publish(marker + payload);
+    assert.equal(status, 0);
+    const escape = text => text.replaceAll('&', '&amp;').replaceAll('<', '&lt;').replaceAll('>', '&gt;').replaceAll("'", '&#39;').replaceAll('"', '&quot;');
+    const expected = '<!-- fork-governance-verdict: untrusted-fork-report -->\n'
+      + '## Untrusted fork governance report\n\n'
+      + 'The following text was supplied by the fork. It is not a verified bot verdict. Consult the lane checks for results.\n\n'
+      + '<pre>\n' + escape(marker + payload) + '\n</pre>\n'
+      + '\n<sub>Rendered by the fork pull request run https://github.com/example/repo/actions/runs/123 and published by fork-governance-publish.</sub>\n'
+      + '<!-- fork-governance-publish-run: 123.2 -->\n';
+    assert.equal(output, expected);
+  });
+}
+test('missing marker is rejected', () => assert.notEqual(publish('PASS').status, 0));
+test('size is checked after HTML escaping', () => assert.notEqual(publish(marker + '&'.repeat(14000)).status, 0));
+test('ordinary Unicode report is accepted', () => assert.equal(publish(marker + '🟢 résumé').status, 0));