From 52c5fba4e35e40b639c18b8bfbbd8457c902afc8 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 25 Sep 2026 14:34:10 +0000
Subject: [PATCH 1/2] feat(chapel): per-prover outcome telemetry for bench_mrr

Implements #162. The L2.3 ADR introduced exitCode = -5 for preempted
losers, distinct from -3 (timeout) and -4 (subprocess error), but
bench_mrr only reported success/winning_prover per strategy run, so the
wall-clock improvement attributable to preemption was not measurable.

Outcome model (parallel_proof_search.chpl):

- New ProverOutcome enum plus outcomeLabel/categoryLabel/classifyOutcome
  mapping the documented exit-code contract: 0 success, >0 prover
  rejection, -1 not on PATH, -2 temp-file write failure, -3 timeout,
  -4 spawn/IO error, -5 preempted. The two -2/-4 causes collapse into
  subprocess_error because both mean the prover never got a fair hearing.
- NotAttempted is deliberately not an exit code: the sequential strategy
  returns at the first success, so provers after the winner are reported
  as not_attempted rather than silently dropped from the breakdown.
- Each strategy gains a telemetry variant that fills a per-prover
  results/attempted table indexed by provers.domain (not ProverInfo.id,
  so filtered registries stay correctly indexed). The existing public
  procs are now thin wrappers over those variants, so what the bench
  measures and what it reports are the same code path.

Outputs (bench_mrr.chpl):

- stdout wall-clock CSV, unchanged columns.
- bench_mrr_telemetry.csv: one row per prover per fixture x strategy
  (360 rows for the stock matrix), never omitting rows.
- bench_mrr_summary.csv: per fixture x strategy plus an ALL row per
  strategy aggregating the corpus, with preemption_rate =
  preempted/attempted_total measured against provers that actually ran.
- --telemetry-only=true omits the stdout wall-clock CSV.

Also adds `just bench-chapel-mrr-telemetry`, gitignores the generated
CSVs, and documents the column contracts in docs/bench/README.adoc.

NOT VERIFIED BY EXECUTION: this environment has no Chapel toolchain, so
bench_mrr could not be built or run. The acceptance criterion asking for
a re-run showing preemption rates next to wall-clock is therefore not
satisfied here; docs/bench/README.adoc records the re-run procedure and
the baseline writeup is explicitly left un-refreshed rather than filled
with estimates.

Refs #162

Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
---
 .gitignore                                    |   3 +
 Justfile                                      |  21 ++
 .../bench/2026-05-30-chapel-mrr-baseline.adoc |  15 +-
 docs/bench/README.adoc                        | 129 +++++++++
 src/chapel/bench_mrr.chpl                     | 274 +++++++++++++++---
 src/chapel/parallel_proof_search.chpl         | 178 ++++++++++--
 6 files changed, 557 insertions(+), 63 deletions(-)
 create mode 100644 docs/bench/README.adoc

diff --git a/.gitignore b/.gitignore
index e7d095d0..dc5e9dfd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -65,6 +65,9 @@ src/chapel/chapel_smoke
 src/chapel/chapel_smoke_real
 src/chapel/bench_mrr
 src/chapel/bench_mrr_real
+# bench_mrr generated CSVs (#162) — regenerated per run, not tracked
+src/chapel/bench_mrr_telemetry.csv
+src/chapel/bench_mrr_summary.csv
 src/chapel/libechidna_chapel.h
 
 # Zig
diff --git a/Justfile b/Justfile
index 3b97515e..7fc65461 100644
--- a/Justfile
+++ b/Justfile
@@ -666,6 +666,27 @@ bench-chapel-mrr:
     cd src/chapel
     chpl -o bench_mrr bench_mrr.chpl
     ./bench_mrr --verbose=false --timeout=10
+    echo "# wrote src/chapel/bench_mrr_telemetry.csv + src/chapel/bench_mrr_summary.csv" >&2
+
+# Same bench, but surface only the corpus-level outcome breakdown: the
+# per-prover preempted / timed-out / success counts and the preemption
+# rate next to wall-clock, one line per strategy. This is the #162 view —
+# it answers "how much of the speculative win is preemption?" without
+# opening the 360-row telemetry file.
+bench-chapel-mrr-telemetry:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    if command -v idris2 >/dev/null 2>&1 && [ -z "${IDRIS2_PREFIX:-}" ]; then
+      export IDRIS2_PREFIX="$(dirname "$(dirname "$(readlink -f "$(command -v idris2)")")")"
+    fi
+    cd src/chapel
+    chpl -o bench_mrr bench_mrr.chpl
+    ./bench_mrr --verbose=false --timeout=10 --telemetry-only=true
+    echo "corpus-level outcome breakdown (fixture=ALL):"
+    grep '^ALL,' bench_mrr_summary.csv | while IFS=, read -r _ strategy att ok fail preempt timeout na err notatt rate wall _ _; do
+      printf '  %-22s attempted=%-3s success=%-3s failure=%-3s preempted=%-3s timed_out=%-3s rate=%s wall=%ss\n' \
+        "$strategy" "$att" "$ok" "$fail" "$preempt" "$timeout" "$rate" "$wall"
+    done
 
 # Rebuild Chapel 2.8.0 from source with CHPL_LIB_PIC=pic so that
 # `chpl --library --dynamic` can produce a shared-library form of the
diff --git a/docs/bench/2026-05-30-chapel-mrr-baseline.adoc b/docs/bench/2026-05-30-chapel-mrr-baseline.adoc
index ab89b2a8..5d690ea3 100644
--- a/docs/bench/2026-05-30-chapel-mrr-baseline.adoc
+++ b/docs/bench/2026-05-30-chapel-mrr-baseline.adoc
@@ -140,6 +140,15 @@ immediately, so the parallel strategies pay coforall spawn overhead with
 no benefit. The trivial-goal regime observation from the original bench
 applies symmetrically here.
 
-Wave-3 follow-ups still open: real-corpus speedup bench (#161, 10-30 s
-prover invocations) and per-prover preempted/timeout/success telemetry
-(#162).
+Wave-3 follow-ups: real-corpus speedup bench (#161, 10-30 s prover
+invocations) is still open. Per-prover preempted/timeout/success telemetry
+(#162) is now *implemented* — `+bench_mrr+` emits
+`+bench_mrr_telemetry.csv+` and `+bench_mrr_summary.csv+`, and
+`+just bench-chapel-mrr-telemetry+` prints the corpus-level breakdown.
+See `+docs/bench/README.adoc+` for the column contracts.
+
+The readings in *this* file predate that telemetry, so they carry no
+preemption counts: a re-run on a Chapel-enabled host is required to put
+preemption rates next to wall-clock. That re-run has not been performed —
+the telemetry was authored without a Chapel toolchain available, and this
+table is deliberately left un-refreshed rather than filled with estimates.
diff --git a/docs/bench/README.adoc b/docs/bench/README.adoc
new file mode 100644
index 00000000..0ac474e1
--- /dev/null
+++ b/docs/bench/README.adoc
@@ -0,0 +1,129 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 ECHIDNA Project Contributors
+
+= Chapel benchmark artifacts
+
+This directory holds the recorded outputs of
+`+src/chapel/bench_mrr.chpl+` and the writeups that interpret them.
+
+[cols=",",options="header",]
+|===
+|File |What it is
+|`+2026-05-30-chapel-mrr-baseline.adoc+` |Wave-1 writeup: three strategies, wall-clock and winner per fixture.
+|`+2026-05-30-chapel-mrr-baseline.csv+` |The raw 5-run readings that writeup is based on.
+|===
+
+== The bench
+
+`+bench_mrr+` reads each fixture from `+tests/chapel_fixtures/+` and calls
+each of the three search strategies with the same goal string and the full
+30-prover registry:
+
+* `+sequentialProofSearch+` — serial fallback.
+* `+parallelProofSearch+` — best-of: `+coforall+` over all provers, return
+  the fastest success. Wall time is bounded by the slowest task.
+* `+parallelProofSearchSpeculative+` — first-success-wins via atomic CAS,
+  with L2.3 cancel-token preemption of the losers.
+
+== Outputs
+
+Run `+just bench-chapel-mrr+`. It writes three tables.
+
+=== 1. Wall-clock + winner (stdout)
+
+[source]
+----
+fixture,strategy,wallclock_s,success,winning_prover
+----
+
+Pass `+--verbose=false+` (the Justfile recipes do) or the strategy progress
+chatter interleaves with this CSV.
+
+=== 2. Per-prover telemetry (`+bench_mrr_telemetry.csv+`)
+
+One row per prover per fixture × strategy — 360 rows for the stock 4-fixture
+× 3-strategy × 30-prover matrix.
+
+[source]
+----
+fixture,strategy,prover,prover_id,category,outcome,exit_code,wallclock_s
+----
+
+Rows are never omitted. A prover the *sequential* strategy never reached
+because an earlier prover already won is reported as `+not_attempted+`, so
+the per-strategy counts always sum to the registry size. `+outcome+` is one
+of:
+
+[cols=",",options="header",]
+|===
+|Outcome |Meaning
+|`+completed_success+` |Prover ran, exit status 0.
+|`+completed_failure+` |Prover ran and rejected the goal.
+|`+preempted+` |Exit `+-5+`: SIGKILLed by the L2.3 cancel token after the speculative winner was declared.
+|`+timed_out+` |Exit `+-3+`: wall timeout reached, subprocess SIGKILLed.
+|`+not_available+` |Exit `+-1+`: executable not on PATH. Never invoked.
+|`+subprocess_error+` |Exit `+-2+` (ECHIDNA failed to write the temp goal) or `+-4+` (spawn/IO exception).
+|`+not_attempted+` |Sequential returned before reaching this prover. Not an exit code.
+|===
+
+=== 3. Per-strategy summary (`+bench_mrr_summary.csv+`)
+
+One row per fixture × strategy, plus a `+fixture=ALL+` row per strategy
+aggregating the corpus.
+
+[source]
+----
+fixture,strategy,attempted_total,completed_success,completed_failure,
+preempted,timed_out,not_available,subprocess_error,not_attempted,
+preemption_rate,wallclock_s,success,winning_prover
+----
+
+`+preemption_rate+` is `+preempted / attempted_total+` — measured against
+provers that actually ran, not against the whole registry, because a rate
+over provers that were never invoked would be meaningless. The `+ALL+` rows
+are the quick answer to "how much of the speculative wall-clock win is
+preemption?".
+
+`+just bench-chapel-mrr-telemetry+` runs the bench and prints only those
+`+ALL+` rows, one line per strategy.
+
+=== `+--telemetry-only+`
+
+`+--telemetry-only=true+` omits the stdout wall-clock CSV so a run produces
+only the two files. The searches still execute — an outcome cannot be
+observed without invoking the prover — and the timing values inside the two
+files stay populated, because they are already measured and cost nothing to
+keep.
+
+== Re-run status
+
+The telemetry columns were added for issue #162. *The recorded numbers have
+not yet been refreshed*: the change was authored in an environment with no
+Chapel toolchain, so `+bench_mrr+` could not be built or executed there, and
+inventing plausible figures would be worse than leaving this section empty.
+
+To produce the post-#162 readings on a Chapel-enabled host:
+
+[source,bash]
+----
+just bench-chapel-mrr            # wall-clock CSV to stdout + both files
+just bench-chapel-mrr-telemetry  # corpus-level rates only
+
+# Then record the run:
+cp src/chapel/bench_mrr_summary.csv docs/bench/<date>-chapel-mrr-telemetry.csv
+----
+
+Expected shape of the result, which is the hypothesis the bench exists to
+test: in the trivial-goal regime the speculative strategy's losers are
+preempted rather than allowed to finish, so its `+preempted+` count should
+be large and its `+attempted_total+` should still equal the registry size;
+`+sequential+` should show a large `+not_attempted+` count, because it stops
+at the first success. Both are consequences of the L2.3 design and neither
+is currently measured anywhere.
+
+== Related
+
+* `+docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc+` — the `+-5+`
+  preemption contract and why it is distinct from `+-3+`.
+* `+proofs/agda/ParallelSoundness.agda+` — cancellation-safety.
+* `+docs/handover/TODO.adoc+` — real-corpus speedup bench (#161).
diff --git a/src/chapel/bench_mrr.chpl b/src/chapel/bench_mrr.chpl
index b0833dae..a218f22c 100644
--- a/src/chapel/bench_mrr.chpl
+++ b/src/chapel/bench_mrr.chpl
@@ -3,13 +3,55 @@
 //
 // Chapel speedup baseline — runs sequentialProofSearch,
 // parallelProofSearch (best-of), and parallelProofSearchSpeculative
-// against a small fixture corpus and emits a CSV table comparing
-// wall-clock time and the winning prover.
+// against a small fixture corpus and emits three CSV tables:
+//
+//   1. wall-clock + winner       -> stdout
+//   2. per-prover outcome rows   -> --telemetry-out
+//   3. per-strategy summary      -> --summary-out
 //
 // Build: chpl -o bench_mrr bench_mrr.chpl
-// Run:   ./bench_mrr  --timeout=10
+// Run:   ./bench_mrr --verbose=false --timeout=10
+//
+// Pass `--verbose=false` to keep progress chatter out of the stdout CSV;
+// the `bench-chapel-mrr` Justfile recipe already does this.
+//
+// ---------------------------------------------------------------------------
+// Output contracts (column names are stable; see docs/bench/)
+// ---------------------------------------------------------------------------
+//
+// Stdout, one row per fixture x strategy:
+//   fixture,strategy,wallclock_s,success,winning_prover
+//
+// Telemetry (--telemetry-out), one row per prover per fixture x strategy,
+// so 4 fixtures x 3 strategies x 30 provers = 360 rows for the stock
+// registry. Rows are never omitted: a prover the sequential strategy
+// never reached is reported as `not_attempted` rather than dropped, so
+// the per-strategy counts always sum to the registry size.
+//   fixture,strategy,prover,prover_id,category,outcome,exit_code,wallclock_s
+//
+// `outcome` is one of:
+//   completed_success  prover ran, exit status 0
+//   completed_failure  prover ran and rejected the goal
+//   preempted          exit -5, L2.3 SIGKILL by the speculative winner
+//   timed_out          exit -3, wall timeout reached
+//   not_available      exit -1, executable not on PATH (never invoked)
+//   subprocess_error   exit -2 (temp-file write) or -4 (spawn/IO)
+//   not_attempted      sequential returned before reaching this prover
 //
-// CSV columns: fixture,strategy,wallclock_s,success,winning_prover
+// Summary (--summary-out), one row per fixture x strategy plus one
+// `ALL` row per strategy aggregating the corpus. Preemption rate is
+// `preempted / attempted_total`, so it is measured against provers that
+// actually ran, not against the whole registry.
+//   fixture,strategy,attempted_total,completed_success,completed_failure,
+//   preempted,timed_out,not_available,subprocess_error,not_attempted,
+//   preemption_rate,wallclock_s,success,winning_prover
+//
+// --telemetry-only=true omits the stdout wall-clock CSV, so a run
+// produces only the two files. The searches themselves still execute —
+// an outcome cannot be observed without invoking the prover — and the
+// timing values inside the two files stay populated, because they are
+// already measured and cost nothing to keep. The flag is about not
+// emitting the timing table, not about avoiding the work.
 //
 // The fixture corpus is intentionally tiny (one trivially-true goal
 // per available prover language) so the bench completes in well
@@ -22,12 +64,30 @@ use IO;
 
 config const timeout = 10;
 config const fixtureDir = "../../tests/chapel_fixtures";
+config const telemetryOut = "bench_mrr_telemetry.csv";
+config const summaryOut = "bench_mrr_summary.csv";
+config const telemetryOnly = false;
 
 record Fixture {
     var name: string;
     var path: string;
 }
 
+// Tally of `ProverOutcome` values for one fixture x strategy cell.
+// `attempted_total` excludes `not_attempted` by construction, because a
+// preemption rate over provers that were never invoked would be
+// meaningless.
+record OutcomeCounts {
+    var attempted_total: int = 0;
+    var completed_success: int = 0;
+    var completed_failure: int = 0;
+    var preempted: int = 0;
+    var timed_out: int = 0;
+    var not_available: int = 0;
+    var subprocess_error: int = 0;
+    var not_attempted: int = 0;
+}
+
 proc loadFixture(name: string, path: string): string throws {
     var f = open(path, ioMode.r);
     var r = f.reader();
@@ -38,43 +98,104 @@ proc loadFixture(name: string, path: string): string throws {
     return buf;
 }
 
-proc benchOne(goal: string, fixtureName: string, allProvers: [] ProverInfo,
-              timeout: int) {
-
-    // sequential
-    {
-        var t = new stopwatch();
-        t.start();
-        const res = sequentialProofSearch(goal, allProvers, timeout);
-        t.stop();
-        writef("%s,sequential,%.3dr,%s,%s\n",
-               fixtureName, t.elapsed(),
-               if res.success then "true" else "false",
-               if res.success then res.prover else "—");
-    }
+// ---------------------------------------------------------------------------
+// Tallying
+// ---------------------------------------------------------------------------
 
-    // parallel best-of (waits for all)
-    {
-        var t = new stopwatch();
-        t.start();
-        const res = parallelProofSearch(goal, allProvers, timeout);
-        t.stop();
-        writef("%s,parallel_bestof,%.3dr,%s,%s\n",
-               fixtureName, t.elapsed(),
-               if res.success then "true" else "false",
-               if res.success then res.prover else "—");
+proc tallyOutcome(ref c: OutcomeCounts, o: ProverOutcome) {
+    if o == ProverOutcome.NotAttempted {
+        c.not_attempted += 1;
+        return;
     }
 
-    // parallel speculative (first-success-wins)
-    {
-        var t = new stopwatch();
-        t.start();
-        const res = parallelProofSearchSpeculative(goal, allProvers, timeout);
-        t.stop();
-        writef("%s,parallel_speculative,%.3dr,%s,%s\n",
-               fixtureName, t.elapsed(),
-               if res.success then "true" else "false",
-               if res.success then res.prover else "—");
+    c.attempted_total += 1;
+
+    // Plain if/else-if rather than `select`: the branches are
+    // statements, not returns, and this keeps exhaustiveness obvious.
+    if o == ProverOutcome.CompletedSuccess then c.completed_success += 1;
+    else if o == ProverOutcome.CompletedFailure then c.completed_failure += 1;
+    else if o == ProverOutcome.Preempted then c.preempted += 1;
+    else if o == ProverOutcome.TimedOut then c.timed_out += 1;
+    else if o == ProverOutcome.NotAvailable then c.not_available += 1;
+    else if o == ProverOutcome.SubprocessError then c.subprocess_error += 1;
+}
+
+proc addCounts(ref dst: OutcomeCounts, const ref src: OutcomeCounts) {
+    dst.attempted_total   += src.attempted_total;
+    dst.completed_success += src.completed_success;
+    dst.completed_failure += src.completed_failure;
+    dst.preempted         += src.preempted;
+    dst.timed_out         += src.timed_out;
+    dst.not_available     += src.not_available;
+    dst.subprocess_error  += src.subprocess_error;
+    dst.not_attempted     += src.not_attempted;
+}
+
+// Preempted as a fraction of provers that actually ran. Rendered with
+// the same width as the wallclock column so the two line up in a table.
+proc preemptionRate(const ref c: OutcomeCounts): real {
+    if c.attempted_total == 0 then return 0.0;
+    return c.preempted:real / c.attempted_total:real;
+}
+
+// ---------------------------------------------------------------------------
+// CSV line builders
+// ---------------------------------------------------------------------------
+
+proc wallclockLine(fixture: string, strategy: string, wall: real,
+                   res: ProofResult): string {
+    return fixture + "," + strategy + "," + wall:string + ","
+         + (if res.success then "true" else "false") + ","
+         + (if res.success then res.prover else "—");
+}
+
+proc telemetryLine(fixture: string, strategy: string, p: ProverInfo,
+                   r: ProofResult, o: ProverOutcome, wall: real): string {
+    return fixture + "," + strategy + "," + p.name + "," + p.id:string + ","
+         + categoryLabel(p.category) + "," + outcomeLabel(o) + ","
+         + r.exitCode:string + "," + wall:string;
+}
+
+proc summaryLine(fixture: string, strategy: string, const ref c: OutcomeCounts,
+                 wall: real, res: ProofResult): string {
+    return fixture + "," + strategy + ","
+         + c.attempted_total:string + "," + c.completed_success:string + ","
+         + c.completed_failure:string + "," + c.preempted:string + ","
+         + c.timed_out:string + "," + c.not_available:string + ","
+         + c.subprocess_error:string + "," + c.not_attempted:string + ","
+         + preemptionRate(c):string + "," + wall:string + ","
+         + (if res.success then "true" else "false") + ","
+         + (if res.success then res.prover else "—");
+}
+
+// Corpus-level row: wall-clock sums across fixtures; there is no single
+// winning prover, so those two columns are left empty.
+proc corpusSummaryLine(strategy: string, const ref c: OutcomeCounts,
+                       wall: real): string {
+    return "ALL," + strategy + ","
+         + c.attempted_total:string + "," + c.completed_success:string + ","
+         + c.completed_failure:string + "," + c.preempted:string + ","
+         + c.timed_out:string + "," + c.not_available:string + ","
+         + c.subprocess_error:string + "," + c.not_attempted:string + ","
+         + preemptionRate(c):string + "," + wall:string + ",,";
+}
+
+// ---------------------------------------------------------------------------
+// Strategy dispatch
+// ---------------------------------------------------------------------------
+
+// Index into the strategy list below. Returns the same verdict the
+// public (telemetry-free) strategy procs return, while filling the
+// per-prover table.
+proc runStrategy(si: int, goal: string, provers: [] ProverInfo,
+                 ref results: [] ProofResult, ref attempted: [] bool,
+                 timeout: int): ProofResult {
+    if si == 0 {
+        return sequentialProofSearchTelemetry(goal, provers, results, attempted, timeout);
+    } else if si == 1 {
+        return parallelProofSearchTelemetry(goal, provers, results, attempted, timeout);
+    } else {
+        return parallelProofSearchSpeculativeTelemetry(goal, provers, results, attempted, timeout);
     }
 }
 
@@ -88,16 +209,87 @@ proc main(): int {
         new Fixture("agda_trivial",   fixtureDir + "/agda_trivial.agda")
     ];
 
-    writeln("fixture,strategy,wallclock_s,success,winning_prover");
+    const strategyNames: [0..2] string = [
+        "sequential", "parallel_bestof", "parallel_speculative"
+    ];
+
+    const wallclockHeader =
+        "fixture,strategy,wallclock_s,success,winning_prover";
+    const telemetryHeader =
+        "fixture,strategy,prover,prover_id,category,outcome,exit_code,wallclock_s";
+    const summaryHeader =
+        "fixture,strategy,attempted_total,completed_success,completed_failure,"
+        + "preempted,timed_out,not_available,subprocess_error,not_attempted,"
+        + "preemption_rate,wallclock_s,success,winning_prover";
+
+    var teleFile = open(telemetryOut, ioMode.cw);
+    var teleW = teleFile.writer(locking=false);
+    var sumFile = open(summaryOut, ioMode.cw);
+    var sumW = sumFile.writer(locking=false);
+
+    teleW.write(telemetryHeader + "\n");
+    sumW.write(summaryHeader + "\n");
+
+    if !telemetryOnly then
+        writeln(wallclockHeader);
+
+    var corpusTotals: [strategyNames.domain] OutcomeCounts;
+    var corpusWall: [strategyNames.domain] real;
+
     for fx in fixtures {
         var goal: string;
         try {
             goal = loadFixture(fx.name, fx.path);
         } catch e {
-            writef("%s,LOAD_ERROR,0.0,false,%s\n", fx.name, e.message());
+            if !telemetryOnly then
+                writeln(fx.name, ",LOAD_ERROR,0.0,false,", e.message());
             continue;
         }
-        benchOne(goal, fx.name, allProvers, timeout);
+
+        for si in strategyNames.domain {
+            const strategy = strategyNames[si];
+
+            var results: [allProvers.domain] ProofResult;
+            var attempted: [allProvers.domain] bool;
+
+            var t = new stopwatch();
+            t.start();
+            const verdict = runStrategy(si, goal, allProvers, results, attempted, timeout);
+            t.stop();
+            const wall = t.elapsed();
+
+            if !telemetryOnly then
+                writeln(wallclockLine(fx.name, strategy, wall, verdict));
+
+            // One telemetry row per registry entry, always.
+            var counts: OutcomeCounts;
+            for i in allProvers.domain {
+                const o = classifyOutcome(results[i], attempted[i]);
+                tallyOutcome(counts, o);
+                teleW.write(telemetryLine(fx.name, strategy, allProvers[i],
+                                          results[i], o, wall) + "\n");
+            }
+
+            sumW.write(summaryLine(fx.name, strategy, counts, wall, verdict) + "\n");
+            addCounts(corpusTotals[si], counts);
+            corpusWall[si] += wall;
+        }
     }
+
+    for si in strategyNames.domain {
+        sumW.write(corpusSummaryLine(strategyNames[si], corpusTotals[si],
+                                     corpusWall[si]) + "\n");
+    }
+
+    teleW.close();
+    teleFile.close();
+    sumW.close();
+    sumFile.close();
+
+    if verbose {
+        writeln("\nWrote per-prover telemetry -> ", telemetryOut);
+        writeln("Wrote per-strategy summary -> ", summaryOut);
+    }
+
     return 0;
 }
diff --git a/src/chapel/parallel_proof_search.chpl b/src/chapel/parallel_proof_search.chpl
index 53057a85..f808ca28 100644
--- a/src/chapel/parallel_proof_search.chpl
+++ b/src/chapel/parallel_proof_search.chpl
@@ -177,6 +177,88 @@ record ProofResult {
     var category: ProverCategory;
 }
 
+// ---------------------------------------------------------------------------
+// Per-prover outcome telemetry (#162)
+// ---------------------------------------------------------------------------
+
+// Categorical outcome of a single prover attempt. The exit-code
+// encoding is the L2.3 contract (see
+// docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc):
+//
+//      0 -> CompletedSuccess   prover ran, exit status 0
+//     >0 -> CompletedFailure   prover ran and rejected the goal
+//     -1 -> NotAvailable       executable not on PATH (never invoked)
+//     -2 -> SubprocessError    ECHIDNA-side failure writing the temp goal
+//     -3 -> TimedOut           wall timeout reached, subprocess SIGKILLed
+//     -4 -> SubprocessError    spawn/IO exception around the subprocess
+//     -5 -> Preempted          L2.3 SIGKILL by the speculative winner
+//
+// `NotAttempted` is deliberately not an exit code. The sequential
+// strategy returns as soon as a prover succeeds, so the provers after
+// the winner are never invoked; they are reported as NotAttempted so
+// the breakdown still accounts for every registry entry instead of
+// silently dropping rows.
+enum ProverOutcome {
+    CompletedSuccess,
+    CompletedFailure,
+    NotAvailable,
+    TimedOut,
+    Preempted,
+    SubprocessError,
+    NotAttempted
+}
+
+// Stable lowercase labels — these are the literal CSV values, so they
+// are part of the bench output contract. Do not rename without
+// updating docs/bench/.
+proc outcomeLabel(o: ProverOutcome): string {
+    select o {
+        when ProverOutcome.CompletedSuccess do return "completed_success";
+        when ProverOutcome.CompletedFailure do return "completed_failure";
+        when ProverOutcome.NotAvailable     do return "not_available";
+        when ProverOutcome.TimedOut         do return "timed_out";
+        when ProverOutcome.Preempted        do return "preempted";
+        when ProverOutcome.SubprocessError  do return "subprocess_error";
+        when ProverOutcome.NotAttempted     do return "not_attempted";
+    }
+    return "unknown";
+}
+
+// Stable lowercase category labels for the telemetry CSV.
+proc categoryLabel(cat: ProverCategory): string {
+    select cat {
+        when ProverCategory.InteractiveAssistant do return "interactive_assistant";
+        when ProverCategory.SmtSolver            do return "smt_solver";
+        when ProverCategory.FirstOrderAtp        do return "first_order_atp";
+        when ProverCategory.DeclarativeProver    do return "declarative_prover";
+        when ProverCategory.AutoActive           do return "auto_active";
+        when ProverCategory.ConstraintSolver     do return "constraint_solver";
+    }
+    return "unknown";
+}
+
+// Classify one prover result. `wasAttempted` is false for provers the
+// sequential strategy skipped after an earlier success.
+//
+// Note the two distinct `SubprocessError` causes (-2 temp-file write,
+// -4 spawn/IO exception): both mean the prover never got a fair
+// hearing, which is why they are one category rather than two.
+proc classifyOutcome(r: ProofResult, wasAttempted: bool): ProverOutcome {
+    if !wasAttempted then return ProverOutcome.NotAttempted;
+    if r.success then return ProverOutcome.CompletedSuccess;
+    select r.exitCode {
+        when -1 do return ProverOutcome.NotAvailable;
+        when -2 do return ProverOutcome.SubprocessError;
+        when -3 do return ProverOutcome.TimedOut;
+        when -4 do return ProverOutcome.SubprocessError;
+        when -5 do return ProverOutcome.Preempted;
+        otherwise do return ProverOutcome.CompletedFailure;
+    }
+    // Unreachable: every branch returns. Kept so the return type is
+    // satisfied on all paths, mirroring `categoryToInt` above.
+    return ProverOutcome.CompletedFailure;
+}
+
 // ---------------------------------------------------------------------------
 // Prover availability check
 // ---------------------------------------------------------------------------
@@ -409,21 +491,48 @@ proc tryProver(info: ProverInfo, goal: string, timeout: int = defaultTimeout,
 // Search strategies
 // ---------------------------------------------------------------------------
 
-// Sequential proof search (baseline) — tries provers one by one
-proc sequentialProofSearch(goal: string, provers: [] ProverInfo,
-                           timeout: int = defaultTimeout): ProofResult {
+// Sequential search — tries provers one by one, recording the full
+// per-prover table for telemetry (#162).
+//
+// `results` and `attempted` are indexed by `provers.domain`, NOT by
+// `ProverInfo.id`, so filtered registries (see `categorySearch`) stay
+// correctly indexed. Provers the strategy never reaches after an early
+// success keep `attempted[i] == false`, which the bench reports as
+// `not_attempted`.
+//
+// All three strategies delegate to a telemetry variant so that what the
+// bench measures and what the bench reports are the same code path.
+proc sequentialProofSearchTelemetry(goal: string, provers: [] ProverInfo,
+                                    ref results: [] ProofResult,
+                                    ref attempted: [] bool,
+                                    timeout: int = defaultTimeout): ProofResult {
     if verbose then
         writeln("Sequential search: trying ", provers.size, " provers one by one...");
 
+    // Pre-seed so every index is readable even if the loop returns early.
+    for i in provers.domain {
+        attempted[i] = false;
+        results[i] = new ProofResult(
+            success = false, prover = provers[i].name, proverId = provers[i].id,
+            time = 0.0, exitCode = -1, output = "Not attempted",
+            category = provers[i].category
+        );
+    }
+
     var totalTimer = new stopwatch();
     totalTimer.start();
 
-    for prover in provers {
+    for i in provers.domain {
+        const prover = provers[i];
+
         if verbose then
             write("  Trying ", prover.name, "...");
 
         var result = tryProver(prover, goal, timeout);
 
+        attempted[i] = true;
+        results[i] = result;
+
         if verbose then
             writeln(if result.success then " ✓ SUCCESS (" + result.time:string + "s)"
                    else " ✗ " + result.output);
@@ -449,9 +558,20 @@ proc sequentialProofSearch(goal: string, provers: [] ProverInfo,
     );
 }
 
-// Parallel proof search — tries ALL provers concurrently via coforall
-proc parallelProofSearch(goal: string, provers: [] ProverInfo,
-                          timeout: int = defaultTimeout): ProofResult {
+// Sequential proof search (baseline) — tries provers one by one
+proc sequentialProofSearch(goal: string, provers: [] ProverInfo,
+                           timeout: int = defaultTimeout): ProofResult {
+    var results: [provers.domain] ProofResult;
+    var attempted: [provers.domain] bool;
+    return sequentialProofSearchTelemetry(goal, provers, results, attempted, timeout);
+}
+
+// Parallel proof search — tries ALL provers concurrently via coforall,
+// recording the full per-prover table for telemetry.
+proc parallelProofSearchTelemetry(goal: string, provers: [] ProverInfo,
+                                  ref results: [] ProofResult,
+                                  ref attempted: [] bool,
+                                  timeout: int = defaultTimeout): ProofResult {
     if verbose then
         writeln("Parallel search: trying all ", provers.size,
                " provers concurrently...");
@@ -459,16 +579,15 @@ proc parallelProofSearch(goal: string, provers: [] ProverInfo,
     var totalTimer = new stopwatch();
     totalTimer.start();
 
-    // Results array — one per prover
-    var results: [provers.domain] ProofResult;
-
-    // Launch all provers in parallel
-    coforall (prover, i) in zip(provers, provers.domain) {
-        results[i] = tryProver(prover, goal, timeout);
+    // Launch all provers in parallel. Each task owns its own index, so
+    // the writes to `results` and `attempted` never race.
+    coforall i in provers.domain {
+        results[i] = tryProver(provers[i], goal, timeout);
+        attempted[i] = true;
 
         if verbose && results[i].success {
             writef("  ✓ %s succeeded in %.2dr seconds (exit %i)\n",
-                   prover.name, results[i].time, results[i].exitCode);
+                   provers[i].name, results[i].time, results[i].exitCode);
         }
     }
 
@@ -506,6 +625,14 @@ proc parallelProofSearch(goal: string, provers: [] ProverInfo,
     }
 }
 
+// Parallel proof search — tries ALL provers concurrently via coforall
+proc parallelProofSearch(goal: string, provers: [] ProverInfo,
+                          timeout: int = defaultTimeout): ProofResult {
+    var results: [provers.domain] ProofResult;
+    var attempted: [provers.domain] bool;
+    return parallelProofSearchTelemetry(goal, provers, results, attempted, timeout);
+}
+
 // L2.2 speculative search — race all provers, return the first success.
 //
 // Semantics vs `parallelProofSearch` (best-of):
@@ -531,8 +658,13 @@ proc parallelProofSearch(goal: string, provers: [] ProverInfo,
 // the caller because `winner` is set before any cancellation could
 // race the CAS. See proofs/agda/ParallelSoundness.agda:
 // `cancellation-safety` for the formal statement.
-proc parallelProofSearchSpeculative(goal: string, provers: [] ProverInfo,
-                                    timeout: int = defaultTimeout): ProofResult {
+//
+// Telemetry: losers that self-SIGKILLed land in `results` with
+// exitCode = -5, which `classifyOutcome` maps to `preempted`.
+proc parallelProofSearchSpeculativeTelemetry(goal: string, provers: [] ProverInfo,
+                                             ref results: [] ProofResult,
+                                             ref attempted: [] bool,
+                                             timeout: int = defaultTimeout): ProofResult {
     if verbose then
         writeln("Speculative search: ", provers.size,
                 " provers racing, first-success-wins");
@@ -540,13 +672,13 @@ proc parallelProofSearchSpeculative(goal: string, provers: [] ProverInfo,
     var totalTimer = new stopwatch();
     totalTimer.start();
 
-    var results: [provers.domain] ProofResult;
     var winnerIdx: atomic int;
     winnerIdx.write(-1);
     var cancelToken = new owned CancelToken();
 
-    coforall (prover, i) in zip(provers, provers.domain) {
-        results[i] = tryProver(prover, goal, timeout, cancelToken.borrow());
+    coforall i in provers.domain {
+        results[i] = tryProver(provers[i], goal, timeout, cancelToken.borrow());
+        attempted[i] = true;
 
         if results[i].success {
             // Monotone first-wins CAS: only the first successful
@@ -578,6 +710,14 @@ proc parallelProofSearchSpeculative(goal: string, provers: [] ProverInfo,
     );
 }
 
+// L2.2 speculative search — race all provers, return the first success.
+proc parallelProofSearchSpeculative(goal: string, provers: [] ProverInfo,
+                                    timeout: int = defaultTimeout): ProofResult {
+    var results: [provers.domain] ProofResult;
+    var attempted: [provers.domain] bool;
+    return parallelProofSearchSpeculativeTelemetry(goal, provers, results, attempted, timeout);
+}
+
 // Category-filtered parallel search — only try provers from a specific category
 proc categorySearch(goal: string, provers: [] ProverInfo,
                      category: ProverCategory,

From 128fc53ccab03cd27a3383fac0ce77664f637f58 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 25 Sep 2026 14:39:12 +0000
Subject: [PATCH 2/2] fix(docs): reconcile prover counts to the canonical
 source (#251)

Implements #251, with one correction to the premise: the canonical file is
docs/PROVER_COUNT.adoc, which has never existed as a .md in this checkout
(no rename history either -- the tree is one squashed commit). "128"
appears in ten live or recorded places, "113" in the machine-readable
catalogue, and the repository description still advertises 30.

Verified against the tree, not against each other:
  V  ProverKind variants in src/rust/provers/mod.rs  141
  F  backend implementation files                     105
  S  impls exposing suggest_tactics                   102
  D  variants carrying a type-checker role             46
  C  ProverKind::all_core() / default REST surface      12

Live surfaces corrected (they claimed 128 or 30 as today's figure):
  docs/ARCHITECTURE.adoc      -- diagram + tier overview; the Tier 1 list
                                 also named F*/Idris2/Alt-Ergo/Dafny/
                                 Vampire/E-Prover, none of which are in
                                 all_core(); replaced with the actual set
  docs/ROADMAP.adoc           -- endpoint-target row now cites canonical
                                 instead of restating denominators
  docs/architecture/VERISIM-ER-SCHEMA.adoc
  docs-site/content/api/graphql.adoc
  docs/ECOSYSTEM-INTEGRATION.adoc
  docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc
  docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc ("all 12" -> "all Tier 1 (core)")

Live gates de-numbered so they cannot drift again (the canonical file's
own advice: cite it, do not restate a number):
  docs/maintenance/MAINTENANCE-CHECKLIST.adoc
  .machine_readable/policies/MAINTENANCE-AXES.a2ml

.machine_readable/provers.a2ml was 28 variants behind: 113 sections against
a 141-variant enum, a strict subset with no extras, i.e. plainly stale
rather than divergent. Regenerated with the repository's own
scripts/gen-provers-a2ml.sh, so the slugs come from the same sed pipeline:
141 sections, parses as TOML, and all 113 pre-existing entries are byte
identical (diff is 86 insertions / 2 deletions). Its documented consumer,
backend-matrix.yml, no longer exists in .github/workflows/ and nothing else
reads the file, so this has no CI side effects -- recorded as a finding
rather than silently fixed.

scripts/gen-provers-a2ml.sh emitted a frozen date = "2026-04-24"; the date
is now evaluated at run time (outside the quoted heredoc, which must stay
quoted because the comment block contains backticks). Not changed: the
template's AGPL-3.0-or-later header against the committed file's MPL-2.0
header -- the root LICENSE is AGPL, so which line is right is a licensing
call, and a regeneration must not silently flip it.

docs/PROVER_COUNT.adoc gains a "Surface reconciliation" section: every
surface that states a count, what it said, and whether it was corrected,
de-numbered, or deliberately left as a point-in-time record (release
notes, dated audits, handover snapshots, campaign logs, STATE.a2ml), with
the re-check command.

Refs #251

Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
---
 .../policies/MAINTENANCE-AXES.a2ml            |   2 +-
 .machine_readable/provers.a2ml                |  88 ++++++++++-
 docs-site/content/api/graphql.adoc            |   4 +-
 docs/ARCHITECTURE.adoc                        |  27 ++--
 docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc       |   2 +-
 docs/ECOSYSTEM-INTEGRATION.adoc               |   2 +-
 docs/PROVER_COUNT.adoc                        | 148 ++++++++++++++++++
 docs/ROADMAP.adoc                             |  14 +-
 docs/architecture/VERISIM-ER-SCHEMA.adoc      |   3 +-
 docs/maintenance/MAINTENANCE-CHECKLIST.adoc   |   3 +-
 .../SOFTWARE-DEVELOPMENT-APPROACH.adoc        |   3 +-
 scripts/gen-provers-a2ml.sh                   |  15 +-
 12 files changed, 282 insertions(+), 29 deletions(-)

diff --git a/.machine_readable/policies/MAINTENANCE-AXES.a2ml b/.machine_readable/policies/MAINTENANCE-AXES.a2ml
index 1589ab77..2fd07817 100644
--- a/.machine_readable/policies/MAINTENANCE-AXES.a2ml
+++ b/.machine_readable/policies/MAINTENANCE-AXES.a2ml
@@ -20,7 +20,7 @@ sources = ["README.adoc", "ROADMAP.adoc", "docs/maintenance/MAINTENANCE-CHECKLIS
 
 [axes.axis-1.must]
 items = [
-  "30 prover backends compile and pass smoke tests",
+  "All prover backends compile and pass smoke tests (figure: docs/PROVER_COUNT.adoc)",
   "cargo test --lib passes with zero failures",
   "No believe-me or assert_total in Idris2 source",
   "No unsafe blocks without SAFETY comments",
diff --git a/.machine_readable/provers.a2ml b/.machine_readable/provers.a2ml
index 30abeb4a..dc27c06f 100644
--- a/.machine_readable/provers.a2ml
+++ b/.machine_readable/provers.a2ml
@@ -19,8 +19,8 @@
 [metadata]
 version = "1.0.0"
 source  = "src/rust/provers/mod.rs::ProverKind"
-date    = "2026-04-24"
-count   = 113
+date    = "2026-09-25"
+count   = 141
 
 [prover.ABC]
 slug = "abc"
@@ -40,12 +40,18 @@ slug = "affine_type_checker"
 [prover.Agda]
 slug = "agda"
 
+[prover.AgsyHOL]
+slug = "agsy_hol"
+
 [prover.Alloy]
 slug = "alloy"
 
 [prover.AltErgo]
 slug = "alt_ergo"
 
+[prover.AProVE]
+slug = "a_pro_ve"
+
 [prover.Arend]
 slug = "arend"
 
@@ -82,6 +88,12 @@ slug = "coeffect_type_checker"
 [prover.Coq]
 slug = "coq"
 
+[prover.CryptoVerif]
+slug = "crypto_verif"
+
+[prover.CSI]
+slug = "csi"
+
 [prover.CubicalAgda]
 slug = "cubical_agda"
 
@@ -106,12 +118,18 @@ slug = "d_real"
 [prover.DyadicTypeChecker]
 slug = "dyadic_type_checker"
 
+[prover.EasyCrypt]
+slug = "easy_crypt"
+
 [prover.EchoTypeChecker]
 slug = "echo_type_checker"
 
 [prover.EffectRowTypeChecker]
 slug = "effect_row_type_checker"
 
+[prover.ELK]
+slug = "elk"
+
 [prover.EpistemicTypeChecker]
 slug = "epistemic_type_checker"
 
@@ -121,6 +139,9 @@ slug = "e_prover"
 [prover.ExistentialTypeChecker]
 slug = "existential_type_checker"
 
+[prover.Faial]
+slug = "faial"
+
 [prover.FramaC]
 slug = "frama_c"
 
@@ -130,6 +151,12 @@ slug = "f_star"
 [prover.GLPK]
 slug = "glpk"
 
+[prover.GNATprove]
+slug = "gna_tprove"
+
+[prover.GPUVerify]
+slug = "gpu_verify"
+
 [prover.GradualTypeChecker]
 slug = "gradual_type_checker"
 
@@ -151,6 +178,9 @@ slug = "homotopy_type_checker"
 [prover.Idris2]
 slug = "idris2"
 
+[prover.IleanCoP]
+slug = "ilean_co_p"
+
 [prover.Imandra]
 slug = "imandra"
 
@@ -166,6 +196,9 @@ slug = "indexed_type_checker"
 [prover.IntersectionTypeChecker]
 slug = "intersection_type_checker"
 
+[prover.IProver]
+slug = "i_prover"
+
 [prover.Isabelle]
 slug = "isabelle"
 
@@ -178,21 +211,36 @@ slug = "katagoria_verifier"
 [prover.KeY]
 slug = "ke_y"
 
+[prover.KeYmaeraX]
+slug = "ke_ymaera_x"
+
 [prover.Kissat]
 slug = "kissat"
 
+[prover.Konclude]
+slug = "konclude"
+
 [prover.LambdaProlog]
 slug = "lambda_prolog"
 
+[prover.Lash]
+slug = "lash"
+
 [prover.Lean]
 slug = "lean"
 
 [prover.Lean3]
 slug = "lean3"
 
+[prover.Leo3]
+slug = "leo3"
+
 [prover.LinearTypeChecker]
 slug = "linear_type_checker"
 
+[prover.LiquidHaskell]
+slug = "liquid_haskell"
+
 [prover.Matita]
 slug = "matita"
 
@@ -202,6 +250,12 @@ slug = "mercury"
 [prover.Metamath]
 slug = "metamath"
 
+[prover.MetiTarski]
+slug = "meti_tarski"
+
+[prover.MetTeL2]
+slug = "met_te_l2"
+
 [prover.MiniSat]
 slug = "mini_sat"
 
@@ -217,9 +271,15 @@ slug = "mizar"
 [prover.MizAR]
 slug = "miz_ar"
 
+[prover.MleanCoP]
+slug = "mlean_co_p"
+
 [prover.ModalTypeChecker]
 slug = "modal_type_checker"
 
+[prover.NanoCoP]
+slug = "nano_co_p"
+
 [prover.Naproche]
 slug = "naproche"
 
@@ -256,9 +316,15 @@ slug = "phantom_type_checker"
 [prover.PolymorphicTypeChecker]
 slug = "polymorphic_type_checker"
 
+[prover.Princess]
+slug = "princess"
+
 [prover.Prism]
 slug = "prism"
 
+[prover.ProB]
+slug = "pro_b"
+
 [prover.ProbabilisticTypeChecker]
 slug = "probabilistic_type_checker"
 
@@ -274,9 +340,15 @@ slug = "pro_verif"
 [prover.PVS]
 slug = "pvs"
 
+[prover.Qepcad]
+slug = "qepcad"
+
 [prover.QTTTypeChecker]
 slug = "qtt_type_checker"
 
+[prover.Redlog]
+slug = "redlog"
+
 [prover.RefinementTypeChecker]
 slug = "refinement_type_checker"
 
@@ -289,6 +361,9 @@ slug = "rocq"
 [prover.RowTypeChecker]
 slug = "row_type_checker"
 
+[prover.Satallax]
+slug = "satallax"
+
 [prover.SCIP]
 slug = "scip"
 
@@ -307,6 +382,12 @@ slug = "spass"
 [prover.SPIN]
 slug = "spin"
 
+[prover.Stainless]
+slug = "stainless"
+
+[prover.Storm]
+slug = "storm"
+
 [prover.SubtypingTypeChecker]
 slug = "subtyping_type_checker"
 
@@ -325,6 +406,9 @@ slug = "tlc"
 [prover.TropicalTypeChecker]
 slug = "tropical_type_checker"
 
+[prover.Twee]
+slug = "twee"
+
 [prover.Twelf]
 slug = "twelf"
 
diff --git a/docs-site/content/api/graphql.adoc b/docs-site/content/api/graphql.adoc
index 6bbac58c..fd636f05 100644
--- a/docs-site/content/api/graphql.adoc
+++ b/docs-site/content/api/graphql.adoc
@@ -21,7 +21,9 @@ query {
 }
 ----
 
-Returns all 30 prover backends.
+Returns all registered prover backends — 141 `+ProverKind+` variants over
+105 backend implementations. See `+docs/PROVER_COUNT.adoc+` (canonical) for
+the tier split and reproduction commands.
 
 ===== Get Proof State
 
diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc
index e7d3d81e..58afe77c 100644
--- a/docs/ARCHITECTURE.adoc
+++ b/docs/ARCHITECTURE.adoc
@@ -43,14 +43,14 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 │              └──┬───────────────────────────────┬───┘                   │
 │                 │                               │                        │
 │   ┌─────────────▼────────────┐    ┌─────────────▼───────────────────┐   │
-│   │   Trust pipeline          │    │  128 ProverKind backends         │  │
-│   │   (verification/)         │    │  (provers/)                      │  │
-│   │   - integrity             │    │   89 external prover bindings    │  │
-│   │   - portfolio             │    │   39 TypeChecker disciplines     │  │
-│   │   - certificates          │    │      via TypedWasm Sigma         │  │
+│   │   Trust pipeline          │    │  141 ProverKind variants         │  │
+│   │   (verification/)         │    │  105 backend impl files          │  │
+│   │   - integrity             │    │  (provers/)                      │  │
+│   │   - portfolio             │    │  see docs/PROVER_COUNT.adoc      │  │
+│   │   - certificates          │    │                                  │  │
 │   │   - axiom tracker         │    │                                  │  │
-│   │   - confidence            │    │   Tier 1: 12 core (REST default) │  │
-│   │   - mutation              │    │   Tier 2–10: by capability       │  │
+│   │   - confidence            │    │  Tier 1: 12 core (REST default)  │  │
+│   │   - mutation              │    │  Tier 2–10: by capability        │  │
 │   │   - pareto                │    └──────────────────────────────────┘  │
 │   │   - statistics            │                                          │
 │   └───────────────────────────┘                                          │
@@ -80,13 +80,14 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 
 === Tier overview
 
-ECHIDNA carries *128 ProverKind variants*. The exposed surface depends
-on tier:
+ECHIDNA carries *141 `+ProverKind+` variants* across *105 backend
+implementation files*. The exposed surface depends on tier:
 
-* *Tier 1 (12 core)* — the default REST `+/api/verify+` surface:
-Coq/Rocq, Lean 4, Agda, Isabelle/HOL, Idris 2, F*, Z3, CVC5, Alt-Ergo,
-Dafny, Vampire, E Prover.
-* *Tier 2–10* — 116 additional backends: ATPs, SMT, model checkers,
+* *Tier 1 (12 core)* — the default REST `+/api/verify+` surface, and
+exactly the set returned by `+ProverKind::all_core()+`: Coq, Lean 4,
+Agda, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2,
+HOL4.
+* *Tier 2–10* — the remaining variants: ATPs, SMT, model checkers,
 constraint solvers, niche provers, ecosystem type-checkers. Available
 via explicit `+ProverKind+` selection in CLI / REPL / GraphQL but not
 auto-routed.
diff --git a/docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc b/docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc
index 1c9ec884..60a6e10d 100644
--- a/docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc
+++ b/docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc
@@ -250,7 +250,7 @@ file)
 * Uses `+crate::core::Term+` for theorem representation
 * Integrates with `+Theorem+` struct (has `+aspects: Vec<String>+`
 field)
-* Compatible with all 12 prover backends
+* Compatible with all Tier 1 (core) prover backends
 * Works with `+ProofState+` and `+Context+`
 
 ==== With Neural Components (Julia)
diff --git a/docs/ECOSYSTEM-INTEGRATION.adoc b/docs/ECOSYSTEM-INTEGRATION.adoc
index 3a6dcc3c..80eefd23 100644
--- a/docs/ECOSYSTEM-INTEGRATION.adoc
+++ b/docs/ECOSYSTEM-INTEGRATION.adoc
@@ -141,7 +141,7 @@ Needs entry in `+repos+` section of farm-manifest.json
 [source,json]
 ----
 "echidna": {
-  "description": "Neurosymbolic theorem proving platform with 30 prover backends",
+  "description": "Neurosymbolic theorem proving platform with 141 ProverKind variants over 105 backend implementations",
   "forges": ["github", "gitlab", "sourcehut", "codeberg", "bitbucket"],
   "priority": "high",
   "auto_propagate": true,
diff --git a/docs/PROVER_COUNT.adoc b/docs/PROVER_COUNT.adoc
index a36aab39..647e7693 100644
--- a/docs/PROVER_COUNT.adoc
+++ b/docs/PROVER_COUNT.adoc
@@ -154,6 +154,154 @@ document set listed in that file — `+docs/+`, `+.machine_readable/+` and
 `+crates/*/README.md+` are *not* covered, which is where the surviving
 drift accumulated.
 
+=== Surface reconciliation (issue #251)
+
+Drift accumulated because the `+R5a+` guard covers only the top-level
+document set; `+docs/+`, `+.machine_readable/+` and `+crates/*+` sit
+outside it. This table records, surface by surface, what each one said
+and how it is being handled. Three dispositions are in use:
+
+* *corrected* — a live claim that was simply wrong; it now states the
+canonical figure.
+* *de-numbered* — a live gate or checklist; the bare number was removed
+and replaced with a pointer here, so the gate can no longer drift.
+* *record* — a point-in-time document (release note, dated audit,
+handover snapshot, campaign log); left at its authoring-time figure on
+purpose, per the policy above.
+
+[width="100%",cols="46%,20%,34%",options="header",]
+|===
+|Surface |Said |Disposition
+
+|`+docs/ARCHITECTURE.adoc+` (diagram + tier overview)
+|128 variants; 89 external + 39 TypeChecker; Tier 1 = Coq, Lean, Agda,
+Isabelle, Idris2, F*, Z3, CVC5, Alt-Ergo, Dafny, Vampire, E Prover
+|*corrected* — 141 variants over 105 impl files; Tier 1 restated to the
+exact `+ProverKind::all_core()+` set
+
+|`+docs/ROADMAP.adoc+` (endpoint-target table)
+|128 variants; 89 external + 39 TypeChecker; 91/91 `+suggest_tactics+`;
+72 with Verisim fallback
+|*corrected* — 141/105, 46 discipline, 102 `+suggest_tactics+`; cites
+this file instead of restating denominators
+
+|`+docs/architecture/VERISIM-ER-SCHEMA.adoc+`
+|"`which of the 128 backends`"
+|*corrected* — 141 variants, cites this file
+
+|`+docs-site/content/api/graphql.adoc+`
+|"`Returns all 30 prover backends`"
+|*corrected* — 141 variants over 105 impl files, cites this file
+
+|`+docs/ECOSYSTEM-INTEGRATION.adoc+` (forge-registry JSON sample)
+|"`...with 30 prover backends`"
+|*corrected* — 141 variants over 105 impl files
+
+|`+docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc+`
+|"`Core | Rust | 30 prover backends`"
+|*corrected* — 141/105, cites this file
+
+|`+docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc+`
+|"`Compatible with all 12 prover backends`"
+|*corrected* — "`all Tier 1 (core) prover backends`"
+
+|`+docs/maintenance/MAINTENANCE-CHECKLIST.adoc+` and
+`+.machine_readable/policies/MAINTENANCE-AXES.a2ml+`
+|"`All 30 prover backends compile and pass smoke tests`"
+|*de-numbered* — "`All prover backends compile and pass smoke tests`",
+pointer to this file
+
+|`+docs/releases/RELEASE_NOTES_v1.2.adoc+`, `+v1.3.adoc+`
+|12 provers (release-time)
+|*record*
+
+|`+docs/reports/audit/2026-03-31-echidna-audit.adoc+`
+|30 provers (audit-time)
+|*record*
+
+|`+CHANGELOG.adoc+`
+|30 (early entries), 105 (later entry)
+|*record* — each entry describes its release, not `+main+` today
+
+|`+docs/decisions/2026-06-01-saturation-campaign.adoc+`
+|"`had reached 128 ProverKind variants`"
+|*record* — the campaign's starting state
+
+|`+docs/TEST-NEEDS.adoc+`
+|48 backends (CRG B snapshot, 2026-04-04)
+|*record* — dated achievement checklist
+
+|`+docs/handover/+` (`+STATE+`, `+PRODUCTION-WIRING-PLAN+`, `+TODO+`,
+`+llm-warmup-*+`)
+|12 / 30 / 48 in past-state narrative
+|*record* — handover snapshots of what was true then
+
+|`+docs/design/+`, `+docs/academic/+`, `+docs/governance/+`,
+`+docs/isabelle-backend.adoc+`, `+docs/METAMATH_BACKEND.adoc+`
+|12 / 48 / "`48+`" in design-time prose
+|*record* — design/positioning documents of their period
+
+|`+src/chapel/RESULTS.adoc+`
+|9/12 provers succeeded (lab run)
+|*record* — benchmark output
+
+|`+audits/+` (`+assail-classifications.a2ml+`,
+`+audit-ffi-boundary.adoc+`)
+|105 backends / 30 at audit time
+|*record* — audit artefacts
+
+|`+.machine_readable/descriptiles/STATE.a2ml+`
+|113, 128, 48 at various points
+|*record* — session-state ledger (one snapshot even records that it
+disagreed with the enum at the time)
+
+|`+.machine_readable/provers.a2ml+`
+|`+count = 113+` (date 2026-04-24), i.e. 28 variants behind the enum
+|*corrected* — regenerated from `+ProverKind+` with
+`+scripts/gen-provers-a2ml.sh+`: 141 sections, validated as TOML; the 113
+pre-existing entries are byte-identical
+|===
+
+Live surfaces still carrying an unlabelled figure, deferred as explicit
+follow-ups rather than guessed at:
+
+* `+crates/echidna-mcp/src/main.rs+` — six "`105 prover backends`"
+occurrences in MCP tool descriptions (runtime-visible). 105 is the
+correct *implementation-file* denominator, but the label is wrong; it
+should read "`105 backend implementations`" or cite this file.
+* `+src/rust/+` doc comments (`+groove.rs+`, `+learning/mod.rs+`,
+`+llm.rs+`, `+proof_search.rs+`, `+server.rs+`, `+dispatch.rs+`) — 30/48.
+* `+tests/+` (`+aspect_tests.rs+`, `+e2e_prover_test.rs+`,
+`+integration_v1_2.rs+`, `+neural_property_tests.rs+`, `+smoke_e2e.rs+`)
+— stale counts in comments; the assertions themselves are lower bounds
+and still pass.
+* `+.machine_readable/{ROADMAP.a2ml,descriptiles/{AGENTIC,ECOSYSTEM,NEUROSYM}.a2ml}+`
+— 105/141 figures that are correct but unlabelled.
+* Repository GitHub description ("`30 prover backends`") — an
+owner-level settings write, not something a repository commit can fix.
+* `+docs/LEARNING-ARCHITECTURE.adoc+` — "`48-prover dispatch layer`" in a
+live architectural explanation; the denominator needs a decision, not a
+guess.
+* `+.machine_readable/provers.a2ml+`'s documented consumer is gone: it
+says `+backend-matrix.yml+` reads it to build "`one job per prover`", but
+no such workflow exists in `+.github/workflows/+` and nothing else reads
+the file. The per-prover matrix CI the file was built for is therefore
+absent, not merely stale.
+* `+scripts/gen-provers-a2ml.sh+`'s header template declares
+`+AGPL-3.0-or-later+` (matching the root `+LICENSE+`) while the committed
+`+provers.a2ml+` declares `+MPL-2.0+`. Left as-is: which one is correct is
+a licensing decision (see the SPDX/licensing issue), and a regeneration
+must not silently flip a licence line.
+
+Re-check by re-running the sweep:
+
+[source,bash]
+----
+grep -rnE '(^|[^0-9])(12|30|48|74|105|113|128|141)[^0-9]{0,3}(prover|backend|ProverKind)' \
+  --include='*.adoc' --include='*.md' --include='*.a2ml' --include='*.rs' . \
+  | grep -v '^\./\.git'
+----
+
 === Verifying locally
 
 Each command is the definition of its figure. Run from the repository
diff --git a/docs/ROADMAP.adoc b/docs/ROADMAP.adoc
index 8191d781..ceedba65 100644
--- a/docs/ROADMAP.adoc
+++ b/docs/ROADMAP.adoc
@@ -131,12 +131,14 @@ Stage 8  Self‑verified                      ECHIDNA proves ECHIDNA
 [width="100%",cols="34%,33%,33%",options="header",]
 |===
 |Claim |Today |End‑state target
-|"`Every important solver`" |*128 ProverKind variants* (89 external
-prover bindings + 39 TypeChecker disciplines routed through TypedWasm);
-*91 / 91 with real `+suggest_tactics+`* (5 still heuristic-only;
-GNN-ranked is the end-state target per `+docs/PROVER_COUNT.adoc+`); *72
-backends with empty native search but a cross-prover Verisim fallback at
-the dispatcher layer (CLI/REST/REPL)* |*All variants with real
+|"`Every important solver`" |*141 `+ProverKind+` variants* over *105
+backend implementation files*, of which *46* carry a type-checker /
+discipline role and *102* expose real `+suggest_tactics+` (the rest
+heuristic-only; GNN-ranked is the end-state target); some backends have
+empty native search but a cross-prover Verisim fallback at the
+dispatcher layer (CLI/REST/REPL). Denominators, tier split and the
+commands that reproduce each figure: `+docs/PROVER_COUNT.adoc+`
+(canonical) |*All variants with real
 `+suggest_tactics+` (GNN‑ranked top‑k); per-backend search reflects each
 prover’s native capability while cross-prover queries are served from
 Verisim by `+goal_hash+`*
diff --git a/docs/architecture/VERISIM-ER-SCHEMA.adoc b/docs/architecture/VERISIM-ER-SCHEMA.adoc
index 881e46ac..191d0acd 100644
--- a/docs/architecture/VERISIM-ER-SCHEMA.adoc
+++ b/docs/architecture/VERISIM-ER-SCHEMA.adoc
@@ -223,7 +223,8 @@ A single invocation of a prover backend against a goal.
 
 |`+octad_key+` (FK→E1) |`+UUIDv7+` |the goal
 
-|`+prover+` |enum `+ProverKind+` |which of the 128 backends
+|`+prover+` |enum `+ProverKind+` |which of the 141 `+ProverKind+`
+variants (see `+docs/PROVER_COUNT.adoc+`, canonical)
 
 |`+verdict+` |enum
 `+Proven+`/`+Refuted+`/`+Timeout+`/`+Unknown+`/`+Error+` |outcome
diff --git a/docs/maintenance/MAINTENANCE-CHECKLIST.adoc b/docs/maintenance/MAINTENANCE-CHECKLIST.adoc
index 09a43d24..a34c397b 100644
--- a/docs/maintenance/MAINTENANCE-CHECKLIST.adoc
+++ b/docs/maintenance/MAINTENANCE-CHECKLIST.adoc
@@ -7,7 +7,8 @@
 
 === Must
 
-* [ ] All 30 prover backends compile and pass smoke tests
+* [ ] All prover backends compile and pass smoke tests (current figure and
+denominator: `+docs/PROVER_COUNT.adoc+`)
 * [ ] `cargo test --lib` passes with zero failures
 * [ ] No `believe_me` or `assert_total` in Idris2 source
 * [ ] No `unsafe` blocks without `// SAFETY:` comments
diff --git a/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc b/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc
index 4ce3118e..8de6521e 100644
--- a/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc
+++ b/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc
@@ -14,7 +14,8 @@ RSR (Rhodium Standard Repository) practices with formal verification emphasis.
 |===
 | Layer | Language | Purpose
 
-| Core | Rust | 30 prover backends, dispatch pipeline, trust pipeline
+| Core | Rust | 141 `+ProverKind+` variants over 105 backend implementations
+(see `+docs/PROVER_COUNT.adoc+`), dispatch pipeline, trust pipeline
 | ML | Julia | Neural tactic prediction, premise selection, anomaly detection
 | Parallel | Chapel | HPC distributed proof search
 | ABI | Idris2 | Formal interface definitions with dependent types
diff --git a/scripts/gen-provers-a2ml.sh b/scripts/gen-provers-a2ml.sh
index 87389e4d..ba2523c0 100755
--- a/scripts/gen-provers-a2ml.sh
+++ b/scripts/gen-provers-a2ml.sh
@@ -4,6 +4,16 @@
 #
 # Usage: gen-provers-a2ml.sh <variant-list-file>
 #
+# Pass the variants case-insensitively sorted to match the committed
+# layout (.machine_readable/provers.a2ml) and keep diffs minimal.
+# Case-only ties are not resolved by the sort: list `Mizar` before
+# `MizAR`, as the committed file does.
+#
+# NOTE: the header template below declares AGPL-3.0-or-later (matching the
+# root LICENSE) while the committed .machine_readable/provers.a2ml declares
+# MPL-2.0. That discrepancy is a licensing call, tracked separately -- do
+# not let a regeneration silently change the file's SPDX line.
+#
 # The variant-list path is a CLI argument (was the hard-coded
 # /tmp/provers-list.txt); predictable /tmp/* paths are a panic-attack
 # low (path-traversal / TOCTOU on multi-user runners). Callers should
@@ -39,9 +49,12 @@ cat << 'HEADER'
 [metadata]
 version = "1.0.0"
 source  = "src/rust/provers/mod.rs::ProverKind"
-date    = "2026-04-24"
 HEADER
 
+# Emitted outside the quoted heredoc so it is evaluated at run time rather
+# than frozen at authoring time. The comment block above contains backticks,
+# so the heredoc itself must stay quoted (no command substitution).
+printf 'date    = "%s"\n' "$(date -u +%F)"
 printf "count   = %d\n\n" "$(wc -l < "$VARIANT_LIST")"
 
 while IFS= read -r variant; do