diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml
index 9628701a..a274e16e 100644
--- a/.github/workflows/verify-proofs.yml
+++ b/.github/workflows/verify-proofs.yml
@@ -17,6 +17,9 @@ on:
     - verification/proofs/agda/**
     - verification/PROOF-STATUS.adoc
     - scripts/check-proof-status.sh
+    - verification/proof-ledger.jsonl
+    - scripts/proof-ledger.sh
+    - tests/proof-ledger-test.sh
     - scripts/check-trusted-base.sh
     - docs/proof-debt.adoc
     - test/soundness/**
@@ -42,6 +45,9 @@ on:
     - verification/proofs/agda/**
     - verification/PROOF-STATUS.adoc
     - scripts/check-proof-status.sh
+    - verification/proof-ledger.jsonl
+    - scripts/proof-ledger.sh
+    - tests/proof-ledger-test.sh
     - scripts/check-trusted-base.sh
     - docs/proof-debt.adoc
     - test/soundness/**
@@ -426,6 +432,18 @@ jobs:
       - name: PROOF-STATUS.adoc agrees with the tree
         run: bash scripts/check-proof-status.sh
 
+      # The machine ledger is canonical (README-EXPLAINME section 5): it must
+      # obey its rules and the tree, and the Proof Ledger table must be its
+      # rendering. The contracts plant each defect the check exists to catch.
+      - name: Proof ledger is valid and agrees with the tree
+        run: bash scripts/proof-ledger.sh check
+
+      - name: Proof Ledger table is the ledger's rendering
+        run: bash scripts/proof-ledger.sh render --check
+
+      - name: Proof ledger contracts (planted defects)
+        run: bash tests/proof-ledger-test.sh
+
   check-trusted-base:
     name: check-trusted-base
     runs-on: ubuntu-latest
diff --git a/.reuse/dep5 b/.reuse/dep5
index 97db7052..a06444c7 100644
--- a/.reuse/dep5
+++ b/.reuse/dep5
@@ -28,3 +28,10 @@ Comment: Verbatim `gh actions-lock` output, copied byte-for-byte from the
  hyperpolymath/standards .github/workflows/actions.lock at b3ce78e). These
  are tool-owned files: never hand-edit or reformat them; replace them with a
  fresh copy instead.
+
+Files: verification/proof-ledger.jsonl
+Copyright: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+License: MPL-2.0
+Comment: The machine proof ledger: one JCS object per line, so it cannot
+ carry an SPDX comment. Machine-readable specification data, licensed as
+ code.
diff --git a/scripts/proof-ledger.sh b/scripts/proof-ledger.sh
new file mode 100755
index 00000000..bebb8720
--- /dev/null
+++ b/scripts/proof-ledger.sh
@@ -0,0 +1,270 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# proof-ledger.sh — the machine proof ledger (verification/proof-ledger.jsonl)
+# is canonical; the Proof Ledger table in verification/PROOF-STATUS.adoc is
+# rendered from it (README-EXPLAINME-STANDARD section 5, rule 1).
+#
+#   proof-ledger.sh check          validate the ledger against its rules and the tree
+#   proof-ledger.sh render         print the AsciiDoc block for PROOF-STATUS.adoc
+#   proof-ledger.sh render --check fail if PROOF-STATUS.adoc holds a different block
+#   proof-ledger.sh render --write replace the block in PROOF-STATUS.adoc
+#
+# One JSON object per line, I-JSON serialised as JCS (RFC 8785): keys sorted,
+# no insignificant whitespace, one final LF. The ledger is held to a profile
+# in which `jq -cS` output IS the JCS form: ASCII strings and no numbers.
+#
+# Status vocabulary (closed; PROOF-POLICY section 5 gives the upper-case
+# labels): proven, proven-with-postulates, argued, tested-only, open.
+# Proof Witness Grades (PROOF-POLICY section 8) are recorded for theory rows
+# only: 3, 2i, 2ii, 1 or ungraded. A grade is computed from the row's legs,
+# never asserted (section 8.4). A leg (rocq, lean, or other for a
+# foundation-diverse witness) counts when its kernel accepted it (proven or
+# proven-with-postulates) and its statement correspondence is reconciled
+# (section 8.2). PWG-1 needs a current per-commit receipt for every witness;
+# this ledger records none yet, so PWG-1 is refused.
+#
+# The policy this gate enforces is pinned by repository, path and full
+# commit in POLICY_PIN (PROOF-POLICY section 7). Moving the pin is a
+# reviewed change; the check fails when the pin is missing or malformed.
+#
+# Exit: 0 = ledger valid (and the block current, for render --check);
+#       1 = invalid or stale; 2 = usage or IO error.
+
+set -euo pipefail
+
+LEDGER="${PROOF_LEDGER:-verification/proof-ledger.jsonl}"
+DOC="${PROOF_STATUS_DOC:-verification/PROOF-STATUS.adoc}"
+BEGIN_MARK='// BEGIN GENERATED: scripts/proof-ledger.sh render (do not edit by hand)'
+END_MARK='// END GENERATED: proof ledger'
+AGDA_PROFILE='--safe --without-K --cubical-compatible'
+# PROOF-POLICY section 7: repository, path and full 40-character commit.
+POLICY_PIN="${PROOF_POLICY_PIN-metadatastician/standards 3-practice/PROOF-POLICY.adoc b8f60511e76c9015d86990317162dce653c92fe1}"
+
+[ -f "$LEDGER" ] || { echo "::error::proof-ledger: $LEDGER not found"; exit 2; }
+
+check() {
+  local fails=0 n=0 line id unparsed=0
+  if ! [[ "$POLICY_PIN" =~ ^[A-Za-z0-9_.-]+/[A-Za-z0-9_.-]+\ [^\ ]+\.adoc\ [0-9a-f]{40}$ ]]; then
+    echo "::error::proof-ledger: the PROOF-POLICY pin is missing or malformed ('$POLICY_PIN'); it names repository, path and full commit (section 7)"
+    fails=$((fails + 1))
+  fi
+  # Byte profile: every line is its own `jq -cS` rendering, ASCII only, and
+  # the file ends in exactly one LF.
+  if LC_ALL=C grep -nP '[^\x00-\x7F]' "$LEDGER" >/dev/null; then
+    echo "::error::proof-ledger: non-ASCII byte in $LEDGER (the profile is ASCII so that jq -cS is JCS)"; fails=$((fails + 1))
+  fi
+  if [ -n "$(tail -c1 "$LEDGER")" ] || [ -z "$(tail -c2 "$LEDGER" | head -c1)" ]; then
+    echo "::error::proof-ledger: $LEDGER must end in exactly one LF"; fails=$((fails + 1))
+  fi
+  while IFS= read -r line; do
+    n=$((n + 1))
+    if ! canon=$(jq -cS . <<<"$line" 2>/dev/null); then
+      echo "::error::proof-ledger: line $n is not JSON"; fails=$((fails + 1)); unparsed=1
+    elif [ "$(jq -r type <<<"$canon")" != object ]; then
+      echo "::error::proof-ledger: line $n is not a JSON object"; fails=$((fails + 1)); unparsed=1
+    elif [ "$canon" != "$line" ]; then
+      echo "::error::proof-ledger: line $n is not in canonical (jq -cS / JCS) form"; fails=$((fails + 1))
+    fi
+  done < "$LEDGER"
+  [ "$n" -gt 0 ] || { echo "::error::proof-ledger: $LEDGER has no rows"; exit 1; }
+  # The schema pass reads every line as a JSON object; a line that is not one
+  # would abort it, so stop here with the lines named.
+  if [ "$unparsed" -eq 1 ]; then
+    echo "proof-ledger: INVALID ($fails problem(s)) in $LEDGER"
+    return 1
+  fi
+
+  # Schema and status rules, one message per broken rule.
+  local errs
+  errs=$(jq -r --arg agda "$AGDA_PROFILE" '
+    def need(k; t): if (has(k) and (.[k] | type) == t) then empty else "\(.id // "?"): field \(k) must be a \(t)" end;
+    # Field types first: a row with a missing or mistyped field gets only
+    # those messages, since the rules below assume the types.
+    . as $r
+    | [ need("id"; "string"), need("kind"; "string"), need("obligation"; "string"),
+        need("status"; "string"), need("checker"; "string"), need("file"; "string"),
+        need("names"; "array"), need("axioms"; "array"), need("bounds"; "string"),
+        need("trust_boundary"; "string"),
+        (if any(.names[]?, .axioms[]?; type != "string") then "\(.id // "?"): names and axioms hold strings" else empty end) ] as $te
+    | if ($te | length) > 0 then $te[] else
+      ( [keys[] | select(IN("id","kind","obligation","status","checker","file","names","axioms","bounds","trust_boundary","pwg","foundation_diverse","legs") | not)]
+        | if length > 0 then "\($r.id): unknown field(s) \(join(", "))" else empty end ),
+      # The profile in which jq -cS is JCS has no numbers anywhere, and a
+      # control character would break the rendered table.
+      ( if [.. | numbers] | length > 0 then "\(.id): the ledger profile holds no numbers (write them as strings)" else empty end ),
+      ( if [.. | strings | select(any(explode[]; . < 32 or . == 127))] | length > 0 then "\(.id): a string holds a control character" else empty end ),
+      ( if .checker == "" or .obligation == "" or .trust_boundary == "" then "\(.id): checker, obligation and trust_boundary are not empty (use - for no checker)" else empty end ),
+      ( if (.id | test("^[a-z0-9]+(-[a-z0-9]+)*$")) then empty else "\(.id): id must be lower-case words joined by -" end ),
+      ( if IN(.kind; "engineering", "theory") then empty else "\(.id): kind must be engineering or theory" end ),
+      ( if IN(.status; "proven", "proven-with-postulates", "argued", "tested-only", "open") then empty
+        else "\(.id): status \(.status) is outside the closed vocabulary" end ),
+      ( if (.status == "proven" or .status == "proven-with-postulates") and .checker == "-" then "\(.id): a proven row names its checker" else empty end ),
+      ( if .status == "proven" and (.axioms | length) > 0 then "\(.id): proven rests on no axioms; with \(.axioms | join(", ")) it is proven-with-postulates" else empty end ),
+      ( if .status == "proven-with-postulates" and (.axioms | length) == 0 then "\(.id): proven-with-postulates lists its axioms" else empty end ),
+      ( if .status != "proven" and .status != "proven-with-postulates" and (.axioms | length) > 0 then "\(.id): only a proven row carries axioms" else empty end ),
+      ( if .status == "tested-only" and .bounds == "" then "\(.id): tested-only gives its bounds" else empty end ),
+      ( if .status != "tested-only" and .bounds != "" then "\(.id): only a tested-only row has bounds" else empty end ),
+      ( if .status != "open" and .file == "-" then "\(.id): only an open row may have no file" else empty end ),
+      ( if .file != "-" and (.names | length) == 0 then "\(.id): a row with a file names what it rests on in that file" else empty end ),
+      ( if .kind == "theory" then
+          ( if IN(.pwg; "3", "2i", "2ii", "1", "ungraded") then empty else "\(.id): a theory row records pwg as 3, 2i, 2ii, 1 or ungraded" end ),
+          ( if (.foundation_diverse | type) == "boolean" then empty else "\(.id): a theory row records foundation_diverse" end ),
+          ( if (.legs | type) == "array" then
+              # A leg: {prover, route, status, correspondence, axioms}; every
+              # field is checked, since the grade is computed from them.
+              ( .legs[] | . as $l
+                | if type != "object" then "\($r.id): a leg is an object"
+                  else
+                    ( [keys[] | select(IN("prover","route","status","correspondence","axioms") | not)]
+                      | if length > 0 then "\($r.id): unknown leg field(s) \(join(", "))" else empty end ),
+                    ( if IN($l.prover; "rocq", "lean", "other") then empty else "\($r.id): a leg prover is rocq, lean or other" end ),
+                    ( if IN($l.route; "transported", "re-proved") then empty else "\($r.id): a leg route is transported or re-proved" end ),
+                    ( if IN($l.status; "proven", "proven-with-postulates", "assumed", "waived", "unavailable", "bridge-pending") then empty
+                      else "\($r.id): a leg status is proven, proven-with-postulates, assumed, waived, unavailable or bridge-pending" end ),
+                    ( if IN($l.correspondence; "reconciled", "pending") then empty else "\($r.id): a leg correspondence is reconciled or pending" end ),
+                    ( if ($l.axioms | type) == "array" and all($l.axioms[]; type == "string") then empty else "\($r.id): a leg lists its axioms as strings" end ),
+                    ( if $l.status == "proven" and ($l.axioms | length) > 0 then "\($r.id): a proven leg rests on no axioms" else empty end )
+                  end )
+            else "\(.id): a theory row records its legs" end ),
+          # The grade the legs support (section 8.2), compared with the one
+          # recorded: a grade is computed, never asserted.
+          ( def counts: type == "object" and IN(.status; "proven", "proven-with-postulates") and .correspondence == "reconciled";
+            def counted(p): [.legs[]? | select(counts and .prover == p)] | length > 0;
+            (if ((.status == "proven" or .status == "proven-with-postulates")
+                 and (.checker | contains("Agda")) and (.checker | contains($agda))) | not then "ungraded"
+             elif counted("rocq") and counted("lean") then "2ii"
+             elif counted("rocq") or counted("lean") then "2i"
+             else "3" end) as $grade
+            | if .pwg == "1" then "\(.id): PWG-1 needs a current per-commit receipt for every witness, which this ledger does not record (section 8.2)"
+              elif .pwg != $grade then
+                (if $grade == "ungraded" and .pwg != "ungraded"
+                 then "\(.id): PWG-\(.pwg) needs an Agda proof that is proven or proven-with-postulates under the PROOF-POLICY 2.1 invocation (\($agda)); the legs support ungraded"
+                 else "\(.id): pwg is \(.pwg), and the legs support \(if $grade == "ungraded" then "ungraded" else "PWG-" + $grade end)" end)
+              else empty end ),
+          ( if (.foundation_diverse == true) != ([.legs[]? | select(type == "object" and .prover == "other" and IN(.status; "proven", "proven-with-postulates") and .correspondence == "reconciled")] | length > 0)
+            then "\(.id): foundation_diverse is true exactly when an other-foundation leg counts (section 8.3)" else empty end )
+        else
+          ( if has("pwg") or has("legs") or has("foundation_diverse") then "\(.id): pwg, legs and foundation_diverse belong to theory rows" else empty end )
+        end )
+      end
+  ' "$LEDGER")
+  if [ -n "$errs" ]; then
+    while IFS= read -r e; do echo "::error::proof-ledger: $e"; done <<<"$errs"
+    fails=$((fails + $(wc -l <<<"$errs")))
+  fi
+  local dups
+  dups=$(jq -r '.id' "$LEDGER" | sort | uniq -d)
+  if [ -n "$dups" ]; then echo "::error::proof-ledger: duplicate id(s): $dups"; fails=$((fails + 1)); fi
+
+  # Currency against the tree: the file exists, and every name it rests on
+  # is in it (a renamed proof turns this red).
+  local file name
+  while IFS=$'\t' read -r id file name; do
+    if [ ! -f "$file" ]; then
+      echo "::error::proof-ledger: $id names $file, which does not exist"; fails=$((fails + 1)); continue
+    fi
+    if [ -n "$name" ] && ! grep -qwF -- "$name" "$file"; then
+      echo "::error::proof-ledger: $id says $file holds '$name', and it does not (renamed or removed?)"; fails=$((fails + 1))
+    fi
+  done < <(jq -r 'select(.file != "-" and (.names | type) == "array" and (.file | type) == "string") | .id as $i | .file as $f | if (.names | length) == 0 then [$i, $f, ""] else (.names[] | [$i, $f, .]) end | @tsv' "$LEDGER")
+
+  if [ "$fails" -gt 0 ]; then
+    echo "proof-ledger: INVALID ($fails problem(s)) in $LEDGER"
+    return 1
+  fi
+  echo "proof-ledger: $n rows valid; $(census)"
+}
+
+# A census, never a percentage (PROOF-POLICY 8.4, README-EXPLAINME 5 rule 2).
+census() {
+  jq -rs '
+    def c(s): [.[] | select(.status == s)] | length;
+    def g(p): [.[] | select(.kind == "theory" and .pwg == p)] | length;
+    "\(c("proven")) proven of \(length); \(c("proven-with-postulates")) proven-with-postulates, \(c("tested-only")) tested-only, \(c("argued")) argued, \(c("open")) open. Theory rows: \([.[] | select(.kind == "theory")] | length) (PWG-1 \(g("1")), PWG-2ii \(g("2ii")), PWG-2i \(g("2i")), PWG-3 \(g("3")), ungraded \(g("ungraded")))."
+  ' "$LEDGER"
+}
+
+render() {
+  printf '%s\n' "$BEGIN_MARK"
+  printf '%s\n' '[[proof-ledger]]'
+  printf '%s\n' '=== Proof Ledger'
+  printf '\n'
+  # shellcheck disable=SC2016  # the backticks are AsciiDoc, printed literally
+  printf 'Rendered from `+%s+`, which is canonical: where this table and the\n' "$LEDGER"
+  printf 'ledger disagree, the ledger wins and this table is regenerated.\n'
+  # shellcheck disable=SC2016  # the backticks are AsciiDoc, printed literally
+  printf 'Checked against PROOF-POLICY as pinned by `+%s+`.\n' "$POLICY_PIN"
+  printf '\n'
+  printf '*Census:* %s\n' "$(census)"
+  printf '\n'
+  printf '%s\n' '[cols="3,1,2,2,2",options="header"]'
+  printf '%s\n' '|==='
+  printf '%s\n' '|Obligation |Status |Checker (version, flags) |Where |Trust boundary'
+  jq -r '
+    def esc: gsub("\\|"; "{vbar}");
+    def code: "`+" + . + "+`";
+    "\n|" + (.obligation | esc)
+    + "\n|" + .status
+      + (if (.axioms | length) > 0 then " (" + (.axioms | join(", ")) + ")" else "" end)
+      + (if .kind == "theory" then (if .pwg == "ungraded" then ", ungraded" else ", PWG-" + .pwg end)
+           + (if .foundation_diverse then " +foundation-diverse" else "" end) else "" end)
+    + "\n|" + (if .checker == "-" then "-" else (.checker | esc) end)
+    + "\n|" + (if .file == "-" then "-" else (.file | code) + (if (.names | length) > 0 then ": " + (.names | map(code) | join(", ")) else "" end) end)
+    + "\n|" + (.trust_boundary | esc)
+      + (if .bounds != "" then ". Bounds: " + (.bounds | esc) else "" end)
+  ' "$LEDGER"
+  printf '%s\n' '|==='
+  printf '%s\n' "$END_MARK"
+}
+
+# Exactly one BEGIN and one END marker, BEGIN first: a second block (a bad
+# merge, a hand copy) would publish two tables while the first one passed.
+markers_ok() {
+  local b e
+  b=$(grep -cxF -- "$BEGIN_MARK" "$DOC" || true)
+  e=$(grep -cxF -- "$END_MARK" "$DOC" || true)
+  [ "$b" = 1 ] && [ "$e" = 1 ] || return 1
+  [ "$(grep -nxF -- "$BEGIN_MARK" "$DOC" | cut -d: -f1)" -lt "$(grep -nxF -- "$END_MARK" "$DOC" | cut -d: -f1)" ]
+}
+
+doc_block() {
+  awk -v b="$BEGIN_MARK" -v e="$END_MARK" '$0 == b { on = 1 } on { print } $0 == e { exit }' "$DOC"
+}
+
+case "${1:-}" in
+  check) check ;;
+  render)
+    case "${2:-}" in
+      "") render ;;
+      --check)
+        [ -f "$DOC" ] || { echo "::error::proof-ledger: $DOC not found"; exit 2; }
+        if ! markers_ok; then
+          echo "::error::proof-ledger: $DOC lacks the generated-block markers, holds more than one pair, or has them out of order; it needs exactly one pair (render --write needs them too)"; exit 2
+        fi
+        if ! diff -u <(doc_block) <(render); then
+          echo "::error::proof-ledger: the Proof Ledger block in $DOC is not the rendering of $LEDGER; run scripts/proof-ledger.sh render --write"
+          exit 1
+        fi
+        echo "proof-ledger: $DOC block is current" ;;
+      --write)
+        [ -f "$DOC" ] || { echo "::error::proof-ledger: $DOC not found"; exit 2; }
+        if ! markers_ok; then
+          echo "::error::proof-ledger: $DOC lacks the generated-block markers, holds more than one pair, or has them out of order; it needs exactly one pair"; exit 2
+        fi
+        tmp=$(mktemp); blk=$(mktemp)
+        render > "$blk"
+        # The block is read from a file, not passed with -v: awk would
+        # process backslash escapes in a -v value.
+        awk -v b="$BEGIN_MARK" -v e="$END_MARK" '
+          NR == FNR { block = block $0 "\n"; next }
+          $0 == b { printf "%s", block; skip = 1; next }
+          $0 == e { skip = 0; next }
+          !skip { print }' "$blk" "$DOC" > "$tmp"
+        cat "$tmp" > "$DOC"; rm -f "$tmp" "$blk"
+        echo "proof-ledger: wrote the block into $DOC" ;;
+      *) echo "usage: $0 render [--check|--write]" >&2; exit 2 ;;
+    esac ;;
+  *) echo "usage: $0 check | render [--check|--write]" >&2; exit 2 ;;
+esac
diff --git a/tests/proof-ledger-test.sh b/tests/proof-ledger-test.sh
new file mode 100755
index 00000000..fc86d10e
--- /dev/null
+++ b/tests/proof-ledger-test.sh
@@ -0,0 +1,135 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Contracts of scripts/proof-ledger.sh: the real ledger passes, and every
+# planted defect (an overclaim, a vocabulary escape, a renamed proof, a
+# non-canonical line, a hand-edited table) turns it red.
+set -euo pipefail
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+cd "$repo_root"
+work="$(mktemp -d)"
+trap 'rm -rf -- "$work"' EXIT
+script="scripts/proof-ledger.sh"
+pass=0; fail=0
+
+expect() { # <label> <want-exit> <command...>
+  local label=$1 want=$2 rc=0
+  shift 2
+  "$@" >"$work/out" 2>&1 || rc=$?
+  if [ "$rc" -eq "$want" ]; then pass=$((pass + 1)); echo "  ok   $label"
+  else fail=$((fail + 1)); echo "  FAIL $label (exit $rc, wanted $want)" >&2; sed 's/^/       /' "$work/out" >&2; fi
+}
+
+
+# expect_msg <label> <want-exit> <pattern> <command...>: as expect, and the
+# output must name the rule (so another rule failing first cannot pass it).
+expect_msg() {
+  local label=$1 want=$2 pattern=$3 rc=0
+  shift 3
+  "$@" >"$work/out" 2>&1 || rc=$?
+  if [ "$rc" -eq "$want" ] && grep -qF -- "$pattern" "$work/out"; then pass=$((pass + 1)); echo "  ok   $label"
+  else fail=$((fail + 1)); echo "  FAIL $label (exit $rc, wanted $want with '$pattern')" >&2; sed 's/^/       /' "$work/out" >&2; fi
+}
+# mutate <name> <jq filter applied to the row whose id is $id> <id>
+mutate() {
+  jq -cS --arg id "$3" "if .id == \$id then $2 else . end" verification/proof-ledger.jsonl > "$work/$1.jsonl"
+}
+
+expect "the committed ledger is valid" 0 bash "$script" check
+expect "the committed PROOF-STATUS block is the ledger's rendering" 0 bash "$script" render --check
+
+mutate status-escape '.status = "COMPLETE"' abi-types
+expect "a status outside the closed vocabulary is refused" 1 env PROOF_LEDGER="$work/status-escape.jsonl" bash "$script" check
+
+mutate hidden-axioms '.status = "proven"' lean-rate-limiting
+expect "proven with axioms listed is refused (it is proven-with-postulates)" 1 env PROOF_LEDGER="$work/hidden-axioms.jsonl" bash "$script" check
+
+mutate unnamed-axioms '.axioms = []' lean-parser-totality
+expect "proven-with-postulates without its axioms is refused" 1 env PROOF_LEDGER="$work/unnamed-axioms.jsonl" bash "$script" check
+
+mutate renamed-proof '.names += ["noSuchTheorem"]' safety-triangle
+expect "a name the file does not hold is refused" 1 env PROOF_LEDGER="$work/renamed-proof.jsonl" bash "$script" check
+
+mutate missing-file '.file = "verification/proofs/idris2/Gone.idr"' quarantine
+expect "a file that does not exist is refused" 1 env PROOF_LEDGER="$work/missing-file.jsonl" bash "$script" check
+
+mutate unbounded-test '.bounds = ""' kin-gate
+expect "tested-only without bounds is refused" 1 env PROOF_LEDGER="$work/unbounded-test.jsonl" bash "$script" check
+
+mutate open-graded '.pwg = "3"' pagerank-convergence
+expect_msg "a PWG on an open theory row is refused" 1 "PWG-3 needs an Agda proof that is proven" env PROOF_LEDGER="$work/open-graded.jsonl" bash "$script" check
+
+mutate grade-without-leg '.pwg = "2i"' logtalk-migration
+expect "PWG-2i with no counted recheck leg is refused" 1 env PROOF_LEDGER="$work/grade-without-leg.jsonl" bash "$script" check
+
+mutate weak-agda '.checker = "Agda 2.8.0.2, --safe"' logtalk-migration
+expect "a PWG without the PROOF-POLICY 2.1 invocation is refused" 1 env PROOF_LEDGER="$work/weak-agda.jsonl" bash "$script" check
+
+mutate engineering-grade '.pwg = "3"' abi-ffi
+expect "a PWG on an engineering row is refused" 1 env PROOF_LEDGER="$work/engineering-grade.jsonl" bash "$script" check
+
+head -1 verification/proof-ledger.jsonl | jq . > "$work/pretty.jsonl"
+tail -n +2 verification/proof-ledger.jsonl >> "$work/pretty.jsonl"
+expect "a line not in canonical (JCS) form is refused" 1 env PROOF_LEDGER="$work/pretty.jsonl" bash "$script" check
+
+{ cat verification/proof-ledger.jsonl; head -1 verification/proof-ledger.jsonl; } > "$work/dup.jsonl"
+expect "a duplicate id is refused" 1 env PROOF_LEDGER="$work/dup.jsonl" bash "$script" check
+
+cp verification/PROOF-STATUS.adoc "$work/doc.adoc"
+sed -i '0,/^|proven$/s//|proven-with-postulates/' "$work/doc.adoc"
+expect "a hand edit to the rendered table is refused" 1 env PROOF_STATUS_DOC="$work/doc.adoc" bash "$script" render --check
+
+head -c -1 verification/proof-ledger.jsonl > "$work/no-lf.jsonl"
+expect_msg "a ledger without its final LF is refused" 1 "must end in exactly one LF" env PROOF_LEDGER="$work/no-lf.jsonl" bash "$script" check
+
+{ cat verification/proof-ledger.jsonl; echo; } > "$work/extra-lf.jsonl"
+expect_msg "a ledger with an extra final LF is refused" 1 "must end in exactly one LF" env PROOF_LEDGER="$work/extra-lf.jsonl" bash "$script" check
+
+mutate bad-type '.names = "connectorCount"' abi-types
+expect_msg "a mistyped field is reported (exit 1), not a jq crash" 1 "field names must be a array" env PROOF_LEDGER="$work/bad-type.jsonl" bash "$script" check
+if grep -q "jq: error" "$work/out"; then fail=$((fail + 1)); echo "  FAIL the mistyped row crashed jq" >&2; else pass=$((pass + 1)); echo "  ok   the mistyped row does not crash jq"; fi
+
+{ echo '{"id": oops'; cat verification/proof-ledger.jsonl; } > "$work/not-json.jsonl"
+expect_msg "a line that is not JSON is named, and the run stops there" 1 "line 1 is not JSON" env PROOF_LEDGER="$work/not-json.jsonl" bash "$script" check
+
+grep -v '^// END GENERATED: proof ledger$' verification/PROOF-STATUS.adoc > "$work/no-marker.adoc"
+expect_msg "render --check with a marker missing says to restore it (exit 2)" 2 "lacks the generated-block markers" env PROOF_STATUS_DOC="$work/no-marker.adoc" bash "$script" render --check
+
+{ echo '[]'; tail -n +2 verification/proof-ledger.jsonl; } > "$work/array-row.jsonl"
+expect_msg "a line that is JSON but not an object is refused" 1 "line 1 is not a JSON object" env PROOF_LEDGER="$work/array-row.jsonl" bash "$script" check
+
+mutate empty-checker '.checker = ""' abi-types
+expect_msg "a proven row with an empty checker is refused" 1 "are not empty" env PROOF_LEDGER="$work/empty-checker.jsonl" bash "$script" check
+
+mutate control-char '.obligation += "\n|open"' abi-types
+expect_msg "a control character in a field is refused" 1 "control character" env PROOF_LEDGER="$work/control-char.jsonl" bash "$script" check
+
+mutate number-leg '.legs = [{"axioms":[],"correspondence":"reconciled","prover":"rocq","route":"re-proved","status":"proven","receipt":1}]' logtalk-migration
+expect_msg "a number anywhere in a row is refused (jq -cS is JCS only without numbers)" 1 "holds no numbers" env PROOF_LEDGER="$work/number-leg.jsonl" bash "$script" check
+
+mutate asserted-leg '.pwg = "1" | .legs = [{"counts":true}]' logtalk-migration
+expect_msg "a leg that only asserts it counts is refused" 1 "unknown leg field(s) counts" env PROOF_LEDGER="$work/asserted-leg.jsonl" bash "$script" check
+
+mutate pending-leg '.pwg = "2i" | .legs = [{"axioms":[],"correspondence":"pending","prover":"rocq","route":"transported","status":"proven"}]' logtalk-migration
+expect_msg "a leg whose statement is not reconciled does not count" 1 "the legs support PWG-3" env PROOF_LEDGER="$work/pending-leg.jsonl" bash "$script" check
+
+mutate counted-leg '.pwg = "2i" | .legs = [{"axioms":[],"correspondence":"reconciled","prover":"rocq","route":"re-proved","status":"proven"}]' logtalk-migration
+expect "a reconciled, proven Rocq leg supports PWG-2i" 0 env PROOF_LEDGER="$work/counted-leg.jsonl" bash "$script" check
+
+mutate understated '.legs = [{"axioms":[],"correspondence":"reconciled","prover":"rocq","route":"re-proved","status":"proven"},{"axioms":[],"correspondence":"reconciled","prover":"lean","route":"re-proved","status":"proven"}]' logtalk-migration
+expect_msg "a grade below what the legs support is refused too (computed, not asserted)" 1 "the legs support PWG-2ii" env PROOF_LEDGER="$work/understated.jsonl" bash "$script" check
+
+mutate pwg-one '.pwg = "1" | .legs = [{"axioms":[],"correspondence":"reconciled","prover":"rocq","route":"re-proved","status":"proven"},{"axioms":[],"correspondence":"reconciled","prover":"lean","route":"re-proved","status":"proven"}]' logtalk-migration
+expect_msg "PWG-1 is refused while the ledger records no per-commit receipts" 1 "PWG-1 needs a current per-commit receipt" env PROOF_LEDGER="$work/pwg-one.jsonl" bash "$script" check
+
+mutate diverse-claim '.foundation_diverse = true' logtalk-migration
+expect_msg "+foundation-diverse without a counted other-foundation leg is refused" 1 "foundation_diverse is true exactly when" env PROOF_LEDGER="$work/diverse-claim.jsonl" bash "$script" check
+
+expect_msg "a missing PROOF-POLICY pin is refused (section 7)" 1 "pin is missing or malformed" env PROOF_POLICY_PIN="" bash "$script" check
+expect_msg "a pin without a full commit is refused" 1 "pin is missing or malformed" env PROOF_POLICY_PIN="metadatastician/standards 3-practice/PROOF-POLICY.adoc main" bash "$script" check
+
+{ cat verification/PROOF-STATUS.adoc; bash "$script" render; } > "$work/two-blocks.adoc"
+expect_msg "render --check refuses a second generated block" 2 "more than one pair" env PROOF_STATUS_DOC="$work/two-blocks.adoc" bash "$script" render --check
+
+echo "proof-ledger-test: $pass passed, $fail failed"
+[ "$fail" -eq 0 ]
diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index ea95851c..aceb5958 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -16,283 +16,305 @@ neurosymbolic CI/CD platform.
   Convert an earlier proof where possible; otherwise re-prove the theorem
   in Agda, then transport the witness to Rocq/Coq and Lean. Re-prove the
   same statement only when transport is unavailable or unsupported. A
-  translation alone is not a proof.
+  translation alone is not a proof. No Mathlib dependency.
 * Every Agda check runs: agda --safe --without-K --cubical-compatible
   against a pinned toolchain. Capital K is required.
 * For each target recheck, record the statement/assumption correspondence,
   checker version, exact invocation, receipt and source/witness digest.
   Missing tools, unchecked transports and unsuccessful checks are not
-  promoted to PROVEN. An unsuccessful translation does not refute or
+  promoted to `+proven+`. An unsuccessful translation does not refute or
   delete the earlier theorem.
 * Canonical estate policy:
   https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy].
   This file is a proof inventory, not an independent alternative policy.
-* Proof *grades* follow hyperpolymath/mathesis,
-  `+estate-mathematical-architecture+` §§5–6: *Grade 3* is an Agda proof
-  formulated and type-checking under the strict profile; *Grade 2*
-  requires translation(s) into independent foundational system(s);
-  *Grade 1* additionally requires those translated witnesses to compile
-  in headless, isolated CI via verified checker APIs. A target grade is
-  not a status. This inventory records exact statuses (Open / Claimed /
-  `+AGDA-PENDING+` / `+AGDA-VERIFIED+` / Grade 3 …) and never flattens
-  them into a confidence percentage.
+* *Statuses* use the closed vocabulary of README-EXPLAINME §5
+  (`+proven+`, `+proven-with-postulates+`, `+argued+`, `+tested-only+`,
+  `+open+`; PROOF-POLICY §5 gives the upper-case labels). A row that rests
+  on axioms names them, including the ones a Lean kernel adds
+  (`+propext+`, `+Quot.sound+`).
+* *Proof Witness Grades* follow PROOF-POLICY §8 and are always written
+  with their prefix (`+PWG-3+`, `+PWG-2i+`, `+PWG-2ii+`, `+PWG-1+`). They
+  are recorded for theory rows only, derived from receipts, and published
+  as a census, never as a percentage.
 * A checked model proves its stated proposition only. In particular it
   does not prove runtime refinement of Elixir/BEAM code; such claims
-  need their own correspondence evidence and tests.
+  need their own correspondence evidence and tests, and the ledger gives
+  them their own rows.
 
-NOTE: This repo verifies Idris2, Lean and TLA+ artefacts in CI, and —
-since 2026-11-01 — carries one narrowly scoped Agda artefact
-(`+LogtalkMigration.agda+`, below) gated by the same workflow. It does
-not yet run an Agda + Rocq + Lean reconciliation pipeline. The
-pre-existing Lean files below retain their documented scope; they must
-not be represented as independently rechecking Agda proofs until
-checked Agda sources and correspondence evidence actually exist.
+NOTE: This repo verifies Idris2, Lean and TLA+ artefacts in CI, and carries
+one narrowly scoped Agda artefact (`+LogtalkMigration.agda+`) gated by the
+same workflow. It does not yet run an Agda + Rocq + Lean reconciliation
+pipeline. The Lean files state engineering properties; they stay in Lean,
+labelled as such, until they are next touched (PROOF-POLICY §3). They are not
+recheck legs of any Agda proof.
 
-=== Proof Inventory
+// BEGIN GENERATED: scripts/proof-ledger.sh render (do not edit by hand)
+[[proof-ledger]]
+=== Proof Ledger
 
-==== Existing Proofs (pre-2026-04-04)
+Rendered from `+verification/proof-ledger.jsonl+`, which is canonical: where this table and the
+ledger disagree, the ledger wins and this table is regenerated.
+Checked against PROOF-POLICY as pinned by `+metadatastician/standards 3-practice/PROOF-POLICY.adoc b8f60511e76c9015d86990317162dce653c92fe1+`.
 
-NOTE: These tables deliberately carry no line-count column. Hand-maintained LOC
-figures drift silently, nothing consumes them, and sixteen of the twenty
-previously recorded here were wrong — some by more than double. Use `+wc -l+`
-on the paths below. (The four that were right were all tilde-approximations
-that happened to land within two lines; the column was still not worth keeping.)
+*Census:* 18 proven of 42; 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Theory rows: 3 (PWG-1 0, PWG-2ii 0, PWG-2i 0, PWG-3 1, ungraded 2).
 
-[width="100%",cols="28%,14%,42%,16%",options="header",]
+[cols="3,1,2,2,2",options="header"]
 |===
-|File |Language |Properties Proven |Status
-|`+src/Hypatia/ABI/Types.idr+` |Idris2 |Confidence refined type
-(`+So (value >= 0.0 && value <= 1.0)+` auto-proof), core data types,
-and the wire-contract pin `+connectorCount : length allConnectors = 16+`
-|COMPLETE
-
-|`+src/Hypatia/ABI/RuleEngine.idr+` |Idris2 |Safety triangle ordering,
-route totality, dispatch correctness, Bayesian monotonicity, annealing
-caps, end-to-end composition |COMPLETE
-
-|`+src/Hypatia/ABI/GraphQL.idr+` |Idris2 |Query/Mutation/Subscription
-type safety |COMPLETE
-
-|`+src/Hypatia/ABI/GRPC.idr+` |Idris2 |gRPC service type definitions
-|COMPLETE
-
-|`+src/Hypatia/ABI/REST.idr+` |Idris2 |REST endpoint type definitions
-|COMPLETE
-
-|`+src/Hypatia/ABI/FFI.idr+` |Idris2 |GADT constructors,
-`+ffiReturnsApiResponse+` proof |COMPLETE
-
-|`+verify/src/PipelineState.idr+` |Idris2 |Pipeline state machine
-(ValidTransition GADT), terminal/active classification |COMPLETE
-|===
-
-==== New Proofs (2026-04-04)
-
-[width="100%",cols="28%,14%,42%,16%",options="header",]
-|===
-|File |Language |Properties Proven |Status
-|`+verification/proofs/idris2/ConfidenceBounds.idr+` |Idris2
-|[0,1] bounds preserved by construction, Bayesian update,
-success/failure monotonicity, clamping, weighted average |COMPLETE
-
-|`+verification/proofs/idris2/SafetyTriangle.idr+` |Idris2 |Strict
-total order (irreflexive, asymmetric, transitive), trichotomy, routing
-respects hierarchy, optimality (highest available), completeness (all
-tiers reachable) |COMPLETE
-
-|`+verification/proofs/idris2/DispatchStrategy.idr+` |Idris2
-|Confidence-to-strategy monotonicity, boundary proofs (high/mid/low),
-annealing clamp bounds, nascent-never-auto, veteran-unrestricted
-|COMPLETE
-
-|`+verification/proofs/idris2/VerisimdbConnector.idr+` |Idris2
-|Completeness (mandatory fields), Soundness (missing fields rejected),
-Preservation of repo/file/category/severity under projection to the
-canonical JSON finding record (`+FindingFact+`). *Statement superseded
-2026-11-01:* the 2026-04-04 target was the retired Logtalk fact format
-(`+LogtalkFact+`); the equality proof term is unchanged, the target is
-now `+FindingFact+`, and the corresponding module is
-`+lib/verisim_connector.ex+`. Runtime refinement is not claimed.
-|COMPLETE (superseded statement; re-checked 2026-11-01 in Verify Proofs run 41328302925, idris2 --check job 124912804086, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331)
-
-|`+verification/proofs/idris2/Quarantine.idr+` |Idris2 |State
-transitions (ok/soft/hard/permanent), Auto-quarantine triggers, Release
-restoration, Routing blockage |COMPLETE
-
-|`+verification/proofs/idris2/BatchRollback.idr+` |Idris2
-|Transactionality (all-or-nothing), Reversibility (snapshot
-restoration), Fault tolerance (failure handling) |COMPLETE
-
-|`+verification/proofs/lean4/RateLimiting.lean+` |Lean 4 |Counter
-never exceeds configured bound, tryAccept preserves invariant, prune
-preserves invariant, inductive sequence processing, rejection guarantee,
-concrete configs (per-bot/global/burst) |COMPLETE
-
-|`+verification/proofs/lean4/BayesianUpdate.lean+` |Lean 4 |H7:
-posterior in (0,1), monotone in successes/failures, zero-observation
-identity, floor/cap clamp |COMPLETE
-
-|`+verification/proofs/lean4/ParserTotality.lean+` |Lean 4 |VCL
-`+FROM+`-clause parser totality, determinism, round-trip,
-malformed-input rejection |COMPLETE
-
-|`+verification/proofs/lean4/PageRankInvariants.lean+` |Lean 4
-|PageRank preconditions (edge-weight / out-degree non-negativity).
-*Convergence theorem in progress (Mathlib).* |PARTIAL
-
-|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |Lean 4
-|ESN scaling preconditions (floor-clamped denominator positive).
-*Echo-state stability in progress (Mathlib).* |PARTIAL
-
-|`+verification/proofs/idris2/NeuralConsensus.idr+` |Idris2 |H9:
-uniform-mean aggregation of Vect n Prediction is in [0,1], bounded below
-by n * min(inputs), denominator > 0 for non-empty ensembles, 8-network
-specialization |COMPLETE
-
-|`+verification/proofs/tlaplus/KinGate.tla+` |TLA+ |H8: Kin gate
-atomicity. Acquire/Release/Expire transitions + MutualExclusionByType +
-MutualExclusionBotView + ViewCoherentWithLocks + NoOrphanView +
-GrantsAreWellBracketed + EveryRequestProcessed (liveness) |COMPLETE —
-TLC model-check 2026-04-17 passed on 3 bots × 2 repos × MaxRequests=4:
-1,778,860 distinct states, depth 13, no errors in 51s (Eclipse Temurin
-21 JRE, tla2tools 2.19)
-
-|[line-through]#`+verification/proofs/agda/OutcomeLog.agda+`#
-|[line-through]#Agda# |[line-through]#H6: outcome
-log monotonicity (strictly increasing timestamps)# |RETIRED 2026-04-22 —
-downgraded to a runtime assertion in
-`+lib/outcome_tracker.ex:assert_h6_monotone/2+`. Echidnabot audits the
-JSONL for violations. See commit history.
-|===
-
-==== Logtalk → Elixir migration correspondence (2026-11-01)
-
-Finite, implementation-independent table correspondence for the retired
-ECHIDNA `+security_learning.lgt+` alert semantics versus
-`+Hypatia.Rules.SecurityErrors+`. Per the estate verifier mapping this
-is Agda territory; per Mathesis this is now *Grade 3* on the
-strict-profile receipt recorded in the row below (checker version,
-library discipline, exact invocation, result, source digest, and
-verification commit). Fix *strings* and Elixir
-runtime behaviour are outside the model and are pinned by the migration
-ledger and ExUnit tests respectively.
-
-[width="100%",cols="28%,14%,42%,16%",options="header",]
-|===
-|File |Language |Properties stated |Status
-|`+verification/proofs/agda/LogtalkMigration.agda+` |Agda
-|Exhaustive agreement over the 18 transcribed alert types:
-`+categoriesAgree+`, `+severitiesAgree+`, `+autoFixableAgrees+`,
-`+fixPresenceAgrees+`; prevention agreement on the six unchanged shared
-entries; the two ledgered non-equalities stated exactly
-(`+preventionBranchSource+`, `+preventionBranchTarget+`,
-`+preventionCodeReviewSource+`, `+preventionCodeReviewTarget+`); the
-former severity catch-all members explicit (`+catchAllSastLow+`,
-`+catchAllCiTestsLow+`, `+catchAllUnmaintainedLow+`). Source SHA-256
-(at authoring): bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0.
-|Grade 3 — AGDA-VERIFIED. Receipt: official pinned Agda 2.8.0.2 Linux
-release, builtins only/no stdlib; invocation `agda --safe --without-K
---cubical-compatible LogtalkMigration.agda`; success in Verify Proofs
-run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. No Grade 2/1,
-reconciliation, or runtime-refinement claim.
-|===
-
-==== Verdict support (2026-10-14, HYP-01)
-
-A gate verdict names its support: a pattern match, an observation count, or
-a prover re-check. Only the last can be sound. The statuses here use the
-estate vocabulary (PROVEN / TESTED / ASSUMED / OPEN), and every row names
-the artefact that justifies it. `+scripts/check-verdicts.sh+` (CI: `+idris2
---check+` job) and `+scripts/recheck-lean-hole.sh+` (CI: `+lake build+` job)
-are the gates.
-
-[width="100%",cols="28%,14%,42%,16%",options="header",]
-|===
-|File |Language |Claim |Status
-|`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |`+Sound+` has one
-constructor, indexed by `+Mechanical+`, demanding a re-check that
-`+Confirms+`: `+patternNotSound+`, `+observedNotSound+`,
-`+refutedNotSound+`; soundness is decidable (`+decSound+`); the derived
-level is "sound" only with a witness (`+soundLevelHasWitness+`,
-`+patternNeverSoundLevel+`, `+observedNeverSoundLevel+`) and a
-`+SoundVerdict+` always derives it (`+soundVerdictLevel+`); a `+Sha256+`
-literal of the wrong shape does not typecheck |PROVEN
-
-|`+tests/reject/PatternIsNotSound.idr+` |Idris2 |Expected rejection: a
-`+Sound+` witness for a `+Pattern+` support is refused at `+invalid+`
-|TESTED
-
-|`+tests/reject/ObservedIsNotSound.idr+` |Idris2 |Expected rejection:
-`+Observed+` 5 (the rules.a2ml proposal threshold) is refused as sound at
-`+invalid+` |TESTED
-
-|`+tests/reject/RefutedRecheckIsNotSound.idr+` |Idris2 |Expected
-rejection: a re-check that `+Refutes+` is refused as sound at `+invalid+`
-|TESTED
-
-|`+tests/reject/MalformedDigest.idr+` |Idris2 |Expected rejection: a
-digest that is not 64 lower-case hex digits is refused at `+invalid+`
-|TESTED
-
-|`+tests/accept/LeanHoleRecheckSound.idr+` |Idris2 + Lean 4 |Positive
-control: `+soundControl+`, a `+SoundVerdict+` for the code_safety Lean
-proof-hole detector, is accepted and derives "sound" by evaluation
-(`+controlIsSound+`); its `+targetHash+` and `+artefactHash+` are
-re-derived from a fresh Lean 4.30.0 run of the fixture, with two negative
-controls (a hole-free module prints no diagnostic; another run yields
-another digest) |TESTED
-
-|`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |Correspondence of
-`+Verdict+` / `+SoundVerdict+` to Epi / SoundWarrant in
-hyperpolymath/epistemic-types @ 6a68de3 (Warrant.agda). The pin and the
-cited names are checked (`+sibling-citations+` CI job); the
-correspondence is a transcription, not a checked proof |ASSUMED
-
-|`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |Elixir rules carry a proof of
-their support tag. They carry the tag only (HYP-01, PR B); no Elixir rule
-is proved sound |OPEN
-
-|`+src/Hypatia/ABI/Retraction.idr+` |Idris2 |Quarantine as retraction:
-a retraction is a thinning (`+retractThin+`); a token whose support thins
-into the retracted context survives on the same support
-(`+survivesDependent+`); a support naming an assumption that no longer
-occurs does not (`+thinElem+`, `+retractedSupportDies+`); a finding
-survives exactly through one of its tokens (`+survivor+`,
-`+noTokensNoSurvival+`) |PROVEN
-
-|`+tests/reject/RetractedSupportSurvives.idr+` |Idris2 |Expected
-rejection: a token resting on the very rule a quarantine retracts is
-refused as surviving, at `+invalid+` |TESTED
-
-|`+tests/accept/IndependentTokenSurvives.idr+` |Idris2 |Positive
-control: a finding corroborated by two rules survives the quarantine of
-one through the other (`+findingSurvives+`, `+survivesByB+`), and the
-token that rested on the quarantined rule does not (`+tokenADies+`)
-|TESTED
-
-|`+src/Hypatia/ABI/Retraction.idr+` |Idris2 |Correspondence of
-`+Retraction+`, `+Dependent+`, `+survivesDependent+` to Revision.agda in
-hyperpolymath/residual-evidence-types @ 97244f5. Pin and names checked
-(`+sibling-citations+` CI job); transcription, not a checked proof
-|ASSUMED
-
-|Runtime mirror, lib/hypatia/verdict/retraction.ex |Elixir |Quarantine
-retracts the findings that rested only on a quarantined rule, bot or
-prover, keeps corroborated findings on their surviving tokens, and
-restores them on release: test/retraction_test.exs, with the
-untouched-finding negative control and two mutants killed |TESTED
-
-|Runtime wiring |Elixir |`Quarantine.retract_dependents/1` is called by
-a scan or dispatch path. It is not, like the rest of the safety systems
-(CLAUDE.md Known Gap 2) |OPEN
-
-|Derived workflow steps, lib/dispatch_manifest.ex |Elixir |Every
-dispatch-manifest step names the verdict it derives from, and a factless
-step refuses the whole manifest before anything is written:
-test/dispatch_manifest_test.exs. This is hypatia's own derived workflow;
-the Signalbox criterion has no Signalbox repository to apply to |TESTED
-(Signalbox: OPEN)
+|Obligation |Status |Checker (version, flags) |Where |Trust boundary
+
+|Confidence is a refined value in [0,1]; the connector list is pinned at 16 entries
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/Types.idr+`: `+connectorCount+`
+|Types only; the Elixir, Zig and Rust sides are pinned to ffi/connectors.json by tests, not by this proof
+
+|Safety-triangle ordering is a strict order, routing is total and respects the hierarchy, dispatch thresholds are correct
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/RuleEngine.idr+`: `+triangleIrreflexive+`, `+triangleTransitive+`, `+routeRespectsHierarchy+`, `+routeTotality+`, `+eliminateFirst+`, `+controlOnlyAsFallback+`
+|Over the Idris2 model; the Elixir router is not shown to follow it (row models-runtime-refinement)
+
+|Every GraphQL query and mutation returns an ApiResponse
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/GraphQL.idr+`: `+queryReturnsApiResponse+`, `+mutationReturnsApiResponse+`
+|Operation types only; the served GraphQL schema is not checked against them
+
+|The gRPC service definitions are total and well typed
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/GRPC.idr+`: `+scannerService+`, `+dispatchService+`, `+streamService+`, `+healthService+`
+|Type definitions only; no property of a running service
+
+|The REST endpoint table is total and well typed
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/REST.idr+`: `+allEndpoints+`, `+totalEndpointCount+`
+|Type definitions only; the HTTP router is not checked against them
+
+|Every FFI call returns an ApiResponse
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/FFI.idr+`: `+ffiReturnsApiResponse+`
+|Over the GADT; the Zig exports are not checked against it
+
+|Pipeline states change only by valid transitions; terminal and active states are classified
+|proven
+|Idris2 0.7.0, idris2 --build verify/hypatia-verify.ipkg (--total)
+|`+verify/src/PipelineState.idr+`: `+transition+`, `+cancelRunning+`
+|Over the Idris2 state machine; the Elixir pipeline is not shown to follow it
+
+|Confidence stays in [0,1] under Bayesian success and failure updates, clamping and weighted averaging (P1)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/ConfidenceBounds.idr+`: `+successPreservesBounds+`, `+failurePreservesBounds+`, `+clampUpperBound+`
+|Over natural-number fractions; Elixir floats are not modelled
+
+|Tiers form a strict total order and routing picks the highest available tier (P2)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/SafetyTriangle.idr+`: `+tierGTIrreflexive+`, `+tierGTAsymmetric+`, `+tierGTTransitive+`, `+tierTrichotomy+`, `+eliminateAlwaysChosen+`
+|Over the Idris2 model; the Elixir TriangleRouter is not shown to follow it
+
+|Confidence maps monotonically to dispatch strategy at the 95/85 boundaries; nascent recipes never auto-execute (P3)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/DispatchStrategy.idr+`: `+highConfidenceIsAuto+`, `+midConfidenceIsReview+`, `+lowConfidenceIsReport+`
+|Over integer percentages; the Elixir FleetDispatcher is not shown to follow it
+
+|Raw records with every mandatory field parse, records missing one are rejected, and projection to FindingFact keeps repo, file, category and severity (P4; statement superseded 2026-11-01)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/VerisimdbConnector.idr+`: `+cleanFindingCompleteness+`, `+cleanFindingSoundness+`, `+factPreservesData+`, `+parseSeverityTotal+`
+|Over the Idris2 records; lib/verisim_connector.ex is not shown to follow them
+
+|Quarantine triggers, release and routing blockage behave as specified (P5)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/Quarantine.idr+`: `+failuresTriggerHard+`, `+highFPTriggersSoft+`, `+releaseRestoresOk+`, `+hardQuarantineBlocksAuto+`
+|Over the Idris2 model; lib/safety/quarantine.ex is not called by any dispatch path (CLAUDE.md Known Gap 2)
+
+|Batch execution is all-or-nothing and rollback restores the original snapshot (P6)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/BatchRollback.idr+`: `+rollbackRestoresOriginal+`, `+reversibility+`, `+batchIsTransactional+`
+|Over the Idris2 model; lib/safety/batch_rollback.ex is not called by any dispatch path
+
+|Uniform-mean aggregation of n predictions stays in [0,1] and above n times the minimum (H9)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/NeuralConsensus.idr+`: `+sumPredsBounded+`, `+aggregateInBounds+`, `+minLteLeft+`
+|Over natural-number predictions; the Elixir coordinator's floats are not modelled
+
+|Only a confirming mechanical re-check makes a verdict sound; soundness is decidable (HYP-01)
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/Verdict.idr+`: `+patternNotSound+`, `+observedNotSound+`, `+refutedNotSound+`, `+decSound+`, `+soundLevelHasWitness+`, `+soundVerdictLevel+`
+|Over the Idris2 types; lib/hypatia/verdict.ex mirrors them by hand
+
+|A Sound witness for Pattern support does not typecheck
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh
+|`+tests/reject/PatternIsNotSound.idr+`: `+invalid+`
+|One negative example, not a proof over all inputs. Bounds: one expected-rejection check per CI run
+
+|Observed 5 (the proposal threshold) is refused as sound
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh
+|`+tests/reject/ObservedIsNotSound.idr+`: `+invalid+`
+|One negative example, not a proof over all inputs. Bounds: one expected-rejection check per CI run
+
+|A re-check that refutes is refused as sound
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh
+|`+tests/reject/RefutedRecheckIsNotSound.idr+`: `+invalid+`
+|One negative example, not a proof over all inputs. Bounds: one expected-rejection check per CI run
+
+|A digest that is not 64 lower-case hex digits does not typecheck
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh
+|`+tests/reject/MalformedDigest.idr+`: `+invalid+`
+|One negative example, not a proof over all inputs. Bounds: one expected-rejection check per CI run
+
+|A SoundVerdict for the Lean proof-hole detector is accepted and derives sound, with digests re-derived from a fresh Lean run
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh; Lean 4.30.0, scripts/recheck-lean-hole.sh
+|`+tests/accept/LeanHoleRecheckSound.idr+`: `+soundControl+`, `+controlIsSound+`
+|One detector and one fixture. Bounds: one positive control and two negative controls per CI run
+
+|Verdict and SoundVerdict correspond to Epi and SoundWarrant in hyperpolymath/epistemic-types at 6a68de3 (Warrant.agda)
+|argued
+|-
+|`+src/Hypatia/ABI/Verdict.idr+`: `+SoundVerdict+`
+|A transcription; the pin and the cited names are checked by the sibling-citations CI job, the correspondence is not
+
+|Elixir rules are proved sound for the support they carry
+|open
+|-
+|`+src/Hypatia/ABI/Verdict.idr+`: `+Verdict+`
+|Rules carry only the support tag (HYP-01, PR B); no Elixir rule is proved sound
+
+|A quarantine retraction is a thinning: a token survives on the same support iff its support thins into what remains, and a finding survives through one of its tokens
+|proven
+|Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)
+|`+src/Hypatia/ABI/Retraction.idr+`: `+retractThin+`, `+survivesDependent+`, `+thinElem+`, `+retractedSupportDies+`, `+survivor+`, `+noTokensNoSurvival+`
+|Over the Idris2 types; the runtime mirror is a separate row
+
+|A token resting on the retracted rule is refused as surviving
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh
+|`+tests/reject/RetractedSupportSurvives.idr+`: `+invalid+`
+|One negative example. Bounds: one expected-rejection check per CI run
+
+|A finding corroborated by two rules survives the quarantine of one through the other
+|tested-only
+|Idris2 0.7.0, scripts/check-verdicts.sh
+|`+tests/accept/IndependentTokenSurvives.idr+`: `+findingSurvives+`, `+survivesByB+`, `+tokenADies+`
+|One positive example. Bounds: one positive control per CI run
+
+|Retraction, Dependent and survivesDependent correspond to Revision.agda in hyperpolymath/residual-evidence-types at 97244f5
+|argued
+|-
+|`+src/Hypatia/ABI/Retraction.idr+`: `+survivesDependent+`
+|A transcription; the pin and names are checked by the sibling-citations CI job, the correspondence is not
+
+|The Elixir mirror retracts findings resting only on a quarantined rule, bot or prover, keeps corroborated ones, and restores them on release
+|tested-only
+|ExUnit (mix test)
+|`+test/retraction_test.exs+`: `+retract_dependents+`
+|Example-based; lib/hypatia/verdict/retraction.ex is not proved. Bounds: ExUnit cases with an untouched-finding negative control; two mutants killed
+
+|Quarantine.retract_dependents/1 is called by a scan or dispatch path
+|open
+|-
+|`+lib/safety/quarantine.ex+`: `+retract_dependents+`
+|Not wired, like the rest of the safety systems (CLAUDE.md Known Gap 2)
+
+|Every dispatch-manifest step names the verdict it derives from, and a factless step refuses the whole manifest before anything is written
+|tested-only
+|ExUnit (mix test)
+|`+test/dispatch_manifest_test.exs+`: `+DispatchManifest+`
+|Hypatia's own derived workflow only. Bounds: ExUnit cases
+
+|The Signalbox derived-workflow criterion holds
+|open
+|-
+|`+test/dispatch_manifest_test.exs+`: `+DispatchManifest+`
+|There is no Signalbox repository to apply the criterion to
+
+|The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)
+|proven-with-postulates (Quot.sound, propext)
+|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
+|`+verification/proofs/lean4/RateLimiting.lean+`: `+tryAccept_preserves_invariant+`, `+prune_preserves_invariant+`, `+processEvents_preserves_invariant+`, `+at_limit_rejects+`, `+count_bounded_after_accepts+`
+|Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Interface engineering in Lean: moves to Idris2 when next touched (PROOF-POLICY section 3)
+
+|The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)
+|proven-with-postulates (Quot.sound, propext)
+|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
+|`+verification/proofs/lean4/BayesianUpdate.lean+`: `+posterior_lt_one+`, `+posterior_pos+`, `+more_successes_raises+`, `+more_failures_lowers+`, `+clamp_ge_floor+`, `+clamp_le_cap+`, `+bayesian_update_sound+`
+|Over Nat pseudo-counts; Elixir floats are not modelled. Moves to Idris2 when next touched (PROOF-POLICY section 3)
+
+|The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input
+|proven-with-postulates (propext)
+|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
+|`+verification/proofs/lean4/ParserTotality.lean+`: `+parseFrom_deterministic+`, `+parseFrom_passes_remainder+`, `+parseFrom_orphan_from+`, `+parseFrom_no_from_keyword+`
+|FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moves to Idris2 when next touched (PROOF-POLICY section 3)
+
+|PageRank inputs are well formed: edge weights and in/out weight sums are non-negative
+|proven
+|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
+|`+verification/proofs/lean4/PageRankInvariants.lean+`: `+edge_weight_nonneg+`, `+outWeightSum_nonneg+`, `+inWeightSum_nonneg+`, `+pagerank_preconditions_sound+`
+|Preconditions only; convergence is row pagerank-convergence
+
+|ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs
+|proven-with-postulates (propext)
+|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
+|`+verification/proofs/lean4/ESNSpectralScaling.lean+`: `+denom_pos_when_floor_pos+`, `+denom_ge_maxAbs+`, `+denom_ge_floor+`, `+esn_scaling_preconditions_sound+`
+|Preconditions only; echo-state stability is row esn-echo-state
+
+|Kin-gate atomicity: mutual exclusion by type and in the bot view, view coherent with locks, no orphan view, well-bracketed grants, and every request processed (H8)
+|tested-only
+|TLC 2.19 (rev 5a47802), -workers auto -config KinGate.cfg
+|`+verification/proofs/tlaplus/KinGate.tla+`: `+KinGateSafe+`, `+MutualExclusionByType+`, `+MutualExclusionBotView+`, `+ViewCoherentWithLocks+`, `+NoOrphanView+`, `+GrantsAreWellBracketed+`, `+EveryRequestProcessed+`
+|One bounded instance; the Elixir kin gate is not shown to follow the spec. Bounds: 3 bots x 2 repos, MaxRequests = 4: 444715 distinct states, depth 13, no error
+
+|The 18 transcribed alert types agree between security_learning.lgt and Hypatia.Rules.SecurityErrors on category, severity, auto-fixability and fix presence; prevention agrees except the two ledgered non-equalities
+|proven, PWG-3
+|Agda 2.8.0.2, builtins only, --safe --without-K --cubical-compatible
+|`+verification/proofs/agda/LogtalkMigration.agda+`: `+categoriesAgree+`, `+severitiesAgree+`, `+autoFixableAgrees+`, `+fixPresenceAgrees+`, `+preventionAgreesToken+`, `+preventionAgreesPinned+`, `+preventionAgreesMissing+`, `+preventionAgreesHardCoded+`, `+preventionAgreesVulnerabilities+`, `+preventionAgreesSecurityPolicy+`, `+preventionBranchSource+`, `+preventionBranchTarget+`, `+preventionCodeReviewSource+`, `+preventionCodeReviewTarget+`
+|The finite table as transcribed; fix strings and Elixir runtime behaviour are outside the model. No Rocq or Lean leg yet
+
+|Hypatia.Rules.SecurityErrors at runtime follows the table the Agda model states
+|tested-only
+|ExUnit (mix test)
+|`+test/security_errors_test.exs+`: `+SecurityErrors+`
+|Example-based; the transcription into the Agda table is not itself checked. Bounds: ExUnit cases over the migrated alert types
+
+|Damped PageRank iteration converges to a unique stationary vector
+|open, ungraded
+|-
+|-
+|Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib
+
+|With leak rate 0 < a <= 1 and the reservoir scaled to infinity-norm at most 0.95, two state trajectories under the same input converge geometrically (echo-state property), and [-1,1]^n is invariant
+|open, ungraded
+|-
+|-
+|Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib. The runtime scales by the induced infinity-norm, not the spectral radius
+
+|The Elixir runtime follows the Idris2, Lean and TLA+ models above
+|open
+|-
+|-
+|No correspondence evidence beyond the rows that name a runtime test; a model row proves its model only (README-EXPLAINME section 5 rule 3)
+
+|VCL queries return what their semantics says beyond the FROM clause
+|open
+|-
+|`+lib/vcl/query.ex+`: `+fetch_scans+`
+|Only FROM-clause parsing is modelled (row lean-parser-totality)
 |===
+// END GENERATED: proof ledger
 
 === Properties Proven
 
@@ -376,12 +398,18 @@ list)
 rejected
 * *P7.6* Count bounded after any sequence of accepts
 
+Status for all of P7: `proven-with-postulates`. The proofs rest on the Lean
+kernel axioms `propext` and `Quot.sound` (`at_limit_rejects` on
+`propext` only), as `Lean.collectAxioms` reports under Lean 4.30.0.
+
 ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`)
 
-Status for all of P8: *Grade 3 — AGDA-VERIFIED* on the strict-profile
-receipt in the inventory row above (Agda 2.8.0.2, Verify Proofs run
-41328302925, job 124912804344, commit 4018290eaa3265b82209e2a45b6917a4bb0a0331). This grades the finite
-model only.
+Status for all of P8: `proven`, *PWG-3* (AGDA-VERIFIED), on the
+strict-profile receipt: Agda 2.8.0.2, builtins only, Verify Proofs run
+41328302925, job 124912804344, commit 4018290eaa3265b82209e2a45b6917a4bb0a0331,
+source SHA-256 bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0.
+This grades the finite model only. PWG-3 is not a discharge: the Rocq and
+Lean legs are still owed (PROOF-POLICY §8.4).
 
 * *P8.1* Category correspondence: `+categoriesAgree+`
 * *P8.2* Severity correspondence, including the former catch-all:
@@ -412,56 +440,12 @@ model only.
 |`+Obj.magic+` |0 |-
 |===
 
-=== Coverage Map
-
-[width="100%",cols="48%,27%,25%",options="header",]
-|===
-|Hypatia Subsystem |Proven By |Coverage
-|Confidence values |`+ConfidenceBounds.idr+`, `+RuleEngine.idr+` |Full
-
-|Safety triangle routing |`+SafetyTriangle.idr+`, `+RuleEngine.idr+`
-|Full
-
-|Dispatch strategy mapping |`+DispatchStrategy.idr+`, `+RuleEngine.idr+`
-|Full
-
-|Rate limiting |`+RateLimiting.lean+` |Full
-
-|Pipeline state machine |`+PipelineState.idr+` |Full
-
-|Bayesian confidence updating |`+ConfidenceBounds.idr+`,
-`+RuleEngine.idr+` |Full
-
-|Bot dispatch correctness |`+RuleEngine.idr+` |Full
-
-|Annealing stage caps |`+DispatchStrategy.idr+`, `+RuleEngine.idr+`
-|Full
+=== Coverage
 
-|API type safety |`+Types.idr+`, `+GraphQL.idr+`, `+REST.idr+`,
-`+GRPC.idr+`, `+FFI.idr+` |Full
-
-|Quarantine logic |`+Quarantine.idr+` |Full
-
-|Batch rollback |`+BatchRollback.idr+` |Full
-
-|VeriSimDB connector |`+VerisimdbConnector.idr+` |Full (model; statement
-superseded 2026-11-01)
-
-|Logtalk → Elixir alert-table correspondence
-|`+LogtalkMigration.agda+` |Finite model only — Grade 3 /
-AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded
-
-|Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds +
-min-lower-bound)
-
-|VCL parser totality |`+ParserTotality.lean+` |Full (FROM-clause subset)
-
-|VCL query correctness |- |Partial
-
-|Neural network convergence |`+PageRankInvariants.lean+`,
-`+ESNSpectralScaling.lean+` |Preconditions proven; full
-convergence/stability in progress (Lean + Mathlib)
-|===
+Coverage is the Proof Ledger above. A row covers its own model; whether the
+Elixir runtime follows a model is a separate row (`+models-runtime-refinement+`,
+and the rows that name a runtime test). The earlier hand-written coverage map
+marked models "Full" without that evidence and has been retired.
 
 === File Locations
 
diff --git a/verification/proof-ledger.jsonl b/verification/proof-ledger.jsonl
new file mode 100644
index 00000000..04c78200
--- /dev/null
+++ b/verification/proof-ledger.jsonl
@@ -0,0 +1,42 @@
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/Types.idr","id":"abi-types","kind":"engineering","names":["connectorCount"],"obligation":"Confidence is a refined value in [0,1]; the connector list is pinned at 16 entries","status":"proven","trust_boundary":"Types only; the Elixir, Zig and Rust sides are pinned to ffi/connectors.json by tests, not by this proof"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/RuleEngine.idr","id":"abi-rule-engine","kind":"engineering","names":["triangleIrreflexive","triangleTransitive","routeRespectsHierarchy","routeTotality","eliminateFirst","controlOnlyAsFallback"],"obligation":"Safety-triangle ordering is a strict order, routing is total and respects the hierarchy, dispatch thresholds are correct","status":"proven","trust_boundary":"Over the Idris2 model; the Elixir router is not shown to follow it (row models-runtime-refinement)"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/GraphQL.idr","id":"abi-graphql","kind":"engineering","names":["queryReturnsApiResponse","mutationReturnsApiResponse"],"obligation":"Every GraphQL query and mutation returns an ApiResponse","status":"proven","trust_boundary":"Operation types only; the served GraphQL schema is not checked against them"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/GRPC.idr","id":"abi-grpc","kind":"engineering","names":["scannerService","dispatchService","streamService","healthService"],"obligation":"The gRPC service definitions are total and well typed","status":"proven","trust_boundary":"Type definitions only; no property of a running service"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/REST.idr","id":"abi-rest","kind":"engineering","names":["allEndpoints","totalEndpointCount"],"obligation":"The REST endpoint table is total and well typed","status":"proven","trust_boundary":"Type definitions only; the HTTP router is not checked against them"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/FFI.idr","id":"abi-ffi","kind":"engineering","names":["ffiReturnsApiResponse"],"obligation":"Every FFI call returns an ApiResponse","status":"proven","trust_boundary":"Over the GADT; the Zig exports are not checked against it"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build verify/hypatia-verify.ipkg (--total)","file":"verify/src/PipelineState.idr","id":"pipeline-state","kind":"engineering","names":["transition","cancelRunning"],"obligation":"Pipeline states change only by valid transitions; terminal and active states are classified","status":"proven","trust_boundary":"Over the Idris2 state machine; the Elixir pipeline is not shown to follow it"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/ConfidenceBounds.idr","id":"confidence-bounds","kind":"engineering","names":["successPreservesBounds","failurePreservesBounds","clampUpperBound"],"obligation":"Confidence stays in [0,1] under Bayesian success and failure updates, clamping and weighted averaging (P1)","status":"proven","trust_boundary":"Over natural-number fractions; Elixir floats are not modelled"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/SafetyTriangle.idr","id":"safety-triangle","kind":"engineering","names":["tierGTIrreflexive","tierGTAsymmetric","tierGTTransitive","tierTrichotomy","eliminateAlwaysChosen"],"obligation":"Tiers form a strict total order and routing picks the highest available tier (P2)","status":"proven","trust_boundary":"Over the Idris2 model; the Elixir TriangleRouter is not shown to follow it"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/DispatchStrategy.idr","id":"dispatch-strategy","kind":"engineering","names":["highConfidenceIsAuto","midConfidenceIsReview","lowConfidenceIsReport"],"obligation":"Confidence maps monotonically to dispatch strategy at the 95/85 boundaries; nascent recipes never auto-execute (P3)","status":"proven","trust_boundary":"Over integer percentages; the Elixir FleetDispatcher is not shown to follow it"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/VerisimdbConnector.idr","id":"verisimdb-connector","kind":"engineering","names":["cleanFindingCompleteness","cleanFindingSoundness","factPreservesData","parseSeverityTotal"],"obligation":"Raw records with every mandatory field parse, records missing one are rejected, and projection to FindingFact keeps repo, file, category and severity (P4; statement superseded 2026-11-01)","status":"proven","trust_boundary":"Over the Idris2 records; lib/verisim_connector.ex is not shown to follow them"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/Quarantine.idr","id":"quarantine","kind":"engineering","names":["failuresTriggerHard","highFPTriggersSoft","releaseRestoresOk","hardQuarantineBlocksAuto"],"obligation":"Quarantine triggers, release and routing blockage behave as specified (P5)","status":"proven","trust_boundary":"Over the Idris2 model; lib/safety/quarantine.ex is not called by any dispatch path (CLAUDE.md Known Gap 2)"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/BatchRollback.idr","id":"batch-rollback","kind":"engineering","names":["rollbackRestoresOriginal","reversibility","batchIsTransactional"],"obligation":"Batch execution is all-or-nothing and rollback restores the original snapshot (P6)","status":"proven","trust_boundary":"Over the Idris2 model; lib/safety/batch_rollback.ex is not called by any dispatch path"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/NeuralConsensus.idr","id":"neural-consensus","kind":"engineering","names":["sumPredsBounded","aggregateInBounds","minLteLeft"],"obligation":"Uniform-mean aggregation of n predictions stays in [0,1] and above n times the minimum (H9)","status":"proven","trust_boundary":"Over natural-number predictions; the Elixir coordinator's floats are not modelled"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/Verdict.idr","id":"verdict-sound","kind":"engineering","names":["patternNotSound","observedNotSound","refutedNotSound","decSound","soundLevelHasWitness","soundVerdictLevel"],"obligation":"Only a confirming mechanical re-check makes a verdict sound; soundness is decidable (HYP-01)","status":"proven","trust_boundary":"Over the Idris2 types; lib/hypatia/verdict.ex mirrors them by hand"}
+{"axioms":[],"bounds":"one expected-rejection check per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh","file":"tests/reject/PatternIsNotSound.idr","id":"verdict-reject-pattern","kind":"engineering","names":["invalid"],"obligation":"A Sound witness for Pattern support does not typecheck","status":"tested-only","trust_boundary":"One negative example, not a proof over all inputs"}
+{"axioms":[],"bounds":"one expected-rejection check per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh","file":"tests/reject/ObservedIsNotSound.idr","id":"verdict-reject-observed","kind":"engineering","names":["invalid"],"obligation":"Observed 5 (the proposal threshold) is refused as sound","status":"tested-only","trust_boundary":"One negative example, not a proof over all inputs"}
+{"axioms":[],"bounds":"one expected-rejection check per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh","file":"tests/reject/RefutedRecheckIsNotSound.idr","id":"verdict-reject-refuted","kind":"engineering","names":["invalid"],"obligation":"A re-check that refutes is refused as sound","status":"tested-only","trust_boundary":"One negative example, not a proof over all inputs"}
+{"axioms":[],"bounds":"one expected-rejection check per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh","file":"tests/reject/MalformedDigest.idr","id":"verdict-reject-digest","kind":"engineering","names":["invalid"],"obligation":"A digest that is not 64 lower-case hex digits does not typecheck","status":"tested-only","trust_boundary":"One negative example, not a proof over all inputs"}
+{"axioms":[],"bounds":"one positive control and two negative controls per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh; Lean 4.30.0, scripts/recheck-lean-hole.sh","file":"tests/accept/LeanHoleRecheckSound.idr","id":"verdict-accept-lean-hole","kind":"engineering","names":["soundControl","controlIsSound"],"obligation":"A SoundVerdict for the Lean proof-hole detector is accepted and derives sound, with digests re-derived from a fresh Lean run","status":"tested-only","trust_boundary":"One detector and one fixture"}
+{"axioms":[],"bounds":"","checker":"-","file":"src/Hypatia/ABI/Verdict.idr","id":"verdict-epistemic-correspondence","kind":"engineering","names":["SoundVerdict"],"obligation":"Verdict and SoundVerdict correspond to Epi and SoundWarrant in hyperpolymath/epistemic-types at 6a68de3 (Warrant.agda)","status":"argued","trust_boundary":"A transcription; the pin and the cited names are checked by the sibling-citations CI job, the correspondence is not"}
+{"axioms":[],"bounds":"","checker":"-","file":"src/Hypatia/ABI/Verdict.idr","id":"elixir-rules-support","kind":"engineering","names":["Verdict"],"obligation":"Elixir rules are proved sound for the support they carry","status":"open","trust_boundary":"Rules carry only the support tag (HYP-01, PR B); no Elixir rule is proved sound"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --build src/abi/hypatia-abi.ipkg (--total)","file":"src/Hypatia/ABI/Retraction.idr","id":"retraction","kind":"engineering","names":["retractThin","survivesDependent","thinElem","retractedSupportDies","survivor","noTokensNoSurvival"],"obligation":"A quarantine retraction is a thinning: a token survives on the same support iff its support thins into what remains, and a finding survives through one of its tokens","status":"proven","trust_boundary":"Over the Idris2 types; the runtime mirror is a separate row"}
+{"axioms":[],"bounds":"one expected-rejection check per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh","file":"tests/reject/RetractedSupportSurvives.idr","id":"retraction-reject","kind":"engineering","names":["invalid"],"obligation":"A token resting on the retracted rule is refused as surviving","status":"tested-only","trust_boundary":"One negative example"}
+{"axioms":[],"bounds":"one positive control per CI run","checker":"Idris2 0.7.0, scripts/check-verdicts.sh","file":"tests/accept/IndependentTokenSurvives.idr","id":"retraction-accept","kind":"engineering","names":["findingSurvives","survivesByB","tokenADies"],"obligation":"A finding corroborated by two rules survives the quarantine of one through the other","status":"tested-only","trust_boundary":"One positive example"}
+{"axioms":[],"bounds":"","checker":"-","file":"src/Hypatia/ABI/Retraction.idr","id":"retraction-residual-correspondence","kind":"engineering","names":["survivesDependent"],"obligation":"Retraction, Dependent and survivesDependent correspond to Revision.agda in hyperpolymath/residual-evidence-types at 97244f5","status":"argued","trust_boundary":"A transcription; the pin and names are checked by the sibling-citations CI job, the correspondence is not"}
+{"axioms":[],"bounds":"ExUnit cases with an untouched-finding negative control; two mutants killed","checker":"ExUnit (mix test)","file":"test/retraction_test.exs","id":"retraction-runtime-mirror","kind":"engineering","names":["retract_dependents"],"obligation":"The Elixir mirror retracts findings resting only on a quarantined rule, bot or prover, keeps corroborated ones, and restores them on release","status":"tested-only","trust_boundary":"Example-based; lib/hypatia/verdict/retraction.ex is not proved"}
+{"axioms":[],"bounds":"","checker":"-","file":"lib/safety/quarantine.ex","id":"retraction-runtime-wiring","kind":"engineering","names":["retract_dependents"],"obligation":"Quarantine.retract_dependents/1 is called by a scan or dispatch path","status":"open","trust_boundary":"Not wired, like the rest of the safety systems (CLAUDE.md Known Gap 2)"}
+{"axioms":[],"bounds":"ExUnit cases","checker":"ExUnit (mix test)","file":"test/dispatch_manifest_test.exs","id":"dispatch-manifest-steps","kind":"engineering","names":["DispatchManifest"],"obligation":"Every dispatch-manifest step names the verdict it derives from, and a factless step refuses the whole manifest before anything is written","status":"tested-only","trust_boundary":"Hypatia's own derived workflow only"}
+{"axioms":[],"bounds":"","checker":"-","file":"test/dispatch_manifest_test.exs","id":"signalbox","kind":"engineering","names":["DispatchManifest"],"obligation":"The Signalbox derived-workflow criterion holds","status":"open","trust_boundary":"There is no Signalbox repository to apply the criterion to"}
+{"axioms":["Quot.sound","propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/RateLimiting.lean","id":"lean-rate-limiting","kind":"engineering","names":["tryAccept_preserves_invariant","prune_preserves_invariant","processEvents_preserves_invariant","at_limit_rejects","count_bounded_after_accepts"],"obligation":"The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)","status":"proven-with-postulates","trust_boundary":"Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Interface engineering in Lean: moves to Idris2 when next touched (PROOF-POLICY section 3)"}
+{"axioms":["Quot.sound","propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/BayesianUpdate.lean","id":"lean-bayesian-update","kind":"engineering","names":["posterior_lt_one","posterior_pos","more_successes_raises","more_failures_lowers","clamp_ge_floor","clamp_le_cap","bayesian_update_sound"],"obligation":"The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)","status":"proven-with-postulates","trust_boundary":"Over Nat pseudo-counts; Elixir floats are not modelled. Moves to Idris2 when next touched (PROOF-POLICY section 3)"}
+{"axioms":["propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/ParserTotality.lean","id":"lean-parser-totality","kind":"engineering","names":["parseFrom_deterministic","parseFrom_passes_remainder","parseFrom_orphan_from","parseFrom_no_from_keyword"],"obligation":"The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input","status":"proven-with-postulates","trust_boundary":"FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moves to Idris2 when next touched (PROOF-POLICY section 3)"}
+{"axioms":[],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/PageRankInvariants.lean","id":"lean-pagerank-preconditions","kind":"engineering","names":["edge_weight_nonneg","outWeightSum_nonneg","inWeightSum_nonneg","pagerank_preconditions_sound"],"obligation":"PageRank inputs are well formed: edge weights and in/out weight sums are non-negative","status":"proven","trust_boundary":"Preconditions only; convergence is row pagerank-convergence"}
+{"axioms":["propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/ESNSpectralScaling.lean","id":"lean-esn-preconditions","kind":"engineering","names":["denom_pos_when_floor_pos","denom_ge_maxAbs","denom_ge_floor","esn_scaling_preconditions_sound"],"obligation":"ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs","status":"proven-with-postulates","trust_boundary":"Preconditions only; echo-state stability is row esn-echo-state"}
+{"axioms":[],"bounds":"3 bots x 2 repos, MaxRequests = 4: 444715 distinct states, depth 13, no error","checker":"TLC 2.19 (rev 5a47802), -workers auto -config KinGate.cfg","file":"verification/proofs/tlaplus/KinGate.tla","id":"kin-gate","kind":"engineering","names":["KinGateSafe","MutualExclusionByType","MutualExclusionBotView","ViewCoherentWithLocks","NoOrphanView","GrantsAreWellBracketed","EveryRequestProcessed"],"obligation":"Kin-gate atomicity: mutual exclusion by type and in the bot view, view coherent with locks, no orphan view, well-bracketed grants, and every request processed (H8)","status":"tested-only","trust_boundary":"One bounded instance; the Elixir kin gate is not shown to follow the spec"}
+{"axioms":[],"bounds":"","checker":"Agda 2.8.0.2, builtins only, --safe --without-K --cubical-compatible","file":"verification/proofs/agda/LogtalkMigration.agda","foundation_diverse":false,"id":"logtalk-migration","kind":"theory","legs":[],"names":["categoriesAgree","severitiesAgree","autoFixableAgrees","fixPresenceAgrees","preventionAgreesToken","preventionAgreesPinned","preventionAgreesMissing","preventionAgreesHardCoded","preventionAgreesVulnerabilities","preventionAgreesSecurityPolicy","preventionBranchSource","preventionBranchTarget","preventionCodeReviewSource","preventionCodeReviewTarget"],"obligation":"The 18 transcribed alert types agree between security_learning.lgt and Hypatia.Rules.SecurityErrors on category, severity, auto-fixability and fix presence; prevention agrees except the two ledgered non-equalities","pwg":"3","status":"proven","trust_boundary":"The finite table as transcribed; fix strings and Elixir runtime behaviour are outside the model. No Rocq or Lean leg yet"}
+{"axioms":[],"bounds":"ExUnit cases over the migrated alert types","checker":"ExUnit (mix test)","file":"test/security_errors_test.exs","id":"logtalk-runtime","kind":"engineering","names":["SecurityErrors"],"obligation":"Hypatia.Rules.SecurityErrors at runtime follows the table the Agda model states","status":"tested-only","trust_boundary":"Example-based; the transcription into the Agda table is not itself checked"}
+{"axioms":[],"bounds":"","checker":"-","file":"-","foundation_diverse":false,"id":"pagerank-convergence","kind":"theory","legs":[],"names":[],"obligation":"Damped PageRank iteration converges to a unique stationary vector","pwg":"ungraded","status":"open","trust_boundary":"Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib"}
+{"axioms":[],"bounds":"","checker":"-","file":"-","foundation_diverse":false,"id":"esn-echo-state","kind":"theory","legs":[],"names":[],"obligation":"With leak rate 0 < a <= 1 and the reservoir scaled to infinity-norm at most 0.95, two state trajectories under the same input converge geometrically (echo-state property), and [-1,1]^n is invariant","pwg":"ungraded","status":"open","trust_boundary":"Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib. The runtime scales by the induced infinity-norm, not the spectral radius"}
+{"axioms":[],"bounds":"","checker":"-","file":"-","id":"models-runtime-refinement","kind":"engineering","names":[],"obligation":"The Elixir runtime follows the Idris2, Lean and TLA+ models above","status":"open","trust_boundary":"No correspondence evidence beyond the rows that name a runtime test; a model row proves its model only (README-EXPLAINME section 5 rule 3)"}
+{"axioms":[],"bounds":"","checker":"-","file":"lib/vcl/query.ex","id":"vcl-query-correctness","kind":"engineering","names":["fetch_scans"],"obligation":"VCL queries return what their semantics says beyond the FROM clause","status":"open","trust_boundary":"Only FROM-clause parsing is modelled (row lean-parser-totality)"}
diff --git a/verification/proofs/tlaplus/README.adoc b/verification/proofs/tlaplus/README.adoc
index 61db0ddc..55f77a42 100644
--- a/verification/proofs/tlaplus/README.adoc
+++ b/verification/proofs/tlaplus/README.adoc
@@ -50,7 +50,11 @@ java -cp /path/to/tla2tools.jar tlc2.TLC -config KinGate.cfg KinGate.tla
 The default config bounds the model to 3 bots, 2 repos, `MaxRequests=4`
 (bounds both queue depth and total lifetime requests -- the latter is
 what gives `EveryRequestProcessed` a meaningful termination point).
-State space: 1,778,860 distinct states at depth 13, ~51s on 8 cores.
+State space: 444,715 distinct states at depth 13 (TLC 2.19, `tla2tools.jar` v1.7.4;
+the count the proof ledger records for `kin-gate`). An older note here gave
+1,778,860: that is the size of the graph TLC builds to check the temporal
+properties (444,715 states across 4 branches), not the distinct states the
+model reaches.
 
 == Installing TLA+