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/.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/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-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/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/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
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,