diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml
index 7ea8f99..ec04525 100644
--- a/.github/workflows/proven-tests.yml
+++ b/.github/workflows/proven-tests.yml
@@ -49,6 +49,10 @@ jobs:
         run: |
           bun scripts/atlas/census-atlas.mjs check
           bun test tests/atlas/census-atlas.test.mjs
+      - name: Mathesis census tests (offline fixtures) and catalogue currency
+        run: |
+          for t in tests/census/*.sh; do bash "$t"; done
+          bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
       # The claims registry (docs/decisions/0004-claims-registry.adoc): re-derive
       # every grade from the home repositories' receipts at their pinned commits
       # (fetched, digest-checked) and fail if the committed view is stale or a
diff --git a/Justfile b/Justfile
index 4d2372a..c1141b9 100644
--- a/Justfile
+++ b/Justfile
@@ -724,6 +724,14 @@ census:
 update-rows +repos:
     bash scripts/census/update-rows.sh {{repos}}
 
+# Re-list every blob the RSR template has shipped at its template paths, in any commit
+template-blobs:
+    bash scripts/census/template-blobs.sh docs/catalogue/census/template-paths.txt > docs/catalogue/census/template-blobs.tsv
+
+# Offline census tests: row folding, status documents, template blobs, scanner, Rust proofs
+census-test:
+    for t in tests/census/*.sh; do bash "$t" || exit 1; done
+
 # Re-render docs/catalogue/catalogue.adoc from the committed census rows
 catalogue:
     bash scripts/census/render-catalogue.sh docs/catalogue/census > docs/catalogue/catalogue.adoc
diff --git a/docs/catalogue/census/template-blobs.tsv b/docs/catalogue/census/template-blobs.tsv
new file mode 100644
index 0000000..a2f86ef
--- /dev/null
+++ b/docs/catalogue/census/template-blobs.tsv
@@ -0,0 +1,56 @@
+.machine_readable/coaptation/core/Coaptation.idr	0ab769b9e28b70ec6a8e29d7d563579833f1dcd8
+.machine_readable/coaptation/core/Coaptation.idr	4314a13082b84311d04f7b0c00fac720b4549cbb
+.machine_readable/coaptation/core/Coaptation.idr	55935352b627f4279308fb0557b22d179a57e1ff
+.machine_readable/coaptation/core/Coaptation.idr	f8ce43ae437c92ae8741306bbf5ad354768cb199
+.machine_readable/coaptation/core/Coaptation.idr	fe1acc52cff488c47020f19a380c644f13a4c709
+src/interface/Abi/Foreign.idr	3f16342bb5ca2f97e06e81741b155fb4ec4e6538
+src/interface/Abi/Foreign.idr	ad90e0553e99510496c58d9a779e21a43088ea43
+src/interface/Abi/Foreign.idr	b4b4e66a2151af7c96cadcb83d05cb0153ba03c5
+src/interface/Abi/Foreign.idr	ca66b082f4ba49fbe0437a870c2027b13fc8943c
+src/interface/Abi/Foreign.idr	cd537d49bce87fc1d472831eb8afee24a857e0e3
+src/interface/Abi/Layout.idr	2eab791abc97718a0e41b98a287ca4322b243343
+src/interface/Abi/Layout.idr	4a99a3a79a705a3708aa0c0947f6552307233b0c
+src/interface/Abi/Layout.idr	e1f4275969a57cf64cc5c7c36b5dc617fa522628
+src/interface/Abi/Layout.idr	fec979dcb2b5d11d29d24788c9485d10d7063b71
+src/interface/Abi/Types.idr	142878627347529ffc645026863087c9c923dbb2
+src/interface/Abi/Types.idr	4c8c349f10517b0882aed6aafbab0add1c4a7eb2
+src/interface/Abi/Types.idr	6fc4d041c21a69c2b7e3520da1b0886552a5266b
+src/interface/Abi/Types.idr	9d30051346f63a95c94b0165b60fc3ff79ac9b7b
+src/interface/Abi/Types.idr	df67135b92e85168d845c306368b08ad0a7b3ce2
+src/interface/abi.ipkg	14ec2498233c4a5caedce6a624e6f2d93eec22ee
+verification/proofs/agda/Properties.agda	90e4c3cf00bd55a485389d08213fd0176393cade
+verification/proofs/agda/Properties.agda	d78d9d0f787bd9de39e797f5e8698499e87119dd
+verification/proofs/coq/TypeSafety.v	8f5b41894120259096963af872a1508c7a86d8d4
+verification/proofs/coq/TypeSafety.v	c2ec6eb6e60fd9f6718e99c008fce1f7bca1451d
+verification/proofs/idris2/ABI/Compliance.idr	b94a5dbfdc43981c04228e7b9bae3262ddbc17c4
+verification/proofs/idris2/ABI/Compliance.idr	d38c0d5cb05e74d3a75ccba0cf869800d88f7876
+verification/proofs/idris2/ABI/Compliance.idr	ee5efdd1e70d3a25bf225b6acd7d398940be8f64
+verification/proofs/idris2/ABI/Compliance.idr	ffc8020f91ebec378d6936e72f8e881d8744601f
+verification/proofs/idris2/ABI/Foreign.idr	0359e05dca32e08a4221585f46190e8d0db2e4fd
+verification/proofs/idris2/ABI/Foreign.idr	1e550dd9e170806536a7bc6e321cedaa5cc59144
+verification/proofs/idris2/ABI/Foreign.idr	6c83435f79171e9443ca0855b47b228186e1d432
+verification/proofs/idris2/ABI/Foreign.idr	cb98ecdd84e3404a01604992a7bb94f5d0adeb93
+verification/proofs/idris2/ABI/Layout.idr	9040a5e9abe4d2a01a4b03ef1002980ab3f64c99
+verification/proofs/idris2/ABI/Layout.idr	9ca56c6290cce37aaee7a488a4d8351f32359063
+verification/proofs/idris2/ABI/Layout.idr	f0935aebfda2377860e7262b90f6c101299578c3
+verification/proofs/idris2/ABI/Layout.idr	f38fcca3adceab616c46b45acb1b9ba48bcede02
+verification/proofs/idris2/ABI/Platform.idr	0b5ab10792163902d2bba150147f8e6ccbcc6a62
+verification/proofs/idris2/ABI/Platform.idr	3e0635555df0208fe4328f53e6cc01e314accc03
+verification/proofs/idris2/ABI/Platform.idr	6b80d2080de76dc445bcb8b5eb96c9e29458dd54
+verification/proofs/idris2/ABI/Platform.idr	a8d6b947abc64ba430f76bbb05a9f1cdc944d4ba
+verification/proofs/idris2/ABI/Pointers.idr	310c4849b45f5e9f248ba47c1fb27077aed13d2f
+verification/proofs/idris2/ABI/Pointers.idr	31b6c5f29c40d9aaf398910da2db7674094e9445
+verification/proofs/idris2/ABI/Pointers.idr	49efd2f19b27d0d8517728dab0e12820f9e223cc
+verification/proofs/idris2/ABI/Pointers.idr	652c371fedb7f5426ab8a3dd52094a98735fe995
+verification/proofs/idris2/Types.idr	1bf772ab81ad823842ae43514b6508a8ef13d541
+verification/proofs/idris2/Types.idr	85ea9b759e904f11679cf912420d6c609fcd9fcd
+verification/proofs/idris2/Types.idr	cc7cce85cfd14b725e2872907c5a2fa9450938e4
+verification/proofs/idris2/Types.idr	e89a852fa25b00b1d133573b3a97399482f1f4a3
+verification/proofs/idris2/Types.idr	f631b74eae28d4782f738d3004f40048aa14c31d
+verification/proofs/lean4/ApiTypes.lean	144a94319736ce0cb31ac16e6ebc69c2fe680b03
+verification/proofs/lean4/ApiTypes.lean	9ed78b7778ea6925b8208be693d2b794f46130a5
+verification/proofs/lean4/ApiTypes.lean	f02f259c35082553edf22ee7d2761ce07d019e34
+verification/proofs/lean4/lean-toolchain	d0eb99ff68d76c831521c84404ad1fd549f51ac0
+verification/proofs/tlaplus/StateMachine.tla	27f2d69e7306abda0f0e2f18e3bd2993fe00d6a8
+verification/proofs/tlaplus/StateMachine.tla	932992a73c1ad8f8b178a3461fac1fccefc70344
+verification/proofs/tlaplus/StateMachine.tla	f34849477eeb99d7556f7fdb8b6e61230808417e
diff --git a/scripts/census/build-rows.sh b/scripts/census/build-rows.sh
index ec73ba1..e80eece 100644
--- a/scripts/census/build-rows.sh
+++ b/scripts/census/build-rows.sh
@@ -2,71 +2,85 @@
 # SPDX-License-Identifier: MPL-2.0
 # Fold the raw, path-level census into one row per repository.
 #
-# Usage: build-rows.sh RAW_DIR TEMPLATE_PATHS > catalogue-rows.json
-#   RAW_DIR         files.jsonl, holes.jsonl, decls.jsonl, repos-with-status.jsonl
-#                   (written by census-repo.sh + summarise.sh; not committed)
-#   TEMPLATE_PATHS  one path per line: proof files the RSR template ships,
-#                   which are boilerplate wherever they appear
+# Usage: build-rows.sh RAW_DIR TEMPLATE > catalogue-rows.json
+#   RAW_DIR   files.jsonl, holes.jsonl, decls.jsonl, repos-with-status.jsonl
+#             (written by census-repo.sh + summarise.sh; not committed)
+#   TEMPLATE  template-blobs.tsv: "path<TAB>blob" for every blob the RSR
+#             template has had at a proof-file path (template-blobs.sh). A
+#             file is template boilerplate only when its own (path, blob) is
+#             listed, so a repository that rewrote a template file in place is
+#             credited with it. A plain path list (template-paths.txt) still
+#             works, and so do raw rows without a blob: both fall back to
+#             matching by path alone. The template repository itself
+#             (hyperpolymath/rsr-template-repo) owns its files.
 #
 # Rows carry counts only, never file paths, so the committed data neither
 # grows with the estate's file trees nor repeats other repositories' paths.
-# A repo's "own" files are those not on the template list; files under
-# tests/, fixtures/, corpus/, benches/ count as fixtures. "theory" is a
-# first-pass heuristic: more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK
-# files. A human confirms each row.
+# Files under tests/, fixtures/, corpus/, benches/ count as fixtures. "theory"
+# is a first-pass heuristic: more Agda/Lean/Rocq/Isabelle files than
+# Idris2/SPARK/Creusot/Verus files. A human confirms each row.
 #
 # status_doc names one document per repository. A repository's proof status
-# lives in its PROOF-STATUS file (standards PROOF-POLICY §8.5); PROOF-NEEDS
-# lists obligations and proof-debt lists holes. So a PROOF-STATUS document
-# wins over a proof-debt one, which wins over a PROOF-NEEDS one; within a
-# rank the first path in sorted order wins. Taking the first sorted path
-# alone named docs/status/PROOF-NEEDS.adoc over docs/status/PROOF-STATUS.adoc.
+# lives in its PROOF-STATUS file (standards PROOF-POLICY §8.5); proof-debt
+# lists holes and PROOF-NEEDS lists obligations. So the rank is PROOF-STATUS,
+# then proof-debt, then PROOF-NEEDS, by basename. A document nested deeper than
+# one directory (outside docs/status/ and .machine_readable/compliance/)
+# usually belongs to a sub-project and ranks after every shallow one. Within a
+# rank the first path in byte order wins.
+#
+# Each input list is read with FILENAME==ARGV[1], not NR==FNR: an empty list
+# makes NR==FNR true for the next file, which then vanishes.
 set -euo pipefail
 R=$1 T=$2
+home=hyperpolymath/rsr-template-repo
 tmp=$(mktemp -d); trap 'rm -rf "$tmp"' EXIT
+: > "$tmp/template.tsv"
 
-jq -r '[.repo,.path,.ext]|@tsv' "$R/files.jsonl" \
-| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t)' "$T" - \
+# Split files into template boilerplate ($tmp/template.tsv: repo, path) and
+# the repository's own files (passed on).
+jq -r '[.repo,.path,.ext,(.blob // "")]|@tsv' "$R/files.jsonl" \
+| awk -F'\t' -v TM="$tmp/template.tsv" -v home="$home" '
+    FILENAME == ARGV[1] { tp[$1]=1; if (NF >= 2 && $2 != "") { tb[$1 "\t" $2]=1; nb++ }; next }
+    { tmpl = ($1 == home) ? 0 : ($4 != "" && nb > 0) ? (($2 "\t" $4) in tb) : ($2 in tp)
+      if (tmpl) print $1 "\t" $2 > TM; else print }' "$T" - \
 | awk -F'\t' 'BEGIN{OFS="\t"} {
     e=$3; p="other"
     if (e ~ /agda/) p="agda"; else if (e ~ /idr|ipkg/) p="idris2"
     else if (e ~ /lean|lakefile/) p="lean"; else if (e == "v" || e ~ /CoqProject/) p="rocq"
     else if (e == "thy") p="isabelle"; else if (e == "tla" || e == "cfg") p="tla"
     else if (e == "dk" || e == "lp") p="dedukti"; else if (e ~ /smt2|tptp/ || e == "p") p="smt-atp"
-    else if (e ~ /ad[sb]/) p="spark"; else if (e == "mlw") p="why3"
+    else if (e ~ /ad[sbc]/) p="spark"; else if (e == "mlw") p="why3"
     else if (e == "fst") p="fstar"; else if (e == "dfy") p="dafny"; else if (e == "als") p="alloy"
+    else if (e == "rs-creusot") p="creusot"; else if (e == "rs-verus") p="verus"
     fx = ($2 ~ /(^|\/)(tests?|fixtures?|corpus|corpus_fixtures|benches|benchmarks?)\//) ? 1 : 0
     print $1, p, fx }' > "$tmp/cls.tsv"
 
 jq -r '[.repo,.file,.class]|@tsv' "$R/holes.jsonl" \
-| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1"\t"$3}' "$T" - > "$tmp/holes.tsv"
+| awk -F'\t' 'FILENAME==ARGV[1]{t[$1 "\t" $2]=1;next} !(($1 "\t" $2) in t){print $1"\t"$3}' "$tmp/template.tsv" - > "$tmp/holes.tsv"
 
 jq -r '[.repo,.file]|@tsv' "$R/decls.jsonl" \
-| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1}' "$T" - > "$tmp/decls.tsv"
+| awk -F'\t' 'FILENAME==ARGV[1]{t[$1 "\t" $2]=1;next} !(($1 "\t" $2) in t){print $1}' "$tmp/template.tsv" - > "$tmp/decls.tsv"
 
-# A repository may carry more than one status document (a ledger beside a
-# template-era requirements list). Prefer the ledger: PROOF-STATUS, then
-# PROOF-NEEDS, then proof-debt, then the path, so the choice does not depend
-# on alphabetical order.
-jq -r '.repo+"\t"+(if (.path|test("(^|/)PROOF-STATUS[^/]*$";"i")) then "0"
-    elif (.path|test("(^|/)PROOF-NEEDS[^/]*$";"i")) then "1" else "2" end)+"\t"+.path' \
-  "$R/repos-with-status.jsonl" | sort | cut -f1,3 > "$tmp/status.tsv"
+jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" \
+| awk -F'\t' 'BEGIN{OFS="\t"} {
+    b = tolower($2); sub(/.*\//, "", b)
+    rk = (b ~ /^proof-status/) ? 0 : (b ~ /proof-debt/) ? 1 : 2
+    d = $2; if (d ~ /\//) sub(/\/[^\/]*$/, "", d); else d = ""
+    if (d ~ /\// && d !~ /^(docs\/status|\.machine_readable\/compliance)$/) rk += 10
+    print $1, rk, $2 }' \
+| LC_ALL=C sort -t$'\t' -k1,1 -k2,2n -k3,3 | cut -f1,3 > "$tmp/status.tsv"
 
 awk -F'\t' '
   FILENAME ~ /holes\.tsv$/  { h[$1" "$2]++; next }
   FILENAME ~ /decls\.tsv$/  { d[$1]++; next }
-  FILENAME ~ /status\.tsv$/ {
-    b = tolower($2); sub(/.*\//, "", b)
-    k = (b ~ /^proof-status/) ? 3 : (b ~ /^proof-debt/) ? 2 : 1
-    if (!($1 in st) || k > sk[$1]) { st[$1]=$2; sk[$1]=k }
-    next }
+  FILENAME ~ /status\.tsv$/ { if (!($1 in st)) st[$1]=$2; next }
   { n[$1]++; if ($3) fx[$1]++; pc[$1" "$2]++
-    if ($2 ~ /agda|lean|rocq|isabelle/) th[$1]++; if ($2 ~ /idris2|spark/) en[$1]++ }
+    if ($2 ~ /agda|lean|rocq|isabelle/) th[$1]++; if ($2 ~ /idris2|spark|creusot|verus/) en[$1]++ }
   END {
-    split("agda lean rocq isabelle idris2 spark tla dedukti smt-atp why3 fstar dafny alloy other", L, " ")
+    split("agda lean rocq isabelle idris2 spark creusot verus tla dedukti smt-atp why3 fstar dafny alloy other", L, " ")
     for (r in n) {
       provers=""
-      for (i=1;i<=14;i++) if (pc[r" "L[i]]) provers = provers L[i] " " pc[r" "L[i]] ", "
+      for (i=1;i<=16;i++) if (pc[r" "L[i]]) provers = provers L[i] " " pc[r" "L[i]] ", "
       sub(/, $/, "", provers)
       printf "%s\t%s\t%d\t%d\t%s\t%d\t%d\t%d\t%d\t%d\t%s\n",
         (th[r]+0 > en[r]+0) ? "theory" : "engineering", r, n[r], fx[r]+0, provers,
diff --git a/scripts/census/census-repo.sh b/scripts/census/census-repo.sh
index c5fdc63..684e66b 100755
--- a/scripts/census/census-repo.sh
+++ b/scripts/census/census-repo.sh
@@ -12,7 +12,9 @@ O=$BASE/out/$KEY
 mkdir -p "$BASE/out"
 rm -rf "$D" "$O".*
 
-clone() { timeout 600 git clone -q --depth 1 --filter=blob:none --no-checkout "https://github.com/$FN" "$D" 2>&1; }
+# MATHESIS_GIT_BASE lets the tests point the census at a local forge (file://).
+GIT_BASE=${MATHESIS_GIT_BASE:-https://github.com}
+clone() { timeout 600 git clone -q --depth 1 --filter=blob:none --no-checkout "$GIT_BASE/$FN" "$D" 2>&1; }
 err=$(clone); rc=$?
 if [ $rc -ne 0 ]; then
   rm -rf "$D"; sleep 2; err=$(clone); rc=$?
@@ -25,12 +27,48 @@ fi
 git -C "$D" ls-tree -r --name-only HEAD > "$O.tree" 2>/dev/null || true
 if ! [ -s "$O.tree" ]; then rm -rf "$D" "$O.tree"; exit 0; fi
 
-# proof-status docs
-grep -iE '(^|/)(PROOF-STATUS[^/]*|PROOF-NEEDS[^/]*|proof-debt[^/]*)$' "$O.tree" \
+# proof-status docs: a status page, a needs list, or a proof-debt ledger
+# (e.g. CREUSOT-PROOF-DEBT.tsv). build-rows.sh ranks them when a repo has
+# several, so the status page is the one a row names.
+grep -iE '(^|/)(PROOF-STATUS[^/]*|PROOF-NEEDS[^/]*|[^/]*proof-debt[^/]*)$' "$O.tree" \
   | jq -RcS --arg r "$FN" '{path:., repo:$r}' > "$O.status.jsonl"
 
 # candidate paths
-grep -E '\.(agda|lagda|lagda\.md|idr|lidr|ipkg|lean|v|thy|tla|cfg|dk|lp|smt2|tptp|p|ads|adb|mlw|fst|dfy|als|gpr)$|(^|/)(\.?lean-toolchain|lakefile\.lean|lakefile\.toml|_CoqProject|dune|dune-project)$|\.agda-lib$' "$O.tree" > "$O.cand"
+grep -E '\.(agda|lagda|lagda\.md|idr|lidr|ipkg|lean|v|thy|tla|cfg|dk|lp|smt2|tptp|p|ads|adb|adc|mlw|fst|dfy|als|gpr)$|(^|/)(\.?lean-toolchain|lakefile\.lean|lakefile\.toml|_CoqProject|dune|dune-project)$|\.agda-lib$' "$O.tree" > "$O.cand"
+
+# Rust verification (PROOF-POLICY §1.2: Creusot with Pearlite contracts, and
+# Verus). Proofs in Rust live in .rs files, which no prover extension marks,
+# so a crate is found by its manifest instead: a [package] Cargo.toml that
+# depends on a verifier crate. Its .rs files are checked out and kept only
+# when they carry a contract or proof marker, so an unverified crate costs one
+# manifest read and contributes nothing. Kani harnesses (§4.1) need no
+# dependency and are not detected by this rule.
+VERIFIER_DEP='^[[:space:]]*(creusot-std|creusot_std|creusot-contracts|creusot_contracts|vstd|verus_builtin|verus_builtin_macros)[[:space:]]*='
+RUST_MARK='(creusot_std|creusot_contracts|creusot)::(macros::)?(requires|ensures|invariant|variant|trusted|logic|predicate|proof_assert)|#\[[[:space:]]*(requires|ensures)[[:space:]]*\(|verus![[:space:]]*\{'
+grep -E '(^|/)Cargo\.toml$' "$O.tree" > "$O.cargo" || true
+: > "$O.rsdirs"
+if [ -s "$O.cargo" ]; then
+  tr '\n' '\0' < "$O.cargo" | (cd "$D" && timeout 600 xargs -0 -n 400 git checkout -q HEAD -- >/dev/null 2>&1)
+  while IFS= read -r p; do
+    m=$D/$p
+    grep -qE '^\[package\]' "$m" 2>/dev/null || continue
+    grep -qE "$VERIFIER_DEP" "$m" 2>/dev/null || continue
+    printf '%s\n' "${p%Cargo.toml}" >> "$O.rsdirs"
+  done < "$O.cargo"
+fi
+if [ -s "$O.rsdirs" ]; then
+  grep -E '\.rs$' "$O.tree" \
+  | awk 'NR==FNR { d[NR]=$0; n=NR; next } { for (i=1;i<=n;i++) if (d[i] == "" || index($0, d[i]) == 1) { print; break } }' "$O.rsdirs" - \
+  > "$O.rscand" || true
+  if [ -s "$O.rscand" ]; then
+    tr '\n' '\0' < "$O.rscand" | (cd "$D" && timeout 1800 xargs -0 -n 400 git checkout -q HEAD -- >/dev/null 2>&1)
+    while IFS= read -r p; do
+      grep -qE "$RUST_MARK" "$D/$p" 2>/dev/null && printf '%s\n' "$p" >> "$O.cand"
+    done < "$O.rscand"
+  fi
+fi
+rm -f "$O.cargo" "$O.rsdirs" "$O.rscand"
+
 if ! [ -s "$O.cand" ]; then rm -rf "$D"; rm -f "$O.tree" "$O.cand"; [ -s "$O.status.jsonl" ] || rm -f "$O.status.jsonl"; exit 0; fi
 
 # .cfg only if a .tla sits in the same directory; dune only if .v exists
@@ -62,11 +100,18 @@ if [ $ROCQ = 0 ] && [ $HASV = 1 ]; then
     done < <(grep -E '\.v$' "$O.co")
   fi
 fi
-# SPARK repo-level gate
-SPARK=0
-grep -qE '\.gpr$' "$O.cand" && SPARK=1
-if [ $SPARK = 0 ]; then
-  while IFS= read -r p; do grep -qi 'SPARK_Mode' "$D/$p" 2>/dev/null && { SPARK=1; break; }; done < <(grep -E '\.(ads|adb)$' "$O.co")
+# SPARK gate. An Ada file is a SPARK proof file only when SPARK analysis is
+# switched on for it: the file itself carries SPARK_Mode, or a configuration-
+# pragma file (.adc) switches it on for the whole project. A .gpr proves
+# nothing on its own: every Ada project has one. (Until 2026-11-09 a .gpr alone
+# made every .ads/.adb in the repository count as SPARK.)
+SPARK_GLOBAL=0
+while IFS= read -r p; do
+  grep -qi 'SPARK_Mode' "$D/$p" 2>/dev/null && { SPARK_GLOBAL=1; break; }
+done < <(grep -E '\.adc$' "$O.co")
+SPARK_ANY=$SPARK_GLOBAL
+if [ $SPARK_ANY = 0 ]; then
+  while IFS= read -r p; do grep -qi 'SPARK_Mode' "$D/$p" 2>/dev/null && { SPARK_ANY=1; break; }; done < <(grep -E '\.(ads|adb)$' "$O.co")
 fi
 
 prover_of() {
@@ -81,7 +126,7 @@ prover_of() {
     *.lp) echo lambdapi ;;
     *.smt2) echo smtlib ;;
     *.tptp|*.p) echo tptp ;;
-    *.ads|*.adb|*.gpr) echo spark ;;
+    *.ads|*.adb|*.adc|*.gpr) echo spark ;;
     *.mlw) echo why3 ;;
     *.fst) echo fstar ;;
     *.dfy) echo dafny ;;
@@ -108,15 +153,24 @@ while IFS= read -r p; do
       [ $ROCQ = 1 ] || continue
       # skip obvious Verilog
       if grep -qE '^\s*endmodule' "$f" 2>/dev/null && ! grep -qE '^\s*(Require|From|Theorem|Lemma|Definition|Inductive)' "$f"; then continue; fi ;;
-    *.ads|*.adb|*.gpr) [ $SPARK = 1 ] || continue ;;
+    *.ads|*.adb) [ $SPARK_GLOBAL = 1 ] || grep -qi 'SPARK_Mode' "$f" 2>/dev/null || continue ;;
+    *.adc) grep -qi 'SPARK_Mode' "$f" 2>/dev/null || continue ;;
+    *.gpr) [ $SPARK_ANY = 1 ] || continue ;;
     *.p) grep -qE '^\s*(fof|cnf|tff|thf|include)\(' "$f" 2>/dev/null || continue ;;
     *.lp) grep -qE '^\s*(symbol|require|rule|constant|injective|opaque)\b' "$f" 2>/dev/null || continue ;;
   esac
   echo "$p" >> "$O.keep"
 done < "$O.co"
 
+# A .rs file is labelled by its verifier: rs-verus when it holds a verus!
+# block, rs-creusot otherwise (it was kept for a Creusot marker).
+rs_ext() { if grep -qE 'verus![[:space:]]*\{' "$D/$1" 2>/dev/null; then echo rs-verus; else echo rs-creusot; fi; }
 while IFS= read -r p; do
-  jq -cnS --arg e "$(ext_of "$p")" --arg p "$p" --arg r "$FN" '{ext:$e,path:$p,repo:$r}'
+  case "$p" in *.rs) e=$(rs_ext "$p") ;; *) e=$(ext_of "$p") ;; esac
+  # The blob id lets build-rows.sh tell a template file from a repository's own
+  # rewrite of it at the same path (see template-blobs.sh).
+  b=$(git -C "$D" rev-parse "HEAD:$p" 2>/dev/null || true)
+  jq -cnS --arg b "$b" --arg e "$e" --arg p "$p" --arg r "$FN" '{blob:$b,ext:$e,path:$p,repo:$r}'
 done < "$O.keep" > "$O.files.jsonl"
 
 # declarations: emit TSV prover\tkind\tline\tname\tfile then convert
@@ -163,6 +217,27 @@ while IFS= read -r p; do
           s=$0; sub(/^((public[ \t]+)?export[ \t]+|private[ \t]+)/,"",s); split(s,a,/[ \t]+/); print "idris2\t" a[1] "\t" NR "\t" a[2] "\t" fl; next }
         /^((public[ \t]+)?export[ \t]+|private[ \t]+|total[ \t]+|partial[ \t]+|covering[ \t]+)*[^ \t:(][^ \t]*[ \t]+:([ \t]|$)/ {
           s=$0; while (s ~ /^(public|export|private|total|partial|covering)[ \t]+/) sub(/^[^ \t]+[ \t]+/,"",s); split(s,a,/[ \t]+/); print "idris2\tsig\t" NR "\t" a[1] "\t" fl }' "$f" ;;
+    *.rs)
+      # Creusot: a fn whose attributes carry requires/ensures is one contract
+      # (uncontracted and #[trusted] fns are not counted). Verus: proof fn and
+      # spec fn by keyword; an exec fn counts when a requires/ensures clause
+      # follows its signature.
+      awk -v fl="$p" -v pr="$(rs_ext "$p")" '
+        function fname(s,   t) { t=s; sub(/^.*(^|[^A-Za-z0-9_])fn[ \t]+/,"",t); sub(/[^A-Za-z0-9_].*$/,"",t); return t }
+        /^[ \t]*\/\// { next }
+        pr == "rs-creusot" {
+          if ($0 ~ /(requires|ensures)[ \t]*\(/ && $0 ~ /(#\[|cfg_attr|macros::)/) pend=1
+          if ($0 ~ /(^|[^A-Za-z0-9_])fn[ \t]+[A-Za-z_]/) { if (pend) print "creusot\tcontract\t" NR "\t" fname($0) "\t" fl; pend=0 }
+          next
+        }
+        pr == "rs-verus" {
+          if ($0 ~ /(^|[^A-Za-z0-9_])(proof|spec)[ \t]+fn[ \t]+[A-Za-z_]/) {
+            k = ($0 ~ /proof[ \t]+fn/) ? "proof" : "spec"
+            print "verus\t" k "\t" NR "\t" fname($0) "\t" fl; cand=""; next }
+          if ($0 ~ /(^|[^A-Za-z0-9_])fn[ \t]+[A-Za-z_]/) { cand=fname($0); cl=NR; if ($0 ~ /\{/) cand=""; next }
+          if (cand != "" && $0 ~ /^[ \t]*(requires|ensures)([ \t]|$)/) { print "verus\tcontract\t" cl "\t" cand "\t" fl; cand=""; next }
+          if ($0 ~ /\{/) cand=""
+        }' "$f" ;;
     *.tla)
       grep -nE '^\s*(THEOREM|LEMMA)\s+[A-Za-z_][A-Za-z0-9_]*\s*==' "$f" \
       | sed -E 's/^([0-9]+):\s*(THEOREM|LEMMA)\s+([A-Za-z0-9_]+).*/\1\t\2\t\3/' \
diff --git a/scripts/census/idris2-undefined.awk b/scripts/census/idris2-undefined.awk
new file mode 100644
index 0000000..ac6304b
--- /dev/null
+++ b/scripts/census/idris2-undefined.awk
@@ -0,0 +1,27 @@
+# SPDX-License-Identifier: MPL-2.0
+# Report top-level Idris2 type signatures that have no clauses in the same
+# file. Idris2 accepts such a declaration and treats it as a postulate, even
+# under %default total. Input: a comment-blanked .idr file. A signature that
+# follows a %foreign / %extern pragma (possibly with continuation lines and
+# modifier lines in between) is an FFI boundary and is not reported.
+function kw(n) { return n ~ /^(data|record|interface|implementation|module|import|namespace|parameters|mutual|total|partial|covering|public|export|private|infix|infixl|infixr|prefix|failing|using|where|let|in|do|if|then|else|case|of|with|rewrite|auto|default)$/ }
+/^[ \t]*$/ { next }
+/^%(foreign|extern)/ { ffi = 1; next }
+/^[ \t]/ { next }                                   # continuation / nested
+/^((public[ \t]+)?export|private|covering|total|partial)[ \t]*$/ { next }
+{
+  s = $0
+  sub(/^(public[ \t]+)?export[ \t]+/, "", s); sub(/^private[ \t]+/, "", s)
+  sub(/^(covering|total|partial)[ \t]+/, "", s)
+  sub(/^[01][ \t]+/, "", s)
+  if (match(s, /^[A-Za-z_][A-Za-z0-9_']*[ \t]*:/) && substr(s, RLENGTH + 1, 1) != ":") {
+    n = s; sub(/[ \t]*:.*/, "", n)
+    if (!kw(n) && !ffi) sig[n] = NR
+  } else if (match($0, /^[A-Za-z_][A-Za-z0-9_']*/)) {
+    def[substr($0, 1, RLENGTH)] = 1
+  }
+  t = $0  # infix clause: a `name` b = ...
+  while (match(t, /`[A-Za-z_][A-Za-z0-9_']*`/)) { def[substr(t, RSTART + 1, RLENGTH - 2)] = 1; t = substr(t, RSTART + RLENGTH) }
+  ffi = 0
+}
+END { for (n in sig) if (!(n in def)) print sig[n] "\t" n }
diff --git a/scripts/census/proof-holes.sh b/scripts/census/proof-holes.sh
index 2e7c706..5d1eea5 100644
--- a/scripts/census/proof-holes.sh
+++ b/scripts/census/proof-holes.sh
@@ -14,8 +14,15 @@
 #
 # This is a textual scan: it finds candidates, it does not decide them. A
 # kernel-level audit (#print axioms, Print Assumptions, gnatprove report,
-# agda --safe) is the authority; see references/ledger.md. Whole-line comments
-# are skipped; markers inside block comments or strings may still be reported.
+# agda --safe) is the authority; see references/ledger.md. Each file is scanned
+# with its comments blanked out (nested block comments, line comments, and
+# string literals where the language has a simple string syntax), so prose
+# that mentions a marker is not reported. Agda/Idris pragmas are kept.
+#
+# Local changes in hyperpolymath/mathesis (2026-11-09, landed 2026-11-10):
+# the comment-blanking pass, the Idris2 undefined-declaration rule, the Verus
+# rules and the wider Creusot #[trusted] rule are not yet in the proof-craft
+# skill this file was copied from; carry them back there.
 #
 # Exit: 0 clean at the chosen --fail-on level (default: hole), 1 otherwise,
 # 2 usage error.
@@ -40,6 +47,8 @@ EXCLUDE=(--exclude-dir=.git --exclude-dir=target --exclude-dir=_build --exclude-
 for d in "${EXTRA_EX[@]}"; do EXCLUDE+=(--exclude-dir="$d"); done
 
 # rule: lang~include-globs~comment-regex~class~marker~PCRE
+# (comment-regex is kept for the rule format; comments are now blanked by
+# strip_comments before matching, so it is no longer consulted.)
 RULES=$(cat <<'EOF'
 agda~*.agda,*.lagda,*.lagda.md~^\s*--~axiom~postulate~^\s*postulate\b
 agda~*.agda,*.lagda,*.lagda.md~^\s*--~hole~{! !}~\{!
@@ -73,7 +82,11 @@ isabelle~*.thy~^\s*\(\*~hole~sorry~\bsorry\b
 isabelle~*.thy~^\s*\(\*~hole~oops~\boops\b
 isabelle~*.thy~^\s*\(\*~axiom~axiomatization~\baxiomatization\b
 isabelle~*.thy~^\s*\(\*~unsafe~quick_and_dirty~quick_and_dirty
-creusot~*.rs~^\s*//~axiom~#[trusted]~#\[\s*(creusot::)?trusted\s*\]
+creusot~*.rs~^\s*//~axiom~#[trusted]~#\[\s*((creusot|creusot_std|creusot_contracts)::(macros::)?)?trusted\s*\]|cfg_attr\([^)]*,\s*((creusot|creusot_std|creusot_contracts)::(macros::)?)?trusted\s*\)
+verus~*.rs~^\s*//~hole~admit()~\badmit\s*\(\s*\)
+verus~*.rs~^\s*//~axiom~assume()~(?<![!\w])assume\s*\(
+verus~*.rs~^\s*//~axiom~external_body~#\[\s*verifier(::|\s*\(\s*)external_body
+verus~*.rs~^\s*//~axiom~assume_specification~\bassume_specification\b
 creusot~*.rs~^\s*//~hole~assume!~\b(proof_)?assume!\s*\(
 spark~*.adb,*.ads~^\s*--~hole~pragma Assume~pragma\s+Assume\b
 spark~*.adb,*.ads~^\s*--~unsafe~SPARK_Mode Off~SPARK_Mode\s*(=>\s*)?\(?\s*Off
@@ -89,20 +102,104 @@ emit() { # lang class marker file line text
         '{lang:$lang,class:$class,marker:$marker,file:$file,line:$line,text:$text}'
 }
 
-OUT=$(mktemp); trap 'rm -f "$OUT"' EXIT
+OUT=$(mktemp); MIRROR=$(mktemp -d); trap 'rm -rf "$OUT" "$MIRROR"' EXIT
+
+# Comment syntax per language: block-open block-close line-comment
+# second-line-comment kept-pragma-opener string-style ("-" = none).
+syntax() {
+  case "$1" in
+    rocq) echo '(* *) - - - dq' ;;
+    isabelle) echo '(* *) - - - -' ;;
+    agda) echo '{- -} -- - {-# bs' ;;
+    idris2) echo '{- -} -- ||| {-# bs' ;;
+    lean) echo '/- -/ -- - - bs' ;;
+    creusot) echo '/* */ // - - bs' ;;
+    verus) echo '/* */ // - - bs' ;;
+    spark) echo '- - -- - - dq' ;;
+    dedukti) echo '(; ;) // - - -' ;;
+  esac
+}
+strip_comments() { # lang file -> stdout
+  read -r bo bc lc lc2 keep str <<<"$(syntax "$1")"
+  for v in bo bc lc lc2 keep str; do [ "${!v}" = - ] && printf -v "$v" ''; done
+  awk -v bo="$bo" -v bc="$bc" -v lc="$lc" -v lc2="$lc2" -v keep="$keep" -v str="$str" '
+  # Blank out comments (and, where str is set, string literals) while keeping
+  # every newline, so line numbers and the code on each line stay put.
+  # Variables: bo/bc block-comment open/close (nested), lc line-comment
+  # prefix (empty for none), lc2 a second line prefix, keep a block opener
+  # that is *not* a comment (Agda/Idris pragmas "{-#", closed by "#-}"),
+  # str = "bs" (backslash escapes), "dq" (doubled quote) or "" (none).
+  BEGIN { depth = 0; instr = 0; inkeep = 0 }
+  {
+    out = ""; n = length($0); i = 1
+    while (i <= n) {
+      c = substr($0, i, 1)
+      if (instr) {
+        if (str == "bs" && c == "\\") { out = out "  "; i += 2; continue }
+        if (c == "\"") {
+          if (str == "dq" && substr($0, i + 1, 1) == "\"") { out = out "  "; i += 2; continue }
+          instr = 0; out = out c; i++; continue
+        }
+        out = out " "; i++; continue
+      }
+      if (depth > 0) {
+        if (substr($0, i, length(bo)) == bo) { depth++; out = out sprintf("%*s", length(bo), ""); i += length(bo); continue }
+        if (substr($0, i, length(bc)) == bc) { depth--; out = out sprintf("%*s", length(bc), ""); i += length(bc); continue }
+        out = out " "; i++; continue
+      }
+      if (inkeep) {
+        if (substr($0, i, 3) == "#-}") { inkeep = 0; out = out "#-}"; i += 3; continue }
+        out = out c; i++; continue
+      }
+      if (keep != "" && substr($0, i, length(keep)) == keep) { inkeep = 1; out = out keep; i += length(keep); continue }
+      if (bo != "" && substr($0, i, length(bo)) == bo) { depth = 1; out = out sprintf("%*s", length(bo), ""); i += length(bo); continue }
+      if (lc != "" && substr($0, i, length(lc)) == lc) break
+      if (lc2 != "" && substr($0, i, length(lc2)) == lc2) break
+      if (str != "" && c == "\"") { instr = 1; out = out c; i++; continue }
+      out = out c; i++
+    }
+    print out
+  }
+  ' "$2"
+}
+PRUNE=(.git target _build build .lake node_modules deps vendor "${EXTRA_EX[@]}")
+mirror() { # lang globs -> fills $MIRROR/<lang>/ with comment-blanked copies
+  local lang=$1 g names=() pr=()
+  IFS=',' read -ra gl <<<"$2"; for g in "${gl[@]}"; do names+=(-o -name "$g"); done
+  for g in "${PRUNE[@]}"; do pr+=(-o -name "$g"); done
+  find "$DIR" \( "${pr[@]:1}" \) -prune -o -type f \( "${names[@]:1}" \) -print 2>/dev/null |
+  while IFS= read -r src; do
+    rel=${src#"$DIR"/}; mkdir -p "$MIRROR/$lang/$(dirname "$rel")"
+    strip_comments "$lang" "$src" > "$MIRROR/$lang/$rel"
+  done
+}
 while IFS='~' read -r lang globs comment class marker re; do
   [ -z "$lang" ] && continue
   inc=(); IFS=',' read -ra gl <<<"$globs"; for g in "${gl[@]}"; do inc+=(--include="$g"); done
   # Rocq shares .v with V and Verilog; only scan .v files that look like Rocq.
-  grep -rnPI "${EXCLUDE[@]}" "${inc[@]}" -e "$re" "$DIR" 2>/dev/null | while IFS= read -r hit; do
-    f=${hit%%:*}; rest=${hit#*:}; n=${rest%%:*}; txt=${rest#*:}
-    printf '%s\n' "$txt" | grep -qP -- "$comment" && continue
+  [ -d "$MIRROR/$lang" ] || { mkdir -p "$MIRROR/$lang"; mirror "$lang" "$globs"; }
+  grep -rnPI "${inc[@]}" -e "$re" "$MIRROR/$lang" 2>/dev/null | while IFS= read -r hit; do
+    m=${hit%%:*}; rest=${hit#*:}; n=${rest%%:*}
+    f="$DIR/${m#"$MIRROR/$lang"/}"; txt=$(sed -n "${n}p" "$f")
     if [ "$lang" = rocq ] && ! grep -qE '^\s*(Require|From|Theorem|Lemma|Definition|Inductive|Proof\.)' "$f"; then continue; fi
     if [ "$lang" = creusot ] && ! grep -qE 'creusot|pearlite|#\[\s*(requires|ensures)' "$f"; then continue; fi
+    if [ "$lang" = verus ] && ! grep -qE 'verus!\s*\{' "$f"; then continue; fi
     emit "$lang" "$class" "$marker" "${f#"$DIR"/}" "$n" "$(printf '%s' "$txt" | sed 's/^\s*//' | cut -c1-200)"
   done >>"$OUT"
 done <<<"$RULES"
 
+# Idris2: a top-level signature with no clauses is accepted and treated as a
+# postulate, even under %default total (checked with Idris2 0.8.0), so it is
+# an axiom candidate. FFI signatures after %foreign/%extern are not reported.
+UNDEF_AWK="$(cd "$(dirname "$0")" && pwd)/idris2-undefined.awk"
+[ -d "$MIRROR/idris2" ] || { mkdir -p "$MIRROR/idris2"; mirror idris2 "*.idr,*.lidr"; }
+while IFS= read -r m; do
+  f="$DIR/${m#"$MIRROR/idris2"/}"
+  awk -f "$UNDEF_AWK" "$m" | while IFS=$'\t' read -r n name; do
+    emit idris2 axiom "undefined declaration" "${f#"$DIR"/}" "$n" "$(sed -n "${n}p" "$f" | sed 's/^[[:space:]]*//' | cut -c1-200)"
+  done
+done < <(find "$MIRROR/idris2" -type f -name '*.idr') >>"$OUT"
+
 # Agda: every non-fixture module should be checked under --safe.
 while IFS= read -r f; do
   grep -qE 'OPTIONS[^#]*--safe' "$f" || emit agda policy "no --safe" "${f#"$DIR"/}" 1 "file does not set {-# OPTIONS --safe #-}" >>"$OUT"
diff --git a/scripts/census/run-census.sh b/scripts/census/run-census.sh
index bd7d631..1d02011 100644
--- a/scripts/census/run-census.sh
+++ b/scripts/census/run-census.sh
@@ -32,6 +32,6 @@ while IFS= read -r repo; do
 done < "$list"
 MATHESIS_DATA=$work bash "$here/summarise.sh"
 jq -cS -s . "$work/unreachable.jsonl" > "$census/unreachable.json"
-bash "$here/build-rows.sh" "$work" "$census/template-paths.txt" > "$census/catalogue-rows.json"
+bash "$here/build-rows.sh" "$work" "$census/template-blobs.tsv" > "$census/catalogue-rows.json"
 bash "$here/render-catalogue.sh" "$census" > "$here/../../docs/catalogue/catalogue.adoc"
 echo "raw census kept in $work"
diff --git a/scripts/census/summarise.sh b/scripts/census/summarise.sh
index 8483dd1..31b21e3 100644
--- a/scripts/census/summarise.sh
+++ b/scripts/census/summarise.sh
@@ -20,8 +20,9 @@ PROVER='def prover: (.ext) as $e |
   elif ($e|test("^(tla|cfg)$")) then "tla"
   elif $e=="dk" then "dedukti" elif $e=="lp" then "lambdapi"
   elif $e=="smt2" then "smtlib" elif ($e|test("^(tptp|p)$")) then "tptp"
-  elif ($e|test("^(ads|adb|gpr)$")) then "spark" elif $e=="mlw" then "why3"
-  elif $e=="fst" then "fstar" elif $e=="dfy" then "dafny" elif $e=="als" then "alloy" else $e end;'
+  elif ($e|test("^(ads|adb|adc|gpr)$")) then "spark" elif $e=="mlw" then "why3"
+  elif $e=="fst" then "fstar" elif $e=="dfy" then "dafny" elif $e=="als" then "alloy"
+  elif $e=="rs-creusot" then "creusot" elif $e=="rs-verus" then "verus" else $e end;'
 CORPUS_RE='(^|/)(tests?|fixtures?|test-fixtures|testdata|test-data|examples?|benchmarks?|benches|bench|corpus|corpora|samples?|external_corpora|third_party|vendor|training_data)(/|$)'
 
 total=$(wc -l < repos.jsonl)
@@ -99,6 +100,6 @@ echo "## Method and caveats"
 echo
 echo "- Enumeration used the session's list_repos tool (per-letter substring queries). Every repo it returned has pushed_at on or after 2026-09-15, so repos untouched since then may be missing from the listing."
 echo "- Declarations are grep/awk best effort. Agda and Idris2 count every column-0 \`name : type\` signature (helpers included), plus data/record names and postulated names; Lean/Rocq/Isabelle use keyword rules; TLA+ counts THEOREM/LEMMA and .cfg INVARIANT/PROPERTY names. SMT-LIB, TPTP, Dafny, F*, Why3, Alloy and SPARK files are counted as files only."
-echo "- .v files count only in repos with Rocq signs (_CoqProject, dune with coq, or a .v containing Require/Theorem); Verilog-looking files are skipped. .p counts only with TPTP formulas, .lp only with Lambdapi keywords, .ads/.adb only when the repo has a .gpr or SPARK_Mode."
+echo "- .v files count only in repos with Rocq signs (_CoqProject, dune with coq, or a .v containing Require/Theorem); Verilog-looking files are skipped. .p counts only with TPTP formulas, .lp only with Lambdapi keywords, .ads/.adb only when SPARK analysis is on for the file: the file carries SPARK_Mode, or a .adc configuration-pragma file switches it on for the project (a .gpr alone does not count)."
 echo "- Hole counts are textual (proof-holes.sh); a kernel-level audit is the authority."
 } > summary.md
diff --git a/scripts/census/template-blobs.sh b/scripts/census/template-blobs.sh
new file mode 100755
index 0000000..c78c5ed
--- /dev/null
+++ b/scripts/census/template-blobs.sh
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Every blob the RSR template has ever had at its proof-file paths.
+#
+# Usage: template-blobs.sh TEMPLATE_PATHS [OWNER/REPO] > template-blobs.tsv
+#   TEMPLATE_PATHS  one path per line: proof files the RSR template ships
+#   OWNER/REPO      the template repository (default hyperpolymath/rsr-template-repo)
+#
+# Output: one "path<TAB>blob" line per (path, git blob id) the template has
+# held at any commit on any ref, sorted. build-rows.sh treats a repository's
+# file as template boilerplate only when its own (path, blob) is on this list.
+#
+# Why blobs and not paths: a repository that rewrites a template file in place
+# (the RSR template's ABI seam, src/interface/Abi/*.idr, is meant to be
+# replaced) keeps the path but not the content, and is doing exactly the work
+# the census exists to find. Matching every historical blob, not only the
+# current one, also keeps an untouched copy of an older template version
+# classed as boilerplate. Template proof files carry no {{…}} mint tokens, so
+# a mint copies them byte for byte.
+#
+# The clone is blobless and fetches commits and trees only.
+set -euo pipefail
+T=${1:?usage: template-blobs.sh TEMPLATE_PATHS [OWNER/REPO]}
+REPO=${2:-hyperpolymath/rsr-template-repo}
+work=$(mktemp -d); trap 'rm -rf "$work"' EXIT
+git clone -q --filter=blob:none --no-checkout "https://github.com/$REPO" "$work/t"
+mapfile -t paths < <(grep -v '^[[:space:]]*$' "$T")
+git -C "$work/t" log --all --format= --raw --no-abbrev --no-renames -- "${paths[@]}" \
+  | awk -F'\t' '{ split($1, f, " "); if (f[4] !~ /^0+$/) print $2 "\t" f[4] }' \
+  | LC_ALL=C sort -u
diff --git a/scripts/census/update-rows.sh b/scripts/census/update-rows.sh
index d0dded4..5651ee1 100644
--- a/scripts/census/update-rows.sh
+++ b/scripts/census/update-rows.sh
@@ -39,7 +39,7 @@ if [ -s "$work/unreachable.jsonl" ]; then
   echo "update-rows: could not clone: $(jq -r .repo "$work/unreachable.jsonl" | tr '\n' ' ')" >&2
   exit 1
 fi
-bash "$here/build-rows.sh" "$work" "$census/template-paths.txt" > "$work/new-rows.json"
+bash "$here/build-rows.sh" "$work" "$census/template-blobs.tsv" > "$work/new-rows.json"
 jq -R . "$work/census-list.txt" | jq -s . > "$work/names.json"
 jq -cS --slurpfile new "$work/new-rows.json" --slurpfile names "$work/names.json" '
   map(select(.repo as $r | $names[0] | index($r) | not)) + $new[0] | sort_by(.repo)
diff --git a/tests/census/build_rows_test.sh b/tests/census/build_rows_test.sh
new file mode 100755
index 0000000..4a59649
--- /dev/null
+++ b/tests/census/build_rows_test.sh
@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# build-rows.sh: a template file counts as boilerplate only when its (path,
+# blob) is one the template shipped; a customised copy is the repository's own.
+set -euo pipefail
+here=$(cd "$(dirname "$0")" && pwd)
+build=$here/../../scripts/census/build-rows.sh
+T=$(mktemp -d); trap 'rm -rf "$T"' EXIT
+pass=0 fail=0
+check() { local msg=$1; shift; if "$@"; then pass=$((pass + 1)); else echo "FAIL: $msg"; fail=$((fail + 1)); fi; }
+
+printf 'src/Abi/Types.idr\nsrc/Abi/Layout.idr\n' > "$T/paths.txt"
+printf 'src/Abi/Types.idr\tb1\nsrc/Abi/Layout.idr\tb2\n' > "$T/template.tsv"
+R=$T/raw; mkdir -p "$R"
+cat > "$R/files.jsonl" <<'EOF'
+{"blob":"b9","ext":"idr","path":"src/Abi/Types.idr","repo":"x/custom"}
+{"blob":"b2","ext":"idr","path":"src/Abi/Layout.idr","repo":"x/custom"}
+{"blob":"b7","ext":"agda","path":"proofs/Extra.agda","repo":"x/custom"}
+{"blob":"b1","ext":"idr","path":"src/Abi/Types.idr","repo":"x/pristine"}
+{"ext":"idr","path":"src/Abi/Types.idr","repo":"x/old"}
+{"blob":"b1","ext":"idr","path":"src/Abi/Types.idr","repo":"hyperpolymath/rsr-template-repo"}
+EOF
+cat > "$R/holes.jsonl" <<'EOF'
+{"class":"hole","file":"src/Abi/Types.idr","repo":"x/custom"}
+{"class":"hole","file":"src/Abi/Layout.idr","repo":"x/custom"}
+{"class":"hole","file":"src/Abi/Types.idr","repo":"x/pristine"}
+EOF
+cat > "$R/decls.jsonl" <<'EOF'
+{"file":"src/Abi/Types.idr","repo":"x/custom"}
+{"file":"src/Abi/Types.idr","repo":"x/custom"}
+{"file":"src/Abi/Layout.idr","repo":"x/custom"}
+{"file":"proofs/Extra.agda","repo":"x/custom"}
+{"file":"src/Abi/Types.idr","repo":"x/pristine"}
+EOF
+: > "$R/repos-with-status.jsonl"
+
+out=$(bash "$build" "$R" "$T/template.tsv")
+row() { jq -c --arg r "$1" '.[] | select(.repo == $r)' <<<"$out"; }
+check "customised Types.idr is own (2 own files)" [ "$(row x/custom | jq .own_files)" = 2 ]
+check "customised repo provers" [ "$(row x/custom | jq -r .provers)" = "agda 1, idris2 1" ]
+check "hole in the customised file counts, the boilerplate one does not" [ "$(row x/custom | jq .holes)" = 1 ]
+check "declarations: 2 in Types.idr + 1 in Extra.agda" [ "$(row x/custom | jq .declarations)" = 3 ]
+check "pristine template copy yields no row" [ -z "$(row x/pristine)" ]
+check "a file with no recorded blob falls back to its path" [ -z "$(row x/old)" ]
+check "the template repository owns its template files" [ "$(row hyperpolymath/rsr-template-repo | jq .own_files)" = 1 ]
+
+# With a plain path list the path alone decides, as before.
+out=$(bash "$build" "$R" "$T/paths.txt")
+check "path-only mode: only Extra.agda is own" [ "$(row x/custom | jq .own_files)" = 1 ]
+check "path-only mode: no template-path hole counts" [ "$(row x/custom | jq .holes)" = 0 ]
+
+echo "build-rows tests: $pass passed, $fail failed"
+[ "$fail" -eq 0 ]
diff --git a/tests/census/census_rust_test.sh b/tests/census/census_rust_test.sh
new file mode 100755
index 0000000..1782a45
--- /dev/null
+++ b/tests/census/census_rust_test.sh
@@ -0,0 +1,169 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# The census must see proofs written in Rust (PROOF-POLICY §1.2: Creusot with
+# Pearlite contracts, and Verus), and must prefer a repository's proof-status
+# page over its debt ledger.
+#
+# Builds a throwaway git repository with:
+#   kernel/   a crate that depends on creusot-std: two functions carry
+#             contracts (one in the cfg_attr form), one is #[trusted] in the
+#             cfg_attr form, and one carries no contract;
+#   checked/  a crate that depends on vstd: a verus! block with a proof fn, a
+#             spec fn and an exec fn with an ensures clause, plus an
+#             #[verifier::external_body] escape;
+#   plain/    a crate with no verifier dependency, whose file mentions
+#             `ensures` in a comment: it must not be counted;
+#   docs/status/PROOF-STATUS.adoc and crates/CREUSOT-PROOF-DEBT.tsv: the
+#             status page must win over the debt file.
+# then runs census-repo.sh and build-rows.sh against it over file://.
+set -euo pipefail
+here=$(cd "$(dirname "$0")" && pwd)
+census=$here/../../scripts/census
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+fail() { echo "census_rust_test: FAIL: $*" >&2; exit 1; }
+
+src=$work/forge/fixture/rusty
+mkdir -p "$src/kernel/src" "$src/checked/src" "$src/plain/src" "$src/docs/status" "$src/crates"
+cat > "$src/Cargo.toml" <<'EOF'
+[workspace]
+members = ["kernel", "checked", "plain"]
+[workspace.dependencies]
+creusot-std = "0.14"
+EOF
+cat > "$src/kernel/Cargo.toml" <<'EOF'
+[package]
+name = "kernel"
+[dependencies]
+creusot-std = { workspace = true }
+EOF
+cat > "$src/kernel/src/lib.rs" <<'EOF'
+#[cfg_attr(creusot, creusot_std::macros::requires(x@ <= 10))]
+#[cfg_attr(creusot, creusot_std::macros::ensures(result@ == x@ + 1))]
+pub fn succ(x: u32) -> u32 {
+    x + 1
+}
+
+#[ensures(result == a)]
+fn id(a: u8) -> u8 {
+    a
+}
+
+#[cfg_attr(creusot, creusot_std::macros::trusted)]
+pub fn as_float(x: u32) -> f64 {
+    f64::from(x)
+}
+
+pub fn uncontracted(x: u32) -> u32 {
+    x
+}
+EOF
+cat > "$src/checked/Cargo.toml" <<'EOF'
+[package]
+name = "checked"
+[dependencies]
+vstd = "0.0.0"
+EOF
+cat > "$src/checked/src/lib.rs" <<'EOF'
+use vstd::prelude::*;
+verus! {
+spec fn double(x: nat) -> nat { x + x }
+proof fn double_is_even(x: nat)
+    ensures double(x) % 2 == 0,
+{
+}
+fn add_one(x: u8) -> (r: u8)
+    requires x < 255,
+    ensures r == x + 1,
+{
+    x + 1
+}
+#[verifier::external_body]
+fn opaque() {}
+}
+EOF
+cat > "$src/plain/Cargo.toml" <<'EOF'
+[package]
+name = "plain"
+[dependencies]
+serde = "1"
+EOF
+cat > "$src/plain/src/lib.rs" <<'EOF'
+// This ensures nothing: an ordinary crate with no verifier.
+pub fn f() {}
+EOF
+echo '= Proof status' > "$src/docs/status/PROOF-STATUS.adoc"
+printf 'PD-01\tkernel/src/lib.rs\tas_float\ttrusted\n' > "$src/crates/CREUSOT-PROOF-DEBT.tsv"
+git -C "$src" init -q
+git -C "$src" add -A
+git -C "$src" -c user.name=t -c user.email=t@example.invalid commit -q -m fixture
+git -C "$src" config uploadpack.allowFilter true
+
+data=$work/data
+MATHESIS_DATA=$data MATHESIS_GIT_BASE="file://$work/forge" \
+  bash "$census/census-repo.sh" fixture/rusty
+o=$data/out/fixture__rusty
+[ -s "$o.files.jsonl" ] || fail "no files.jsonl: the Rust proofs were not found"
+
+files=$(jq -r '[.path,.ext]|@tsv' "$o.files.jsonl" | sort)
+expected=$(printf 'checked/src/lib.rs\trs-verus\nkernel/src/lib.rs\trs-creusot')
+[ "$files" = "$expected" ] || fail "files were
+$files
+expected
+$expected"
+
+decls=$(jq -r '[.file,.kind,.name]|@tsv' "$o.decls.jsonl" | sort)
+expected=$(printf 'checked/src/lib.rs\tcontract\tadd_one\nchecked/src/lib.rs\tproof\tdouble_is_even\nchecked/src/lib.rs\tspec\tdouble\nkernel/src/lib.rs\tcontract\tid\nkernel/src/lib.rs\tcontract\tsucc')
+[ "$decls" = "$expected" ] || fail "declarations were
+$decls
+expected
+$expected"
+
+holes=$(jq -r '[.file,.lang,.class,.marker]|@tsv' "$o.holes.jsonl" | sort)
+expected=$(printf 'checked/src/lib.rs\tverus\taxiom\texternal_body\nkernel/src/lib.rs\tcreusot\taxiom\t#[trusted]')
+[ "$holes" = "$expected" ] || fail "holes were
+$holes
+expected
+$expected"
+
+jq -r '.path' "$o.status.jsonl" | grep -qx 'docs/status/PROOF-STATUS.adoc' \
+  || fail "the PROOF-STATUS page was not recognised as a status doc"
+jq -r '.path' "$o.status.jsonl" | grep -qx 'crates/CREUSOT-PROOF-DEBT.tsv' \
+  || fail "the debt ledger CREUSOT-PROOF-DEBT.tsv was not recognised as a status doc"
+
+# Fold into a catalogue row the way run-census.sh does.
+: > "$data/repos.jsonl"; echo fixture/rusty > "$data/census-list.txt"
+MATHESIS_DATA=$data bash "$census/summarise.sh" >/dev/null
+: > "$work/template-paths.txt"
+row=$(bash "$census/build-rows.sh" "$data" "$work/template-paths.txt" | jq -c '.[0]')
+[ "$(jq -r .provers <<<"$row")" = "creusot 1, verus 1" ] || fail "provers: $row"
+[ "$(jq -r .class <<<"$row")" = "engineering" ] || fail "class: $row"
+[ "$(jq -r .declarations <<<"$row")" = "5" ] || fail "declarations: $row"
+[ "$(jq -r .axioms <<<"$row")" = "2" ] || fail "axioms: $row"
+[ "$(jq -r .status_doc <<<"$row")" = "docs/status/PROOF-STATUS.adoc" ] || fail "status_doc: $row"
+
+# Status-doc ranking, on build-rows.sh alone: a nested sub-project's status
+# page (two or more directories deep) must not displace the
+# repository's own top-level needs list, as it did for developer-ecosystem.
+raw=$work/raw-ranking
+mkdir -p "$raw"
+printf '%s\n' '{"ext":"idr","path":"src/A.idr","repo":"x/nested"}' > "$raw/files.jsonl"
+: > "$raw/holes.jsonl"; : > "$raw/decls.jsonl"
+printf '%s\n' \
+  '{"path":"PROOF-NEEDS.adoc","repo":"x/nested"}' \
+  '{"path":"ecosystem/sub/PROOF-STATUS.adoc","repo":"x/nested"}' \
+  > "$raw/repos-with-status.jsonl"
+doc=$(bash "$census/build-rows.sh" "$raw" "$work/template-paths.txt" | jq -r '.[0].status_doc')
+[ "$doc" = "PROOF-NEEDS.adoc" ] || fail "nested status page won over the top-level needs list: $doc"
+
+# A repository's own one-level layout (standards keeps its needs list in
+# 3-practice/) is not a nested sub-project: its needs list beats a debt
+# ledger nested two directories deep, which would otherwise rank first.
+printf '%s\n' \
+  '{"path":"3-practice/PROOF-NEEDS.adoc","repo":"x/nested"}' \
+  '{"path":"crates/sub/proof-debt.adoc","repo":"x/nested"}' \
+  > "$raw/repos-with-status.jsonl"
+doc=$(bash "$census/build-rows.sh" "$raw" "$work/template-paths.txt" | jq -r '.[0].status_doc')
+[ "$doc" = "3-practice/PROOF-NEEDS.adoc" ] || fail "a one-level needs list lost to a nested debt ledger: $doc"
+
+echo "census_rust_test: ok (Creusot and Verus files, contracts, escapes and the status page all found)"
diff --git a/tests/census/proof_holes_comments_test.sh b/tests/census/proof_holes_comments_test.sh
new file mode 100755
index 0000000..b12a1da
--- /dev/null
+++ b/tests/census/proof_holes_comments_test.sh
@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# proof-holes.sh must report markers in code and skip the same markers in
+# comments and strings (nested block comments, comments spanning lines,
+# trailing line comments), while keeping Agda/Idris pragmas.
+set -euo pipefail
+
+SCAN="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)/scripts/census/proof-holes.sh"
+F=$(mktemp -d)
+trap 'rm -rf "$F"' EXIT
+
+printf '%s\n' 'Require Import Arith.' '(* comment *) Lemma a : False. Admitted.' 'Axioms x y : nat.' \
+  '(* Admitted.' '   Axiom z. *)' 'Unset Guard Checking.' 'Definition s := "Admitted.".' > "$F/A.v"
+printf '%s\n' '{-# OPTIONS --safe --type-in-type #-}' 'module B where' '{- postulate q {- n -} -}' \
+  'postulate p : Set -- postulate r' '{-# TERMINATING #-}' 'f = {! !}' > "$F/B.agda"
+printf '%s\n' 'module C' '%default partial' '{- believe_me -}' 'x = believe_me 3 -- believe_me' \
+  '||| believe_me in doc' '0 postulated : Void' '%foreign "C:f,libc"' 'export' 'ffi : Int -> Int' 'infixl 5 `snoc`' 'snoc : Nat -> Nat -> Nat' 'a `snoc` b = a' > "$F/C.idr"
+printf '%s\n' 'theorem t : False := by sorry' '/- sorry' ' axiom a : False -/' 'axiom b : False' \
+  'def s := "sorry"' > "$F/D.lean"
+printf '%s\n' '/* #[trusted] */' '#[trusted]' 'fn f() { creusot::x; }' > "$F/E.rs"
+printf '%s\n' 'pragma Assume (X);' '-- pragma Assume (Y);' > "$F/F.adb"
+printf '%s\n' 'lemma x: "A" sorry' '(* sorry *)' > "$F/G.thy"
+
+got=$(bash "$SCAN" --fail-on none "$F" | jq -r '"\(.file):\(.line) \(.marker)"' | sort)
+want=$(sort <<'WANT'
+A.v:2 Admitted
+A.v:3 Axiom
+A.v:6 Unset Checking
+B.agda:1 --type-in-type
+B.agda:4 postulate
+B.agda:5 TERMINATING
+B.agda:6 {! !}
+C.idr:2 %default partial
+C.idr:4 believe_me
+C.idr:6 undefined declaration
+D.lean:1 sorry
+D.lean:4 axiom
+E.rs:2 #[trusted]
+F.adb:1 pragma Assume
+G.thy:1 sorry
+WANT
+)
+if [ "$got" != "$want" ]; then
+  echo "FAIL: proof-holes.sh findings differ from the expected set"
+  diff <(printf '%s\n' "$want") <(printf '%s\n' "$got") || true
+  exit 1
+fi
+bash "$SCAN" "$F" >/dev/null && { echo "FAIL: --fail-on hole passed although holes exist"; exit 1; }
+echo "PASS: 15 markers in code reported, comment and string decoys skipped"
diff --git a/tests/census/status_doc_rank_test.sh b/tests/census/status_doc_rank_test.sh
new file mode 100755
index 0000000..92c0ce9
--- /dev/null
+++ b/tests/census/status_doc_rank_test.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# build-rows.sh picks one status document per repository: PROOF-STATUS
+# before proof-debt before PROOF-NEEDS, whatever their paths sort to.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.."
+raw=$(mktemp -d); trap 'rm -rf "$raw"' EXIT
+: > "$raw/holes.jsonl"; : > "$raw/decls.jsonl"
+# An empty template list must not drop every row (awk NR==FNR did).
+: > "$raw/template.txt"
+for r in a/needs-first a/debt-only a/needs-only; do
+  printf '{"repo":"%s","path":"src/X.agda","ext":"agda"}\n' "$r" >> "$raw/files.jsonl"
+done
+cat > "$raw/repos-with-status.jsonl" <<'J'
+{"repo":"a/needs-first","path":"docs/status/PROOF-NEEDS.adoc"}
+{"repo":"a/needs-first","path":"docs/status/PROOF-STATUS.adoc"}
+{"repo":"a/needs-first","path":"docs/proof-debt.adoc"}
+{"repo":"a/debt-only","path":"PROOF-NEEDS.adoc"}
+{"repo":"a/debt-only","path":"docs/proof-debt.md"}
+{"repo":"a/needs-only","path":"PROOF-NEEDS.adoc"}
+J
+got=$(bash scripts/census/build-rows.sh "$raw" "$raw/template.txt" \
+      | jq -r '.[] | .repo + " " + .status_doc' | sort)
+want=$'a/debt-only docs/proof-debt.md\na/needs-first docs/status/PROOF-STATUS.adoc\na/needs-only PROOF-NEEDS.adoc'
+if [ "$got" != "$want" ]; then
+  printf 'FAIL: status documents\n--- want\n%s\n--- got\n%s\n' "$want" "$got" >&2
+  exit 1
+fi
+echo "PASS: build-rows.sh ranks PROOF-STATUS, then proof-debt, then PROOF-NEEDS"
+# A listed template path still counts as boilerplate: with every proof file
+# on the list, no repository has own files, so there are no rows.
+echo "src/X.agda" > "$raw/template.txt"
+if [ "$(bash scripts/census/build-rows.sh "$raw" "$raw/template.txt")" != "[]" ]; then
+  echo "FAIL: template paths were counted as own files" >&2
+  exit 1
+fi
+echo "PASS: template paths are set aside, and an empty template list drops nothing"