diff --git a/CLAUDE.md b/CLAUDE.md
index 9a6373b3..db49b580 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -140,7 +140,7 @@ Shape, by area:
 - **Idris2 ABI**: `EchidnaABI.TacticRecord` (fixed-point confidence, total-order proofs, in-range round-trip lemmas) + sibling modules; type-checked on every push by `idris2-abi-ci.yml`.
 - **GNN integration**: graph construction (7 node kinds, 8 edge kinds), 32-dim local term embeddings, GNN inference client, hybrid GNN + symbolic scoring, Julia `/gnn/rank` with cosine fallback.
 - **Corpus identity**: `src/rust/corpus/canonical.rs` hashes a declaration's canonical type shape (`dk-shape-v1`) so the same theorem matches across provers without a synonym table — tier 1 keeps binders and sorts, tier 2 (`skeleton`) erases them for Isabelle/Why3. The Vector octad defaults to a 256-dim structural n-gram embedder (`echidna-corpus-structural-v2`); the 32-dim `HashEmbedder` is legacy/GNN-parity only. See `docs/CORPUS.adoc`.
-- **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` formalises soundness, completeness, and cancellation-safety with zero postulate / admit / believe_me. L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.adoc`](docs/handover/TODO.adoc).
+- **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` models the speculative CAS + cancel-token protocol over every interleaving and proves the winner is stable, really succeeded and is the first successful prover to reach the CAS, that preempted losers are inert and that a success always yields a winner (zero postulate / admit / believe_me; assumes sequentially consistent atomics). L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.adoc`](docs/handover/TODO.adoc).
 - **Wave-3 container infrastructure**: per-prover images in `.containerization/Containerfile.wave3`; weekly cron in `container-ci.yml` runs stub-sentinel detection across all 8 Tier-3 cells.
 - **Julia ML layer**: logistic-regression tactic prediction shipped; Flux.jl scaffolds for GNN/Transformer training present but not yet trained on real data — corpus ready under `training_data/`.
 - **Migrations in flight**: AffineScript → AffineScript-TEA (UI); npm → Bun (`echidna-playground`); CI workflow consolidation under the governance ruleset.
diff --git a/Cargo.lock b/Cargo.lock
index 0bf91e23..0592b0e7 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -133,7 +133,7 @@ version = "1.1.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc"
 dependencies = [
- "windows-sys 0.60.2",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -144,7 +144,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d"
 dependencies = [
  "anstyle",
  "once_cell_polyfill",
- "windows-sys 0.60.2",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -640,7 +640,7 @@ version = "3.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34"
 dependencies = [
- "windows-sys 0.52.0",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -1246,7 +1246,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb"
 dependencies = [
  "libc",
- "windows-sys 0.52.0",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -2093,7 +2093,7 @@ version = "0.50.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5"
 dependencies = [
- "windows-sys 0.60.2",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -2837,20 +2837,22 @@ dependencies = [
 
 [[package]]
 name = "rmcp"
-version = "3.5.0"
+version = "3.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fae7019994ae0fe4ada40b732f798f3ff26f0f04facb1477f1bf37eb4f18a2d3"
+checksum = "d24a7e92f4bcaa36b97fa93c4fa7ca8f3e669eced949345b3462dba333c7f909"
 dependencies = [
  "base64 0.23.1",
  "chrono",
  "futures",
  "indexmap",
+ "libc",
  "pastey",
  "pin-project-lite",
  "rmcp-macros",
  "schemars",
  "serde",
  "serde_json",
+ "sha2 0.11.0",
  "thiserror",
  "tokio",
  "tokio-util",
@@ -2860,9 +2862,9 @@ dependencies = [
 
 [[package]]
 name = "rmcp-macros"
-version = "3.5.0"
+version = "3.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c7e66877136e969d5a2d561ee5841b17717a0619aebd64abb47a2a2f46e34683"
+checksum = "b3140f24a766f80f9ec1607bde85680959a69b83d46fa9ce87dadab7e67ab029"
 dependencies = [
  "darling 0.24.0",
  "proc-macro2",
@@ -2910,7 +2912,7 @@ dependencies = [
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys 0.52.0",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -3251,7 +3253,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "52d1cfed4120b4d927bf7c0f86d2087a4a7d6027c906d9f9d525a80573b9be51"
 dependencies = [
  "libc",
- "windows-sys 0.60.2",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -3391,10 +3393,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd"
 dependencies = [
  "fastrand",
- "getrandom 0.4.2",
+ "getrandom 0.3.4",
  "once_cell",
  "rustix",
- "windows-sys 0.52.0",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -4198,7 +4200,7 @@ version = "0.1.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22"
 dependencies = [
- "windows-sys 0.52.0",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
diff --git a/docs/bench/README.adoc b/docs/bench/README.adoc
index 0ac474e1..92709801 100644
--- a/docs/bench/README.adoc
+++ b/docs/bench/README.adoc
@@ -125,5 +125,6 @@ is currently measured anywhere.
 
 * `+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.
+* `+proofs/agda/ParallelSoundness.agda+` — race-protocol model:
+  `+winner-stable+`, `+preempted-inert+`, `+cancel-after-win+`.
 * `+docs/handover/TODO.adoc+` — real-corpus speedup bench (#161).
diff --git a/docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc b/docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc
index c5362eee..eb7fe482 100644
--- a/docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc
+++ b/docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc
@@ -86,6 +86,20 @@ verdict over the whole result vector is unaffected by this difference.
 The Agda module’s header docstring is updated in this PR to spell out
 the L2.3 cross-reference.
 
+[NOTE]
+====
+*Superseded 2026-11-09.* The `+cancellation-safety _ = tt+` lemma quoted
+above held by definition (`+true ∨ x = true+`), covered only index 0 and did
+not model the CAS, the token or any interleaving, so it did not establish
+the claim made for it. `+proofs/agda/ParallelSoundness.agda+` now has a
+layer B: a small-step model of this procedure, run over every interleaving
+of `+done i+` and the cancel write. It proves `+winner-stable+`,
+`+preempted-inert+`, `+cancel-after-win+`, `+race-sound+`, `+race-complete+`,
+`+winner-is-first+` and `+race-agrees+`, assuming that Chapel's atomics are
+sequentially consistent. The paragraphs above are kept as the record of
+the original decision.
+====
+
 The CAS itself is the linearisation point: any prover whose poll
 observes `+cancelled = true+` ran AFTER the winning CAS. The
 happens-before edge from `+winnerIdx.compareAndSwap(-1, i)+` →
diff --git a/proofs/agda/ParallelSoundness.agda b/proofs/agda/ParallelSoundness.agda
index 8fdf19b9..e81a7bae 100644
--- a/proofs/agda/ParallelSoundness.agda
+++ b/proofs/agda/ParallelSoundness.agda
@@ -1,64 +1,77 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- ParallelSoundness.agda — Speculative parallel proof-search soundness.
 --
--- Models the Chapel `parallelProofSearchSpeculative` function
--- (src/chapel/parallel_proof_search.chpl) as a pure first-success-wins
--- fold over a vector of single-prover outcomes, and proves three
--- semantic invariants of the aggregation:
+-- Two layers.
 --
---   1.  Soundness                — `speculative xs = true → Any IsTrue xs`
---                                  (no spurious portfolio successes;
---                                   if the verdict is true, at least one
---                                   prover individually said true)
---   2.  Completeness             — `Any IsTrue xs → speculative xs = true`
---                                  (no real success is silently dropped)
---   3.  Cancellation-safety      — once a prover position witnesses
---                                  success, the verdict is true regardless
---                                  of what other provers do (the winner is
---                                  insensitive to the losers' state).
---                                  THIS IS THE L2.3 PREEMPTION CLAIM.
---                                  Once the speculative-search winner has
---                                  flipped the shared `CancelToken`, every
---                                  in-flight loser self-SIGKILLs on its
---                                  next poll and returns a preempted
---                                  result (exitCode = -5). Those preempted
---                                  results are NEVER returned to the
---                                  caller — `winner` was set before any
---                                  cancellation could race the CAS — so
---                                  the aggregation verdict is unchanged.
+-- A.  Aggregation (sections 1–4). `speculative` is the any-true fold over
+--     the provers' outcomes, with soundness and completeness. This layer
+--     says only that boolean OR is correct; it says nothing about
+--     concurrency, and on its own it is NOT a cancellation-safety result.
 --
--- The Chapel implementation uses an atomic compare-and-swap on a
--- shared `winnerIdx` to record the first-completing successful prover.
--- This Agda model captures the same observational semantics — any-true
--- over the result vector — by structural recursion. The CAS protocol
--- is a refinement of this model: it picks ONE successful index out of
--- the (possibly several) provers that succeed, but the aggregation
--- verdict (success or not) is unaffected by which index wins.
+-- B.  Race protocol (sections 5–9). A small-step model of
+--     `parallelProofSearchSpeculativeTelemetry` in
+--     src/chapel/parallel_proof_search.chpl, run over EVERY interleaving
+--     of its events:
 --
--- L2.3 cancel-token implementation lives in `src/chapel/parallel_proof_search.chpl`:
--- the `CancelToken` class (class for shared-by-reference semantics across
--- coforall tasks), the `cancelToken` parameter on `tryProver`, and the
--- `cancelToken.cancelled.write(true)` paired with the CAS in
--- `parallelProofSearchSpeculative`. `cancellation-safety` below is the
--- formal statement of what that implementation preserves.
+--       * `done i`  — prover i reaches its CAS, after its `tryProver` call
+--                     has returned. A prover that observed the cancel token
+--                     before finishing returned a preempted result
+--                     (exitCode = -5, success = false). Otherwise it reports
+--                     its outcome `rs[i]`, and on success it attempts the
+--                     CAS `winnerIdx: -1 → i`. In Chapel the return and the
+--                     CAS are separate statements, so a prover can return
+--                     and be descheduled before its CAS. Nothing it does in
+--                     that gap is visible to the others (`results[i]` and
+--                     `attempted[i]` are its own slots, read only after the
+--                     join), so the event sits at the CAS, the
+--                     linearisation point, and the gap is just a later
+--                     `done i`.
+--       * `signal`  — the CAS winner's `cancelToken.cancelled.write(true)`.
+--                     It is a separate event, so every interleaving of the
+--                     CAS and the cancel write with other provers' finishes
+--                     is covered.
 --
--- Wave-1 scope: this module proves the AGGREGATION layer. The
--- complementary layer — that `tryProver` itself is sound (i.e. its
--- `success = true` return implies the proof actually checks under the
--- existing trust pipeline) — is the responsibility of SoundnessPreservation
--- and the per-prover Idris2 ABI proofs in `src/abi/`, both of which
--- predate this PR. ParallelSoundness composes with them: an aggregation-
--- sound module over a verifier-sound input remains sound at the
--- portfolio level.
+--     Theorems, each for an arbitrary schedule and an arbitrary winner
+--     index (the previous version covered index 0 only, by `tt`):
+--
+--       race-sound          the reported winner really succeeded;
+--       winner-stable       once a winner is set, no later event changes it;
+--       preempted-inert     after cancellation a finishing prover leaves the
+--                           state exactly as it was (exitCode -5 is inert);
+--       cancel-after-win    the token is never set without a winner, so no
+--                           success is preempted before a winner exists;
+--       race-complete       if a successful prover finishes, a winner exists;
+--       winner-is-first     the winner is exactly the first successful
+--                           prover to reach the CAS in schedule order (any
+--                           index). It need not be the first to return from
+--                           `tryProver`: one that returns first and is
+--                           descheduled before its CAS can lose;
+--       race-agrees         on a schedule in which every prover finishes,
+--                           "a winner exists" ⇔ `speculative rs` (layer A).
+--
+-- Assumed boundary (ASSUMED, not proved here):
+--   * Chapel atomics are sequentially consistent (Chapel's default memory
+--     order), so the CAS and the cancel write are linearisable and every
+--     execution corresponds to some schedule `List (Event n)`.
+--   * `tryProver` returns `success = false` whenever it observes the token
+--     (src/chapel/parallel_proof_search.chpl, the exitCode = -5 branch), and
+--     otherwise reports the outcome `rs[i]` modelled here.
+--   * `coforall` joins every task before `winnerIdx.read()`.
+-- Whether `success = true` means the proof really checks is the job of the
+-- per-prover trust pipeline, not of this module.
 
 module ParallelSoundness where
 
-open import Data.Bool  using (Bool; true; false; _∨_)
-open import Data.Nat   using (ℕ; zero; suc)
-open import Data.Vec   using (Vec; []; _∷_)
-open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Bool    using (Bool; true; false; _∨_; _∧_; not)
+open import Data.Nat     using (ℕ)
+open import Data.Fin     using (Fin; zero; suc)
+open import Data.Vec     using (Vec; []; _∷_; lookup)
+open import Data.List    using (List; []; _∷_)
+open import Data.Maybe   using (Maybe; just; nothing)
+open import Data.Product using (∃; _,_)
+open import Data.Empty   using (⊥; ⊥-elim)
 open import Relation.Nullary using (¬_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
 open import Data.Vec.Relation.Unary.Any using (Any; here; there)
 
 ------------------------------------------------------------------------
@@ -74,21 +87,15 @@ IsTrue true  = ⊤
 IsTrue false = ⊥
 
 ------------------------------------------------------------------------
--- 2.  Speculative aggregation: any-true over the portfolio
+-- 2.  Layer A — any-true aggregation over the portfolio
 ------------------------------------------------------------------------
 
--- Pure model of `parallelProofSearchSpeculative`. Returns true iff
--- at least one prover in the input vector returned success.
--- Structural recursion stands in for the Chapel-side atomic-CAS:
--- both compute the same predicate (∃ i. xs[i] = true), the latter
--- additionally records which index won the race.
 speculative : {n : ℕ} → Vec Bool n → Bool
 speculative []       = false
 speculative (b ∷ bs) = b ∨ speculative bs
 
 ------------------------------------------------------------------------
--- 3.  Soundness — if the portfolio verdict is true, an actual
---                 successful prover exists in the input
+-- 3.  Layer A soundness — a true verdict has a successful witness
 ------------------------------------------------------------------------
 
 speculative-sound : {n : ℕ} (xs : Vec Bool n)
@@ -99,8 +106,7 @@ speculative-sound (true  ∷ _)    _  = here tt
 speculative-sound (false ∷ bs)   p  = there (speculative-sound bs p)
 
 ------------------------------------------------------------------------
--- 4.  Completeness — if any prover succeeded, the aggregation
---                    cannot silently swallow the success
+-- 4.  Layer A completeness — no success is silently dropped
 ------------------------------------------------------------------------
 
 speculative-complete : {n : ℕ} (xs : Vec Bool n)
@@ -110,23 +116,221 @@ speculative-complete (true  ∷ _)  _          = tt
 speculative-complete (false ∷ _)  (here ())
 speculative-complete (false ∷ bs) (there p)  = speculative-complete bs p
 
+-- Index view of Any, used to connect the two layers.
+any→index : {n : ℕ} (xs : Vec Bool n) → Any IsTrue xs → ∃ λ i → lookup xs i ≡ true
+any→index (true  ∷ _)  (here _)  = zero , refl
+any→index (false ∷ _)  (here ())
+any→index (_ ∷ xs)     (there p) with any→index xs p
+... | i , eq = suc i , eq
+
+index→any : {n : ℕ} (xs : Vec Bool n) (i : Fin n) → lookup xs i ≡ true → Any IsTrue xs
+index→any (true  ∷ _)  zero    _  = here tt
+index→any (false ∷ _)  zero    ()
+index→any (_ ∷ xs)     (suc i) eq = there (index→any xs i eq)
+
 ------------------------------------------------------------------------
--- 5.  Cancellation-safety — a successful head wins regardless of
---                            the tail
---
--- Interpretation: in the Wave-1 speculative implementation no mid-flight
--- preemption happens. Even so, the FIRST observed success determines
--- the verdict; subsequent provers' outcomes (in this model, the tail
--- vector) cannot retroactively invalidate the win. Below: if `b = true`
--- at the head, the speculative result is true for ANY tail `bs`.
+-- 5.  Layer B — state, events and the step relation
+------------------------------------------------------------------------
+
+-- `winner` is `winnerIdx` (nothing = -1); `cancelled` is the token.
+record State (n : ℕ) : Set where
+  constructor ⟨_,_⟩
+  field
+    winner    : Maybe (Fin n)
+    cancelled : Bool
+open State public
+
+data Event (n : ℕ) : Set where
+  done   : Fin n → Event n   -- prover i's tryProver returns
+  signal : Event n           -- the CAS winner writes the cancel token
+
+start : {n : ℕ} → State n
+start = ⟨ nothing , false ⟩
+
+-- compareAndSwap(-1, i): succeeds only when no winner is recorded.
+cas : {n : ℕ} → Maybe (Fin n) → Fin n → Maybe (Fin n)
+cas nothing  i = just i
+cas (just w) _ = just w
+
+-- A finishing prover attempts the CAS only if its observed result is a
+-- success; the observed result is `false` once the token is set (exitCode -5).
+finish : {n : ℕ} → Bool → Maybe (Fin n) → Fin n → Maybe (Fin n)
+finish true  w i = cas w i
+finish false w _ = w
+
+-- Only a CAS winner writes the token; with no winner the event is a no-op.
+signalled : {n : ℕ} → Maybe (Fin n) → Bool → Bool
+signalled (just _) _ = true
+signalled nothing  c = c
+
+step : {n : ℕ} → Vec Bool n → State n → Event n → State n
+step rs ⟨ w , c ⟩ (done i) = ⟨ finish (not c ∧ lookup rs i) w i , c ⟩
+step rs ⟨ w , c ⟩ signal   = ⟨ w , signalled w c ⟩
+
+-- An execution: any interleaving of events, applied in order.
+run : {n : ℕ} → Vec Bool n → State n → List (Event n) → State n
+run rs s []       = s
+run rs s (e ∷ es) = run rs (step rs s e) es
+
 ------------------------------------------------------------------------
+-- 6.  The protocol invariant: winners succeeded, and the token is set
+--     only after a win
+------------------------------------------------------------------------
+
+Good : {n : ℕ} → Vec Bool n → Maybe (Fin n) → Set
+Good rs nothing  = ⊤
+Good rs (just w) = lookup rs w ≡ true
+
+Armed : {n : ℕ} → Maybe (Fin n) → Bool → Set
+Armed nothing  c = c ≡ false
+Armed (just _) _ = ⊤
+
+record Inv {n : ℕ} (rs : Vec Bool n) (s : State n) : Set where
+  field
+    good  : Good rs (winner s)
+    armed : Armed (winner s) (cancelled s)
+open Inv public
+
+start-inv : {n : ℕ} (rs : Vec Bool n) → Inv rs start
+start-inv rs = record { good = tt ; armed = refl }
 
-cancellation-safety : {n : ℕ} (bs : Vec Bool n)
-                    → IsTrue (speculative (true ∷ bs))
-cancellation-safety _ = tt
+finish-just : {n : ℕ} (b : Bool) (v i : Fin n) → finish b (just v) i ≡ just v
+finish-just true  v i = refl
+finish-just false v i = refl
+
+done-from-nothing : {n : ℕ} (rs : Vec Bool n) (i : Fin n) (b : Bool)
+                  → lookup rs i ≡ b
+                  → Inv rs ⟨ finish b nothing i , false ⟩
+done-from-nothing rs i true  eq = record { good = eq ; armed = tt }
+done-from-nothing rs i false _  = record { good = tt ; armed = refl }
+
+step-inv : {n : ℕ} (rs : Vec Bool n) (s : State n) (e : Event n)
+         → Inv rs s → Inv rs (step rs s e)
+step-inv rs ⟨ just v , c ⟩ (done i) inv
+  rewrite finish-just (not c ∧ lookup rs i) v i = record { good = good inv ; armed = tt }
+step-inv rs ⟨ nothing , true ⟩  (done i) record { armed = () }
+step-inv rs ⟨ nothing , false ⟩ (done i) inv = done-from-nothing rs i (lookup rs i) refl
+step-inv rs ⟨ just v  , c ⟩ signal inv = record { good = good inv ; armed = tt }
+step-inv rs ⟨ nothing , c ⟩ signal inv = inv
+
+run-inv : {n : ℕ} (rs : Vec Bool n) (s : State n) (es : List (Event n))
+        → Inv rs s → Inv rs (run rs s es)
+run-inv rs s []       inv = inv
+run-inv rs s (e ∷ es) inv = run-inv rs (step rs s e) es (step-inv rs s e inv)
 
 ------------------------------------------------------------------------
--- 6.  Sanity checks (executable; close the loop on the definitions)
+-- 7.  Soundness, stability and cancellation-safety over every schedule
+------------------------------------------------------------------------
+
+-- The reported winner, at ANY index, genuinely succeeded.
+race-sound : {n : ℕ} (rs : Vec Bool n) (es : List (Event n)) {w : Fin n}
+           → winner (run rs start es) ≡ just w → lookup rs w ≡ true
+race-sound rs es eq = subst (Good rs) eq (good (run-inv rs start es (start-inv rs)))
+
+step-keeps : {n : ℕ} (rs : Vec Bool n) (s : State n) (e : Event n) {w : Fin n}
+           → winner s ≡ just w → winner (step rs s e) ≡ just w
+step-keeps rs ⟨ just v , c ⟩ (done i) refl = finish-just (not c ∧ lookup rs i) v i
+step-keeps rs ⟨ just v , c ⟩ signal   refl = refl
+
+-- Cancellation-safety (1): once a winner is recorded, no later event —
+-- a loser's success, a preempted loser, or the cancel write — changes it.
+winner-stable : {n : ℕ} (rs : Vec Bool n) (s : State n) (es : List (Event n)) {w : Fin n}
+              → winner s ≡ just w → winner (run rs s es) ≡ just w
+winner-stable rs s []       eq = eq
+winner-stable rs s (e ∷ es) eq = winner-stable rs (step rs s e) es (step-keeps rs s e eq)
+
+-- Cancellation-safety (2): after the token is set, a finishing prover
+-- (preempted, exitCode -5) leaves the whole state unchanged.
+preempted-inert : {n : ℕ} (rs : Vec Bool n) (w : Maybe (Fin n)) (i : Fin n)
+                → step rs ⟨ w , true ⟩ (done i) ≡ ⟨ w , true ⟩
+preempted-inert rs w i = refl
+
+-- Cancellation-safety (3): in every reachable state the token is set only
+-- if a winner exists, so a success is never preempted before a win.
+cancel-after-win : {n : ℕ} (rs : Vec Bool n) (es : List (Event n))
+                 → Armed (winner (run rs start es)) (cancelled (run rs start es))
+cancel-after-win rs es = armed (run-inv rs start es (start-inv rs))
+
+------------------------------------------------------------------------
+-- 8.  Completeness and the winner's identity
+------------------------------------------------------------------------
+
+data _∈_ {n : ℕ} (e : Event n) : List (Event n) → Set where
+  now   : {es : List (Event n)} → e ∈ (e ∷ es)
+  later : {e′ : Event n} {es : List (Event n)} → e ∈ es → e ∈ (e′ ∷ es)
+
+IsSet : {n : ℕ} → Maybe (Fin n) → Set
+IsSet nothing  = ⊥
+IsSet (just _) = ⊤
+
+set-stays : {n : ℕ} (rs : Vec Bool n) (s : State n) (es : List (Event n)) {w : Fin n}
+          → winner s ≡ just w → IsSet (winner (run rs s es))
+set-stays rs s es eq with winner (run rs s es) | winner-stable rs s es eq
+... | just _ | _ = tt
+
+done-sets : {n : ℕ} (rs : Vec Bool n) (s : State n) (i : Fin n)
+          → Inv rs s → lookup rs i ≡ true
+          → ∃ λ w → winner (step rs s (done i)) ≡ just w
+done-sets rs ⟨ just v , c ⟩    i _ _ = v , finish-just (not c ∧ lookup rs i) v i
+done-sets rs ⟨ nothing , true ⟩  i record { armed = () } _
+done-sets rs ⟨ nothing , false ⟩ i _ eq rewrite eq = i , refl
+
+-- If a successful prover finishes at any point of any schedule, there is
+-- a winner at the end — whatever else happened before or after.
+race-complete : {n : ℕ} (rs : Vec Bool n) (s : State n) (es : List (Event n)) {i : Fin n}
+              → Inv rs s → lookup rs i ≡ true → done i ∈ es
+              → IsSet (winner (run rs s es))
+race-complete rs s (done i ∷ es) inv ok now with done-sets rs s i inv ok
+... | _ , eq = set-stays rs (step rs s (done i)) es eq
+race-complete rs s (e ∷ es) inv ok (later p) =
+  race-complete rs (step rs s e) es (step-inv rs s e inv) ok p
+
+-- The first successful prover to reach the CAS, in schedule order.
+pick : {n : ℕ} → Bool → Fin n → Maybe (Fin n) → Maybe (Fin n)
+pick true  i _    = just i
+pick false _ rest = rest
+
+first : {n : ℕ} → Vec Bool n → List (Event n) → Maybe (Fin n)
+first rs []            = nothing
+first rs (signal ∷ es) = first rs es
+first rs (done i ∷ es) = pick (lookup rs i) i (first rs es)
+
+-- The winner is exactly the first successful prover to reach the CAS (not
+-- necessarily the first to return from `tryProver`): any index can win,
+-- and the result is determined by the schedule alone.
+winner-is-first : {n : ℕ} (rs : Vec Bool n) (es : List (Event n))
+                → winner (run rs start es) ≡ first rs es
+winner-is-first rs []            = refl
+winner-is-first rs (signal ∷ es) = winner-is-first rs es
+winner-is-first rs (done i ∷ es) = go (lookup rs i)
+  where
+  go : (b : Bool) → winner (run rs ⟨ finish b nothing i , false ⟩ es) ≡ pick b i (first rs es)
+  go true  = winner-stable rs ⟨ just i , false ⟩ es refl
+  go false = winner-is-first rs es
+
+------------------------------------------------------------------------
+-- 9.  Agreement with layer A on schedules where every prover finishes
+------------------------------------------------------------------------
+
+Covers : {n : ℕ} → List (Event n) → Set
+Covers {n} es = (i : Fin n) → done i ∈ es
+
+isSet→just : {n : ℕ} (m : Maybe (Fin n)) → IsSet m → ∃ λ w → m ≡ just w
+isSet→just (just w) _ = w , refl
+isSet→just nothing  ()
+
+race-agrees : {n : ℕ} (rs : Vec Bool n) (es : List (Event n)) → Covers es
+            → IsTrue (speculative rs) → IsSet (winner (run rs start es))
+race-agrees rs es cov p with any→index rs (speculative-sound rs p)
+... | i , ok = race-complete rs start es (start-inv rs) ok (cov i)
+
+race-agrees-sound : {n : ℕ} (rs : Vec Bool n) (es : List (Event n))
+                  → IsSet (winner (run rs start es)) → IsTrue (speculative rs)
+race-agrees-sound rs es set with isSet→just (winner (run rs start es)) set
+... | w , eq = speculative-complete rs (index→any rs w (race-sound rs es eq))
+
+------------------------------------------------------------------------
+-- 10.  Sanity checks (executable; close the loop on the definitions)
 ------------------------------------------------------------------------
 
 example-empty : speculative (false ∷ false ∷ false ∷ []) ≡ false
@@ -135,12 +339,27 @@ example-empty = refl
 example-some  : speculative (false ∷ true  ∷ false ∷ []) ≡ true
 example-some  = refl
 
-example-head  : speculative (true  ∷ false ∷ false ∷ []) ≡ true
-example-head  = refl
+-- Two successes race; prover 2 finishes first and wins, the token is set,
+-- and prover 1's later success is preempted. The winner is index 2, not 0.
+race-example : winner (run (false ∷ true ∷ true ∷ [])
+                           start
+                           (done (suc (suc zero)) ∷ signal ∷ done (suc zero) ∷ done zero ∷ []))
+             ≡ just (suc (suc zero))
+race-example = refl
+
+-- A success that finishes BEFORE the winner's cancel write still loses the
+-- CAS: the winner is unchanged.
+cas-race-example : winner (run (true ∷ true ∷ [])
+                               start
+                               (done zero ∷ done (suc zero) ∷ signal ∷ []))
+                 ≡ just zero
+cas-race-example = refl
+
+-- No success, no winner, on any schedule shape used here.
+no-winner-example : winner (run (false ∷ false ∷ []) start (done zero ∷ signal ∷ done (suc zero) ∷ []))
+                  ≡ nothing
+no-winner-example = refl
 
--- All-false vector cannot witness Any IsTrue (contrapositive of
--- soundness; useful as an independent sanity check that IsTrue
--- IsTrue false is uninhabited under this encoding).
 no-success-2 : ¬ Any IsTrue (false ∷ false ∷ [])
 no-success-2 (here ())
 no-success-2 (there (here ()))
diff --git a/src/chapel/parallel_proof_search.chpl b/src/chapel/parallel_proof_search.chpl
index 53ad5c52..8250b895 100644
--- a/src/chapel/parallel_proof_search.chpl
+++ b/src/chapel/parallel_proof_search.chpl
@@ -656,8 +656,11 @@ proc parallelProofSearch(goal: string, provers: [] ProverInfo,
 // terminate — their results land in the table with exitCode = -5
 // instead of running to completion, but they are never returned to
 // the caller because `winner` is set before any cancellation could
-// race the CAS. See proofs/agda/ParallelSoundness.agda:
-// `cancellation-safety` for the formal statement.
+// race the CAS. See proofs/agda/ParallelSoundness.agda, layer B: a
+// small-step model of this procedure over every interleaving, with
+// `winner-stable`, `preempted-inert`, `cancel-after-win`, `race-sound`,
+// `race-complete` and `winner-is-first`. Its assumed boundary is that
+// these atomics are sequentially consistent (Chapel's default order).
 //
 // Telemetry: losers that self-SIGKILLed land in `results` with
 // exitCode = -5, which `classifyOutcome` maps to `preempted`.
diff --git a/src/rust/proof_search.rs b/src/rust/proof_search.rs
index 3c90d3bf..949b63c9 100644
--- a/src/rust/proof_search.rs
+++ b/src/rust/proof_search.rs
@@ -384,7 +384,8 @@ mod chapel_ffi {
                         let start = start.clone();
                         std::thread::spawn(move || {
                             start.wait();
-                            let strategy = ChapelParallelSearch::new().expect("real Chapel runtime");
+                            let strategy =
+                                ChapelParallelSearch::new().expect("real Chapel runtime");
                             assert_eq!(ChapelParallelSearch::available_prover_count(), 0);
                             for _ in 0..2 {
                                 assert!(strategy.available());
@@ -414,10 +415,8 @@ mod chapel_ffi {
             // No global environment mutation races with other Rust tests, and
             // no external prover can be dispatched by this allocation/free probe.
             let empty_path = tempfile::tempdir().expect("empty prover search directory");
-            let mut command = real_probe_command(
-                "real_search_without_provers_fails_and_frees_result",
-                CHILD,
-            );
+            let mut command =
+                real_probe_command("real_search_without_provers_fails_and_frees_result", CHILD);
             command.env("PATH", empty_path.path());
             run_real_probe(
                 &mut command,
@@ -478,7 +477,10 @@ mod chapel_ffi {
                     matches!(stopped_before_cleanup, Ok(true)),
                     "deadline returned with a live or unobservable prover: {stopped_before_cleanup:?}"
                 );
-                assert!(elapsed < Duration::from_secs(3), "deadline took {elapsed:?}");
+                assert!(
+                    elapsed < Duration::from_secs(3),
+                    "deadline took {elapsed:?}"
+                );
                 let result = result.expect("native timeout returns a failed search result");
                 assert!(!result.success);
                 assert_eq!(
@@ -500,17 +502,12 @@ mod chapel_ffi {
             .expect("write finite prover");
             std::fs::set_permissions(&prover, std::fs::Permissions::from_mode(0o700))
                 .expect("make finite prover executable");
-            let mut command = real_probe_command(
-                "real_search_deadline_stops_the_owned_prover",
-                CHILD,
-            );
+            let mut command =
+                real_probe_command("real_search_deadline_stops_the_owned_prover", CHILD);
             command
                 .env("PATH", fixture.path())
                 .env(PID_FILE, fixture.path().join("prover.pid"));
-            run_real_probe(
-                &mut command,
-                "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED",
-            );
+            run_real_probe(&mut command, "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED");
         }
     }
 }
diff --git a/src/rust/provers/chuffed.rs b/src/rust/provers/chuffed.rs
index 879e33ba..35d30d3a 100644
--- a/src/rust/provers/chuffed.rs
+++ b/src/rust/provers/chuffed.rs
@@ -236,16 +236,12 @@ mod tests {
 
     #[cfg(unix)]
     fn version_fixture(script: &str, timeout: u64) -> (tempfile::TempDir, ChuffedBackend) {
-        use std::os::unix::fs::PermissionsExt;
-
         let directory = tempfile::tempdir().unwrap();
         let executable = directory.path().join("version-probe");
-        std::fs::write(
+        crate::provers::test_fixture::write_executable(
             &executable,
-            format!("#!/bin/sh\n[ \"$#\" -eq 1 ] && [ \"$1\" = '--help' ] || exit 64\n{script}\n"),
-        )
-        .unwrap();
-        std::fs::set_permissions(&executable, std::fs::Permissions::from_mode(0o700)).unwrap();
+            &format!("#!/bin/sh\n[ \"$#\" -eq 1 ] && [ \"$1\" = '--help' ] || exit 64\n{script}\n"),
+        );
         let backend = ChuffedBackend::new(ProverConfig {
             executable,
             timeout,
diff --git a/src/rust/provers/faial.rs b/src/rust/provers/faial.rs
index 1983cdf6..d4e8cb41 100644
--- a/src/rust/provers/faial.rs
+++ b/src/rust/provers/faial.rs
@@ -355,18 +355,14 @@ mod tests {
 
     #[cfg(unix)]
     fn version_fixture(script: &str, timeout: u64) -> (tempfile::TempDir, FaialBackend) {
-        use std::os::unix::fs::PermissionsExt;
-
         let directory = tempfile::tempdir().unwrap();
         let executable = directory.path().join("version-probe");
-        std::fs::write(
+        crate::provers::test_fixture::write_executable(
             &executable,
-            format!(
+            &format!(
                 "#!/bin/sh\n[ \"$#\" -eq 1 ] && [ \"$1\" = '--version' ] || exit 64\n{script}\n"
             ),
-        )
-        .unwrap();
-        std::fs::set_permissions(&executable, std::fs::Permissions::from_mode(0o700)).unwrap();
+        );
         let backend = FaialBackend::new(ProverConfig {
             executable,
             timeout,
diff --git a/src/rust/provers/gpuverify.rs b/src/rust/provers/gpuverify.rs
index f994ce82..2a8c4bf0 100644
--- a/src/rust/provers/gpuverify.rs
+++ b/src/rust/provers/gpuverify.rs
@@ -389,18 +389,14 @@ mod tests {
 
     #[cfg(unix)]
     fn version_fixture(script: &str, timeout: u64) -> (tempfile::TempDir, GpuVerifyBackend) {
-        use std::os::unix::fs::PermissionsExt;
-
         let directory = tempfile::tempdir().unwrap();
         let executable = directory.path().join("version-probe");
-        std::fs::write(
+        crate::provers::test_fixture::write_executable(
             &executable,
-            format!(
+            &format!(
                 "#!/bin/sh\n[ \"$#\" -eq 1 ] && [ \"$1\" = '--version' ] || exit 64\n{script}\n"
             ),
-        )
-        .unwrap();
-        std::fs::set_permissions(&executable, std::fs::Permissions::from_mode(0o700)).unwrap();
+        );
         let backend = GpuVerifyBackend::new(ProverConfig {
             executable,
             timeout,
diff --git a/src/rust/provers/mod.rs b/src/rust/provers/mod.rs
index 51a527c0..48668a2e 100644
--- a/src/rust/provers/mod.rs
+++ b/src/rust/provers/mod.rs
@@ -14,6 +14,8 @@ use std::path::{Path, PathBuf};
 use crate::core::{ProofState, Tactic, TacticResult};
 
 pub mod outcome;
+#[cfg(all(test, unix))]
+pub(crate) mod test_fixture;
 pub use outcome::{classify_anyhow_error, ProverOutcome};
 
 pub mod io;
diff --git a/src/rust/provers/test_fixture.rs b/src/rust/provers/test_fixture.rs
new file mode 100644
index 00000000..d69db34c
--- /dev/null
+++ b/src/rust/provers/test_fixture.rs
@@ -0,0 +1,52 @@
+// SPDX-License-Identifier: MPL-2.0
+//! Test-only helper for writing an executable fixture script.
+//!
+//! Writing a script and executing it straight away races with every other
+//! test thread that spawns a process: a `fork` taken while the write
+//! descriptor is still open copies it into the child, and until that child
+//! reaches `exec` (the descriptor is close-on-exec) the kernel refuses to
+//! execute the file with `ETXTBSY` ("Text file busy"). That failure showed up
+//! in CI as `Failed to execute fzn-chuffed --help: Text file busy`.
+//!
+//! [`write_executable`] closes its own descriptor and then runs the script
+//! once with a sentinel argument until the kernel accepts it. After one
+//! successful `exec` no writer is left and no later `fork` can inherit one,
+//! so the test's own spawn cannot see `ETXTBSY`. The fixture scripts exit at
+//! once on any argument they do not expect, so the probe runs no fixture body.
+
+use std::io::{ErrorKind, Write};
+use std::os::unix::fs::OpenOptionsExt;
+use std::path::Path;
+use std::time::Duration;
+
+/// Write `contents` to `path` as an owner-executable script and wait until the
+/// kernel will execute it. The script must exit without side effects when
+/// called with a single unexpected argument.
+pub(crate) fn write_executable(path: &Path, contents: &str) {
+    {
+        let mut file = std::fs::OpenOptions::new()
+            .write(true)
+            .create_new(true)
+            .mode(0o700)
+            .open(path)
+            .expect("create fixture executable");
+        file.write_all(contents.as_bytes())
+            .expect("write fixture executable");
+    }
+    for _ in 0..200 {
+        match std::process::Command::new(path)
+            .arg("--echidna-fixture-ready")
+            .stdin(std::process::Stdio::null())
+            .stdout(std::process::Stdio::null())
+            .stderr(std::process::Stdio::null())
+            .status()
+        {
+            Err(error) if error.kind() == ErrorKind::ExecutableFileBusy => {
+                std::thread::sleep(Duration::from_millis(10));
+            },
+            Err(error) => panic!("fixture executable cannot run: {error}"),
+            Ok(_) => return,
+        }
+    }
+    panic!("fixture executable stayed busy (ETXTBSY) for 2 s");
+}
diff --git a/src/rust/provers/version_probe.rs b/src/rust/provers/version_probe.rs
index 081e88dd..0410de7c 100644
--- a/src/rust/provers/version_probe.rs
+++ b/src/rust/provers/version_probe.rs
@@ -54,14 +54,12 @@ mod tests {
         fn fixture(script: &str, timeout: u64) -> (tempfile::TempDir, ProverConfig) {
             let directory = tempfile::tempdir().unwrap();
             let executable = directory.path().join("version-probe");
-            std::fs::write(
+            crate::provers::test_fixture::write_executable(
                 &executable,
-                format!(
+                &format!(
                     "#!/bin/sh\n[ \"$#\" -eq 1 ] && [ \"$1\" = '--version' ] || exit 64\n{script}\n"
                 ),
-            )
-            .unwrap();
-            std::fs::set_permissions(&executable, std::fs::Permissions::from_mode(0o700)).unwrap();
+            );
             let config = ProverConfig {
                 executable,
                 timeout,
diff --git a/src/zig_ffi/chapel_bridge.zig b/src/zig_ffi/chapel_bridge.zig
index 807c23fe..f8d12591 100644
--- a/src/zig_ffi/chapel_bridge.zig
+++ b/src/zig_ffi/chapel_bridge.zig
@@ -70,7 +70,8 @@ fn callOnOwner(owner: anytype, comptime function: anytype, args: anytype, result
         result: @TypeOf(result),
 
         fn run(raw: *anyopaque) void {
-            const self: *@This() = @ptrCast(@alignCast(raw));
+            // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+            const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
             self.result.* = @call(.auto, function, self.arguments);
         }
     };
@@ -650,7 +651,8 @@ const CallerAllocator = struct {
     }
 
     fn alloc(raw: *anyopaque, len: usize, alignment: std.mem.Alignment, ret_addr: usize) ?[*]u8 {
-        const self: *@This() = @ptrCast(@alignCast(raw));
+        // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+        const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
         if (!self.record() or self.allocations >= self.fail_after) return null;
         const pointer = std.heap.c_allocator.rawAlloc(len, alignment, ret_addr) orelse return null;
         self.allocations += 1;
@@ -659,7 +661,8 @@ const CallerAllocator = struct {
     }
 
     fn resize(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) bool {
-        const self: *@This() = @ptrCast(@alignCast(raw));
+        // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+        const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
         _ = self.record();
         _ = memory;
         _ = alignment;
@@ -669,7 +672,8 @@ const CallerAllocator = struct {
     }
 
     fn remap(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) ?[*]u8 {
-        const self: *@This() = @ptrCast(@alignCast(raw));
+        // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+        const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
         _ = self.record();
         _ = memory;
         _ = alignment;
@@ -679,7 +683,8 @@ const CallerAllocator = struct {
     }
 
     fn free(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, ret_addr: usize) void {
-        const self: *@This() = @ptrCast(@alignCast(raw));
+        // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+        const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
         _ = self.record();
         // The backing allocator is cross-thread safe so a failed assertion
         // never requires corrupting memory or leaking the test allocation.
diff --git a/src/zig_ffi/runtime_owner.zig b/src/zig_ffi/runtime_owner.zig
index 79d9d543..da2f1b8a 100644
--- a/src/zig_ffi/runtime_owner.zig
+++ b/src/zig_ffi/runtime_owner.zig
@@ -169,7 +169,8 @@ const Probe = struct {
     }
 
     fn work(raw: *anyopaque) void {
-        const self: *@This() = @ptrCast(@alignCast(raw));
+        // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+        const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
         self.wrong_thread = self.wrong_thread or self.init_id != std.Thread.getCurrentId();
         self.calls += 1;
     }
@@ -239,7 +240,8 @@ test "shutdown drains accepted work and refuses new work before joining" {
         shutdown_failed: bool = false,
 
         fn work(raw: *anyopaque) void {
-            const self: *@This() = @ptrCast(@alignCast(raw));
+            // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+            const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
             self.mutex.lock();
             self.entered = true;
             self.changed.broadcast();
@@ -311,7 +313,8 @@ test "owner callbacks cannot re-enter or finalize themselves" {
         stop_refused: bool = false,
 
         fn work(raw: *anyopaque) void {
-            const self: *@This() = @ptrCast(@alignCast(raw));
+            // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+            const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
             var nested = Work{ .context = self.probe, .run = Probe.work };
             self.call_refused = if (self.owner.call(&nested)) |_| false else |err| err == error.ReentrantCall;
             self.stop_refused = if (self.owner.shutdown()) |_| false else |err| err == error.ReentrantCall;
@@ -358,7 +361,8 @@ test "a nonowner process-exit request refuses active work without a join cycle"
         exit_refused: bool = false,
 
         fn work(raw: *anyopaque) void {
-            const self: *@This() = @ptrCast(@alignCast(raw));
+            // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with
+            const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds
             self.mutex.lock();
             self.entered = true;
             self.changed.broadcast();