From 0fd8d0225f18d074dfd11d79221804c0c437b60f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 7 Nov 2026 01:34:20 +0000
Subject: [PATCH 1/4] Document verification integration status separately from
 prover declarations

---
 .machine_readable/provers.a2ml                | 16 ++--
 .../verification-integrations.a2ml            | 79 +++++++++++++++++
 docs/PROVER_COUNT.adoc                        | 18 ++--
 scripts/check-verification-integrations.py    | 84 +++++++++++++++++++
 scripts/gen-provers-a2ml.sh                   | 14 ++--
 5 files changed, 190 insertions(+), 21 deletions(-)
 create mode 100644 .machine_readable/verification-integrations.a2ml
 create mode 100644 scripts/check-verification-integrations.py

diff --git a/.machine_readable/provers.a2ml b/.machine_readable/provers.a2ml
index dc27c06f..18952ef7 100644
--- a/.machine_readable/provers.a2ml
+++ b/.machine_readable/provers.a2ml
@@ -3,23 +3,23 @@
 #
 # provers.a2ml — Authoritative enumeration of ECHIDNA prover backends.
 #
-# Generated from src/rust/provers/mod.rs::ProverKind. One section per
+# Generated from crates/echidna-core/src/prover_kind.rs::ProverKind. One section per
 # variant, keyed by the variant's PascalCase name for stability against
 # slug-format drift. `slug` is the snake_case identifier used on the
 # wire (matches serde's rename_all = "snake_case" default).
 #
-# Downstream consumers:
-#   - .github/workflows/backend-matrix.yml (vcl-ut) reads this file to
-#     build its matrix strategy, one job per prover.
-#   - Future sync check fails CI if this file drifts from ProverKind::all().
+# This is a declaration inventory, not a claim that each variant has a
+# runnable backend or a successful proof. See verification-integrations.a2ml
+# for the assessed roles of selected tools outside and within this enum.
 #
-# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in src/rust/provers/mod.rs.
+# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in
+# crates/echidna-core/src/prover_kind.rs.
 # If that enum changes, regenerate with scripts/gen-provers-a2ml.sh.
 
 [metadata]
 version = "1.0.0"
-source  = "src/rust/provers/mod.rs::ProverKind"
-date    = "2026-09-25"
+source  = "crates/echidna-core/src/prover_kind.rs::ProverKind"
+date    = "2026-11-07"
 count   = 141
 
 [prover.ABC]
diff --git a/.machine_readable/verification-integrations.a2ml b/.machine_readable/verification-integrations.a2ml
new file mode 100644
index 00000000..c2bfb286
--- /dev/null
+++ b/.machine_readable/verification-integrations.a2ml
@@ -0,0 +1,79 @@
+# SPDX-License-Identifier: MPL-2.0
+# Selected verification-tool roles at the ECHIDNA boundary.
+# This complements provers.a2ml: every enum variant not listed below defaults
+# to declared_unverified. A source file or enum variant is not a successful run.
+# This ledger records source integration, not proof validity or tool health.
+
+[metadata]
+schema = "verification-integrations/1"
+reviewed = "2026-11-07"
+enum_source = "crates/echidna-core/src/prover_kind.rs"
+enum_registry = ".machine_readable/provers.a2ml"
+enum_default = "declared_unverified"
+
+# backend_declared: enum variant and backend source exist; runtime unverified.
+# partial_non_backend: ECHIDNA has corpus/internal code, not a prover backend.
+# via_parent: a language/family served by the named tool, not its own backend.
+# not_integrated: a verifier with no ECHIDNA backend at this review.
+# not_a_prover: language or compute substrate, not a prover integration.
+
+[tool.Idris2]
+status = "backend_declared"
+role = "dependent-type checker"
+prover_kind = "Idris2"
+local_paths = ["src/rust/provers/idris2.rs"]
+
+[tool.GNATprove]
+status = "backend_declared"
+role = "SPARK/Ada verifier"
+prover_kind = "GNATprove"
+local_paths = ["src/rust/provers/gnatprove.rs"]
+
+[tool.SPARK]
+status = "via_parent"
+role = "Ada verification language and toolchain"
+parent_tool = "GNATprove"
+
+[tool.Creusot]
+status = "partial_non_backend"
+role = "Rust deductive verification"
+local_paths = ["src/rust/corpus/creusot.rs", "crates/echidna-core-creusot/src/lib.rs"]
+upstream = "https://github.com/creusot-rs/creusot"
+
+[tool.Pearlite]
+status = "via_parent"
+role = "Creusot specification language"
+parent_tool = "Creusot"
+
+[tool.Verus]
+status = "not_integrated"
+role = "Rust verification"
+upstream = "https://github.com/verus-lang/verus"
+
+[tool.Kani]
+status = "not_integrated"
+role = "Rust model checking"
+upstream = "https://github.com/model-checking/kani"
+
+[tool.Aeneas]
+status = "not_integrated"
+role = "Rust-to-proof translation"
+upstream = "https://github.com/AeneasVerif/aeneas"
+
+[tool.Atoma]
+status = "not_integrated"
+role = "estate Zig verification research prototype"
+upstream = "https://github.com/hyperpolymath/atoma"
+
+[tool.Chapel]
+status = "not_a_prover"
+role = "parallel proof-search compute substrate"
+local_paths = ["src/chapel/parallel_proof_search.chpl"]
+
+[tool.ATS2]
+status = "not_a_prover"
+role = "programming language and type system"
+
+[tool.Zig]
+status = "not_a_prover"
+role = "implementation and FFI language"
diff --git a/docs/PROVER_COUNT.adoc b/docs/PROVER_COUNT.adoc
index 8f6a2f80..a1f1a9cc 100644
--- a/docs/PROVER_COUNT.adoc
+++ b/docs/PROVER_COUNT.adoc
@@ -18,10 +18,16 @@ ____
 
 === TL;DR
 
+Counts describe declarations and source files, not successful tool runs.
+The machine-readable link:../.machine_readable/verification-integrations.a2ml[verification integration ledger]
+distinguishes selected backend, corpus, internal-proof, and non-prover roles.
+Run `python scripts/check-verification-integrations.py` to check its source
+references and the full 141-variant declaration inventory.
+
 [width="100%",cols="34%,33%,33%",options="header",]
 |===
 |Question |Answer |Command
-|Total `+ProverKind+` variants in `+src/rust/provers/mod.rs+` |*141*
+|Total `+ProverKind+` variants in `+crates/echidna-core/src/prover_kind.rs+` |*141*
 |`+V+` below
 
 |Backend implementation files in `+src/rust/provers/+` |*105* |`+F+`
@@ -309,7 +315,7 @@ root.
 [source,bash]
 ----
 # V — total ProverKind variants (141)
-awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' src/rust/provers/mod.rs \
+awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' crates/echidna-core/src/prover_kind.rs \
   | grep -cE '^\s*[A-Z][A-Za-z0-9_]*\s*,'
 
 # F — backend implementation files (105)
@@ -319,15 +325,15 @@ ls src/rust/provers/*.rs | grep -cv 'mod\.rs$'
 git grep -l 'fn suggest_tactics' -- 'src/rust/provers/*.rs' | wc -l
 
 # C — Tier-1 core, exposed by default at GET /api/provers (12)
-awk '/fn all_core/{f=1} f&&/\]/{print;exit} f' src/rust/provers/mod.rs \
+awk '/fn all_core/{f=1} f&&/\]/{print;exit} f' crates/echidna-core/src/prover_kind.rs \
   | grep -oE 'ProverKind::[A-Za-z0-9_]+' | wc -l
 
 # D — variants carrying a type-checker / discipline role (46)
-awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' src/rust/provers/mod.rs \
+awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' crates/echidna-core/src/prover_kind.rs \
   | grep -icE 'typecheck|discipline'
 ----
 
-`+ProverKind::all()+` in `+src/rust/provers/mod.rs+` is the machine
+`+ProverKind::all()+` in `+crates/echidna-core/src/prover_kind.rs+` is the machine
 source of truth; this document is its human-readable mirror. If a count
 changes, update this file *and* `+.machine_readable/provers.a2ml+` in
 the same PR.
@@ -345,5 +351,5 @@ provers`".
 
 If a count changes (new wave absorbed, backend retired), update this
 file in the same PR. The single source of truth for the count is
-`+ProverKind::all()+` in `+src/rust/provers/mod.rs+`; this doc is the
+`+ProverKind::all()+` in `+crates/echidna-core/src/prover_kind.rs+`; this doc is the
 human-readable mirror.
diff --git a/scripts/check-verification-integrations.py b/scripts/check-verification-integrations.py
new file mode 100644
index 00000000..4c4fe7ed
--- /dev/null
+++ b/scripts/check-verification-integrations.py
@@ -0,0 +1,84 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: MPL-2.0
+"""Check the declared prover inventory and the selected integration ledger."""
+
+from __future__ import annotations
+
+import re
+import subprocess
+import sys
+import tomllib
+from datetime import date
+from pathlib import Path
+
+
+ROOT = Path(__file__).resolve().parents[1]
+LEDGER = ROOT / ".machine_readable/verification-integrations.a2ml"
+STATUSES = {
+    "backend_declared",
+    "partial_non_backend",
+    "via_parent",
+    "not_integrated",
+    "not_a_prover",
+}
+
+
+def enum_variants(source: Path) -> set[str]:
+    text = source.read_text(encoding="utf-8")
+    start = text.index("pub enum ProverKind")
+    opening = text.index("{", start)
+    depth = 1
+    cursor = opening + 1
+    while depth:
+        if text[cursor] == "{":
+            depth += 1
+        elif text[cursor] == "}":
+            depth -= 1
+        cursor += 1
+    body = text[opening + 1 : cursor - 1]
+    return set(re.findall(r"^\s*([A-Za-z][A-Za-z0-9_]*)\s*,", body, re.M))
+
+
+def main() -> int:
+    with LEDGER.open("rb") as stream:
+        ledger = tomllib.load(stream)
+    meta = ledger["metadata"]
+    assert meta["schema"] == "verification-integrations/1"
+    assert meta["enum_default"] == "declared_unverified"
+    date.fromisoformat(meta["reviewed"])
+
+    variants = enum_variants(ROOT / meta["enum_source"])
+    with (ROOT / meta["enum_registry"]).open("rb") as stream:
+        registered = tomllib.load(stream)
+    assert set(registered["prover"]) == variants, "provers.a2ml differs from ProverKind"
+    assert registered["metadata"]["count"] == len(variants)
+    assert registered["metadata"]["source"] == f'{meta["enum_source"]}::ProverKind'
+
+    tracked = set(
+        subprocess.check_output(
+            ["git", "ls-tree", "-r", "--name-only", "HEAD"], cwd=ROOT, text=True
+        ).splitlines()
+    )
+    tools = ledger["tool"]
+    for name, entry in tools.items():
+        status = entry["status"]
+        assert status in STATUSES, f"{name}: unknown status {status}"
+        assert entry.get("role"), f"{name}: missing role"
+        variant = entry.get("prover_kind")
+        if status == "backend_declared":
+            assert variant in variants, f"{name}: missing ProverKind {variant}"
+            assert entry.get("local_paths"), f"{name}: missing backend evidence"
+        else:
+            assert variant is None, f"{name}: non-backend entry claims a ProverKind"
+            assert name not in variants, f"{name}: now has a ProverKind; update status"
+        if status == "via_parent":
+            assert entry.get("parent_tool") in tools, f"{name}: missing parent tool"
+        for path in entry.get("local_paths", []):
+            assert path in tracked, f"{name}: missing tracked evidence {path}"
+
+    print(f"OK: {len(variants)} ProverKind declarations; {len(tools)} assessed tool roles")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/gen-provers-a2ml.sh b/scripts/gen-provers-a2ml.sh
index 01cdb4b3..8b4e5b87 100755
--- a/scripts/gen-provers-a2ml.sh
+++ b/scripts/gen-provers-a2ml.sh
@@ -32,22 +32,22 @@ cat << 'HEADER'
 #
 # provers.a2ml — Authoritative enumeration of ECHIDNA prover backends.
 #
-# Generated from src/rust/provers/mod.rs::ProverKind. One section per
+# Generated from crates/echidna-core/src/prover_kind.rs::ProverKind. One section per
 # variant, keyed by the variant's PascalCase name for stability against
 # slug-format drift. `slug` is the snake_case identifier used on the
 # wire (matches serde's rename_all = "snake_case" default).
 #
-# Downstream consumers:
-#   - .github/workflows/backend-matrix.yml (vcl-ut) reads this file to
-#     build its matrix strategy, one job per prover.
-#   - Future sync check fails CI if this file drifts from ProverKind::all().
+# This is a declaration inventory, not a claim that each variant has a
+# runnable backend or a successful proof. See verification-integrations.a2ml
+# for the assessed roles of selected tools outside and within this enum.
 #
-# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in src/rust/provers/mod.rs.
+# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in
+# crates/echidna-core/src/prover_kind.rs.
 # If that enum changes, regenerate with scripts/gen-provers-a2ml.sh.
 
 [metadata]
 version = "1.0.0"
-source  = "src/rust/provers/mod.rs::ProverKind"
+source  = "crates/echidna-core/src/prover_kind.rs::ProverKind"
 HEADER
 
 # Emitted outside the quoted heredoc so it is evaluated at run time rather

From 8f0aef5bfa47fb5d40f74d12d2f55edde95c1bdc Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 7 Nov 2026 01:49:24 +0000
Subject: [PATCH 2/4] Use repository-compliant shell validator

---
 docs/PROVER_COUNT.adoc                     |  2 +-
 scripts/check-verification-integrations.py | 84 ---------------------
 scripts/check-verification-integrations.sh | 87 ++++++++++++++++++++++
 3 files changed, 88 insertions(+), 85 deletions(-)
 delete mode 100644 scripts/check-verification-integrations.py
 create mode 100644 scripts/check-verification-integrations.sh

diff --git a/docs/PROVER_COUNT.adoc b/docs/PROVER_COUNT.adoc
index a1f1a9cc..5fbd0cb8 100644
--- a/docs/PROVER_COUNT.adoc
+++ b/docs/PROVER_COUNT.adoc
@@ -21,7 +21,7 @@ ____
 Counts describe declarations and source files, not successful tool runs.
 The machine-readable link:../.machine_readable/verification-integrations.a2ml[verification integration ledger]
 distinguishes selected backend, corpus, internal-proof, and non-prover roles.
-Run `python scripts/check-verification-integrations.py` to check its source
+Run `bash scripts/check-verification-integrations.sh` to check its source
 references and the full 141-variant declaration inventory.
 
 [width="100%",cols="34%,33%,33%",options="header",]
diff --git a/scripts/check-verification-integrations.py b/scripts/check-verification-integrations.py
deleted file mode 100644
index 4c4fe7ed..00000000
--- a/scripts/check-verification-integrations.py
+++ /dev/null
@@ -1,84 +0,0 @@
-#!/usr/bin/env python3
-# SPDX-License-Identifier: MPL-2.0
-"""Check the declared prover inventory and the selected integration ledger."""
-
-from __future__ import annotations
-
-import re
-import subprocess
-import sys
-import tomllib
-from datetime import date
-from pathlib import Path
-
-
-ROOT = Path(__file__).resolve().parents[1]
-LEDGER = ROOT / ".machine_readable/verification-integrations.a2ml"
-STATUSES = {
-    "backend_declared",
-    "partial_non_backend",
-    "via_parent",
-    "not_integrated",
-    "not_a_prover",
-}
-
-
-def enum_variants(source: Path) -> set[str]:
-    text = source.read_text(encoding="utf-8")
-    start = text.index("pub enum ProverKind")
-    opening = text.index("{", start)
-    depth = 1
-    cursor = opening + 1
-    while depth:
-        if text[cursor] == "{":
-            depth += 1
-        elif text[cursor] == "}":
-            depth -= 1
-        cursor += 1
-    body = text[opening + 1 : cursor - 1]
-    return set(re.findall(r"^\s*([A-Za-z][A-Za-z0-9_]*)\s*,", body, re.M))
-
-
-def main() -> int:
-    with LEDGER.open("rb") as stream:
-        ledger = tomllib.load(stream)
-    meta = ledger["metadata"]
-    assert meta["schema"] == "verification-integrations/1"
-    assert meta["enum_default"] == "declared_unverified"
-    date.fromisoformat(meta["reviewed"])
-
-    variants = enum_variants(ROOT / meta["enum_source"])
-    with (ROOT / meta["enum_registry"]).open("rb") as stream:
-        registered = tomllib.load(stream)
-    assert set(registered["prover"]) == variants, "provers.a2ml differs from ProverKind"
-    assert registered["metadata"]["count"] == len(variants)
-    assert registered["metadata"]["source"] == f'{meta["enum_source"]}::ProverKind'
-
-    tracked = set(
-        subprocess.check_output(
-            ["git", "ls-tree", "-r", "--name-only", "HEAD"], cwd=ROOT, text=True
-        ).splitlines()
-    )
-    tools = ledger["tool"]
-    for name, entry in tools.items():
-        status = entry["status"]
-        assert status in STATUSES, f"{name}: unknown status {status}"
-        assert entry.get("role"), f"{name}: missing role"
-        variant = entry.get("prover_kind")
-        if status == "backend_declared":
-            assert variant in variants, f"{name}: missing ProverKind {variant}"
-            assert entry.get("local_paths"), f"{name}: missing backend evidence"
-        else:
-            assert variant is None, f"{name}: non-backend entry claims a ProverKind"
-            assert name not in variants, f"{name}: now has a ProverKind; update status"
-        if status == "via_parent":
-            assert entry.get("parent_tool") in tools, f"{name}: missing parent tool"
-        for path in entry.get("local_paths", []):
-            assert path in tracked, f"{name}: missing tracked evidence {path}"
-
-    print(f"OK: {len(variants)} ProverKind declarations; {len(tools)} assessed tool roles")
-    return 0
-
-
-if __name__ == "__main__":
-    sys.exit(main())
diff --git a/scripts/check-verification-integrations.sh b/scripts/check-verification-integrations.sh
new file mode 100644
index 00000000..72747ffd
--- /dev/null
+++ b/scripts/check-verification-integrations.sh
@@ -0,0 +1,87 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+enum_source='crates/echidna-core/src/prover_kind.rs'
+registry='.machine_readable/provers.a2ml'
+ledger='.machine_readable/verification-integrations.a2ml'
+
+mapfile -t enum_names < <(awk '
+  /^pub enum ProverKind \{/ { inside = 1; next }
+  inside && /^}/ { exit }
+  inside && /^    [[:alpha:]][[:alnum:]_]*,/ {
+    name = $1; sub(/,$/, "", name); print name
+  }
+' "$enum_source" | LC_ALL=C sort)
+mapfile -t registry_names < <(sed -n 's/^\[prover\.\([[:alnum:]_]*\)\]$/\1/p' "$registry" | LC_ALL=C sort)
+
+if ((${#enum_names[@]} != 141)); then
+  printf 'Expected 141 ProverKind declarations, found %s\n' "${#enum_names[@]}" >&2
+  exit 1
+fi
+if ! diff -u <(printf '%s\n' "${enum_names[@]}") <(printf '%s\n' "${registry_names[@]}"); then
+  printf 'Registry differs from ProverKind declarations\n' >&2
+  exit 1
+fi
+if ! grep -Fxq "enum_source = \"$enum_source\"" "$ledger"; then
+  printf 'Ledger enum_source is stale\n' >&2
+  exit 1
+fi
+if ! grep -Fxq "enum_registry = \"$registry\"" "$ledger"; then
+  printf 'Ledger enum_registry is stale\n' >&2
+  exit 1
+fi
+
+declare -A statuses kinds parents
+while IFS='|' read -r tool status kind parent; do
+  [[ -n "$tool" ]] || continue
+  if [[ -v statuses[$tool] ]]; then
+    printf 'Duplicate tool entry: %s\n' "$tool" >&2; exit 1
+  fi
+  case "$status" in
+    backend_declared|via_parent|partial_non_backend|not_integrated|not_a_prover) ;;
+    *) printf 'Invalid status for %s: %s\n' "$tool" "$status" >&2; exit 1 ;;
+  esac
+  statuses[$tool]="$status"
+  kinds[$tool]="$kind"
+  parents[$tool]="$parent"
+done < <(awk '
+  function emit() { if (tool != "") print tool "|" status "|" kind "|" parent }
+  /^\[tool\.[[:alnum:]_]+\]$/ {
+    emit(); tool = $0; sub(/^\[tool\./, "", tool); sub(/\]$/, "", tool)
+    status = kind = parent = ""; next
+  }
+  tool != "" && /^status = / { status = $3; gsub(/"/, "", status) }
+  tool != "" && /^prover_kind = / { kind = $3; gsub(/"/, "", kind) }
+  tool != "" && /^parent_tool = / { parent = $3; gsub(/"/, "", parent) }
+  END { emit() }
+' "$ledger")
+
+if ((${#statuses[@]} != 12)); then
+  printf 'Expected 12 assessed tool roles, found %s\n' "${#statuses[@]}" >&2
+  exit 1
+fi
+for tool in "${!statuses[@]}"; do
+  if [[ "${statuses[$tool]}" == backend_declared ]]; then
+    if [[ -z "${kinds[$tool]}" ]] || ! printf '%s\n' "${enum_names[@]}" | grep -Fxq "${kinds[$tool]}"; then
+      printf 'Missing declared backend variant for %s\n' "$tool" >&2; exit 1
+    fi
+  elif [[ -n "${kinds[$tool]}" ]]; then
+    printf 'Non-backend %s declares a prover variant\n' "$tool" >&2; exit 1
+  fi
+  if [[ "${statuses[$tool]}" == via_parent ]]; then
+    if [[ -z "${parents[$tool]}" || ! -v statuses[${parents[$tool]}] ]]; then
+      printf 'Missing parent tool for %s\n' "$tool" >&2; exit 1
+    fi
+  fi
+done
+
+while IFS= read -r path; do
+  [[ -n "$path" ]] || continue
+  if ! git cat-file -e "HEAD:$path" 2>/dev/null; then
+    printf 'Missing local evidence path: %s\n' "$path" >&2; exit 1
+  fi
+done < <(sed -n 's/^local_paths = \[\(.*\)\]$/\1/p' "$ledger" | tr -d '" ' | tr ',' '\n')
+
+printf 'OK: %s ProverKind declarations; %s assessed tool roles\n' "${#enum_names[@]}" "${#statuses[@]}"

From 28857396b767e8976ea612af3c9d20116283d6ae Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 7 Nov 2026 02:03:40 +0000
Subject: [PATCH 3/4] Validate integration inventory in existing dogfood gate

---
 .github/workflows/dogfood-gate.yml         |  2 ++
 scripts/check-verification-integrations.sh | 40 +++++++++++++++++++---
 2 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 0729c2be..29bd304e 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -57,6 +57,8 @@ jobs:
         run: |
           bash scripts/ci/test-manifest-validator-regressions.sh
           bash .github/hooks/validate-a2ml.sh
+      - name: Check prover integration inventory
+        run: bash scripts/check-verification-integrations.sh
       - name: Write summary
         run: |
           A2ML_COUNT="${{ steps.detect.outputs.count }}"
diff --git a/scripts/check-verification-integrations.sh b/scripts/check-verification-integrations.sh
index 72747ffd..4db3630d 100644
--- a/scripts/check-verification-integrations.sh
+++ b/scripts/check-verification-integrations.sh
@@ -24,6 +24,16 @@ if ! diff -u <(printf '%s\n' "${enum_names[@]}") <(printf '%s\n' "${registry_nam
   printf 'Registry differs from ProverKind declarations\n' >&2
   exit 1
 fi
+if ! grep -Eq '^count[[:space:]]*=[[:space:]]*141$' "$registry" ||
+   ! grep -Eq '^source[[:space:]]*=[[:space:]]*"crates/echidna-core/src/prover_kind.rs::ProverKind"$' "$registry"; then
+  printf 'Registry count or source metadata is stale\n' >&2
+  exit 1
+fi
+if ! grep -Fxq 'schema = "verification-integrations/1"' "$ledger" ||
+   ! grep -Fxq 'enum_default = "declared_unverified"' "$ledger"; then
+  printf 'Ledger schema or default status is stale\n' >&2
+  exit 1
+fi
 if ! grep -Fxq "enum_source = \"$enum_source\"" "$ledger"; then
   printf 'Ledger enum_source is stale\n' >&2
   exit 1
@@ -33,8 +43,16 @@ if ! grep -Fxq "enum_registry = \"$registry\"" "$ledger"; then
   exit 1
 fi
 
-declare -A statuses kinds parents
-while IFS='|' read -r tool status kind parent; do
+awk '
+  /^[[:space:]]*$/ || /^#/ { next }
+  /^\[metadata\]$/ || /^\[tool\.[[:alnum:]_]+\]$/ { next }
+  /^[a-z_]+ = "[^"]*"$/ { next }
+  /^local_paths = \["[^"]+"(, "[^"]+")*\]$/ { next }
+  { printf "Unsupported or malformed ledger line %d: %s\n", NR, $0 > "/dev/stderr"; exit 1 }
+' "$ledger"
+
+declare -A statuses kinds parents roles evidence
+while IFS='|' read -r tool status kind parent role has_paths; do
   [[ -n "$tool" ]] || continue
   if [[ -v statuses[$tool] ]]; then
     printf 'Duplicate tool entry: %s\n' "$tool" >&2; exit 1
@@ -46,15 +64,19 @@ while IFS='|' read -r tool status kind parent; do
   statuses[$tool]="$status"
   kinds[$tool]="$kind"
   parents[$tool]="$parent"
+  roles[$tool]="$role"
+  evidence[$tool]="$has_paths"
 done < <(awk '
-  function emit() { if (tool != "") print tool "|" status "|" kind "|" parent }
+  function emit() { if (tool != "") print tool "|" status "|" kind "|" parent "|" role "|" has_paths }
   /^\[tool\.[[:alnum:]_]+\]$/ {
     emit(); tool = $0; sub(/^\[tool\./, "", tool); sub(/\]$/, "", tool)
-    status = kind = parent = ""; next
+    status = kind = parent = role = has_paths = ""; next
   }
   tool != "" && /^status = / { status = $3; gsub(/"/, "", status) }
   tool != "" && /^prover_kind = / { kind = $3; gsub(/"/, "", kind) }
   tool != "" && /^parent_tool = / { parent = $3; gsub(/"/, "", parent) }
+  tool != "" && /^role = / { role = $0; sub(/^role = "/, "", role); sub(/"$/, "", role) }
+  tool != "" && /^local_paths = / { has_paths = "yes" }
   END { emit() }
 ' "$ledger")
 
@@ -63,13 +85,23 @@ if ((${#statuses[@]} != 12)); then
   exit 1
 fi
 for tool in "${!statuses[@]}"; do
+  if [[ -z "${roles[$tool]}" ]]; then
+    printf 'Missing role for %s\n' "$tool" >&2; exit 1
+  fi
   if [[ "${statuses[$tool]}" == backend_declared ]]; then
     if [[ -z "${kinds[$tool]}" ]] || ! printf '%s\n' "${enum_names[@]}" | grep -Fxq "${kinds[$tool]}"; then
       printf 'Missing declared backend variant for %s\n' "$tool" >&2; exit 1
     fi
+    if [[ "${evidence[$tool]}" != yes ]]; then
+      printf 'Missing local backend evidence for %s\n' "$tool" >&2; exit 1
+    fi
   elif [[ -n "${kinds[$tool]}" ]]; then
     printf 'Non-backend %s declares a prover variant\n' "$tool" >&2; exit 1
   fi
+  if [[ "${statuses[$tool]}" == not_integrated || "${statuses[$tool]}" == not_a_prover ]] &&
+     printf '%s\n' "${enum_names[@]}" | grep -Fxq "$tool"; then
+    printf '%s is declared in ProverKind but marked %s\n' "$tool" "${statuses[$tool]}" >&2; exit 1
+  fi
   if [[ "${statuses[$tool]}" == via_parent ]]; then
     if [[ -z "${parents[$tool]}" || ! -v statuses[${parents[$tool]}] ]]; then
       printf 'Missing parent tool for %s\n' "$tool" >&2; exit 1

From 16a80b13c07c79448b9f5f108ff359063283b9d2 Mon Sep 17 00:00:00 2001
From: "coderabbitai[bot]"
 <136622811+coderabbitai[bot]@users.noreply.github.com>
Date: Sat, 7 Nov 2026 07:27:23 +0000
Subject: [PATCH 4/4] docs(scripts): Document AWK emit output in verification
 integration checker

<!-- coderabbit-ai-generated:v1 -->
---
 scripts/check-verification-integrations.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/scripts/check-verification-integrations.sh b/scripts/check-verification-integrations.sh
index 4db3630d..a24fa461 100644
--- a/scripts/check-verification-integrations.sh
+++ b/scripts/check-verification-integrations.sh
@@ -67,6 +67,8 @@ while IFS='|' read -r tool status kind parent role has_paths; do
   roles[$tool]="$role"
   evidence[$tool]="$has_paths"
 done < <(awk '
+  # Write the current tool, status, kind, parent, role and path-presence flag
+  # to stdout as one pipe-delimited line; emit nothing when tool is empty.
   function emit() { if (tool != "") print tool "|" status "|" kind "|" parent "|" role "|" has_paths }
   /^\[tool\.[[:alnum:]_]+\]$/ {
     emit(); tool = $0; sub(/^\[tool\./, "", tool); sub(/\]$/, "", tool)