Queue M30: survey how much algorithm correctness can be machine-checked

[MikeGrier]

Adds a repository-level milestone asking how much of this workspace's concurrency can be machine-checked, framed as a scoping instrument rather than a replacement for testing and inspection.

Why

The workspace checks concurrency with recorded reasoning, unit tests, a sabotage suite and a mutation sweep. That has found real bugs. It also has a measured blind spot: weakening a producer's Acquire load of the consumer's position to Relaxed left the entire windows-waitable-queues suite green, while every logic defect injected beside it was caught. A test observes what a run happened to do; it cannot observe an ordering a run happened not to need.

A method that proves a protocol correct for three producers and a capacity of two does not prove the shipping code correct — but it moves a class of question out of argued carefully into checked, leaving a short named list of what still needs inspection. That list is the deliverable.

The five items

1. Survey the argued-but-unchecked algorithms and match each to a tool class — TLA+/PlusCal (protocol-level, exhaustive over a small configuration, no memory model), loom (actual Rust under C11, which is where the measured blind spot lives), bounded proof, const assertions, or none. The "no tool fits this" rows matter as much as the rest.

2. Pilot exactly one, chosen because parameter shrinking turns an untestable property into an exhaustive one: reserving_mpsc's claim-position recurrence needs 2^32 pushes to reach the wrap — about 37 seconds of sustained maximum-rate pushing, far outside a unit suite but not beyond a long integration test. The count is not what makes it untestable. Reaching the wrap is necessary but not sufficient: a producer must also be stalled inside a window a few instructions wide, and no test can schedule that. A model whose position wraps at 8 makes the whole interleaving exhaustive in seconds and yields a trace.

   Success has an unusual shape here, because SH-14.1 is a live defect this crate ships and documents — not a hypothetical. A faithful model of the shipping protocol at a wrappable width must find it, so a green run on that model is evidence the model is unfaithful rather than evidence the protocol is sound. The two checks therefore attach to configurations rather than to modified and unmodified code: the model must reproduce SH-14.1 where the wrap is reachable, and must come back green where it is not (pushes bounded below the wrap, or a single producer, which has no race to lose). Plus a stated refinement argument, or the result is a counterexample in a toy model and nothing more.

3. Record what the pilot could not reach, by name, beside the existing "How far the memory orderings are verified, and how far they are not" section.

4. Re-home M31.6 (see below).

5. Decide adoption, with its cost stated.

Two things it is careful about

• It does not pre-empt D-31, which decided on considered grounds that 0.1.0 ships without machine-checked orderings. D-31's reasoning is the starting point rather than something to overturn: a model checker covers atomics and cannot cover SetEvent/ResetEvent, so stubbing them verifies a model of SetEvent rather than SetEvent — the "measures the model, not the thing" trap this workspace has already been caught by once.
• It names the cost that applies to any specification: it is another statement of the contract, able to drift from the code with nothing to detect it. That is CONTRACT INTEGRITY's restatement problem applied to an artefact that looks authoritative, so a stale model that still passes is worse than no model. The decision has to say what keeps the two in step, who re-runs it, and what happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome — D-31 reached one already on narrower grounds.

Found while writing it

M31.6 — the loom verification windows-waitable-queues tells adopters is planned before 1.0 — is referenced three times in that crate's design notes and, until this PR, had no live checklist item anywhere in the repository; the crate has only a COMPLETED-CHECKLIST.md. A public commitment that nothing will cause anyone to pick up is exactly the "design notes are not a work queue" failure the repository instructions name. M30.4 re-homes it with the scope D-31 describes (both MPSC shapes or neither).

Note on the milestone number: this was authored as M23 and renumbered to M30 in 4e94a3f. M23 was already taken by an archived milestone in the root COMPLETED-CHECKLIST.md, including an anchored M23.6, so the two would have given M23.1–M23.5 a second meaning in an append-only history. M30 is the next free number.

Verification

Both files ASCII and LF-only; every relative link resolves; the #d-31 anchor exists and matches how the rest of the repository links to D-numbers. Documentation only — no code, no build impact.

[Copilot]

🟡 Changes recommended

Documentation clarifications and checklist-hygiene updates are needed before approval.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Adds repository-level M23 planning for evaluating machine-checking options for concurrency correctness.

Changes:

• Registers M23 in the repository plan.
• Defines survey, pilot, limitation, re-homing, and adoption-decision work items.

File summaries

File	Summary
PLANS.md	Registers the new M23 milestone.
CHECKLIST.md	Defines M23 and its planned work items.

Review details

Suppressed comments (9)

CHECKLIST.md:279

• Add a blank line before ## M-inf. The checklist hygiene rule requires a separator between a multi-line item's final continuation and the next milestone heading; without it, the newly added M23.5 runs directly into the parked section.

  once already on narrower grounds.

CHECKLIST.md:229

• M23.1 requires a survey table but does not name where that table will live. Because this is a repository-level scoping instrument, the result needs a durable, named artifact rather than existing only in the eventual review discussion; specify the target document here.

  The output is a table, and the "no tool fits this" rows are as valuable as the rest.

CHECKLIST.md:260

• After adding M23.4, this sentence is no longer true: M23.4 is itself a live checklist item, even though the queue crate has only a completed checklist. Rephrase it as a pre-change state so the rationale does not contradict the checklist it describes.

  tells adopters it is planned before 1.0. There is no live checklist item for it anywhere in the
  repository -- the crate has only a `COMPLETED-CHECKLIST.md`. That is the "design notes are not a

CHECKLIST.md:253

• This documentation location is only correct if M23.2 actually pilots reserving_mpsc. The item currently leaves another candidate open, but the waitable-queues README is not the right home for limitations of a file-watcher, IoRing, or other pilot. Make the pilot choice mandatory here or say that M23.3 records the limits beside whichever component is piloted.

  Put it where a reader deciding how much to trust the crate will meet it -- beside the existing
  "How far the memory orderings are verified, and how far they are not" section, which is already
  written in the right register.

CHECKLIST.md:218

• Please distinguish the already executable windows-file-watcher ContractChecker from the production watcher state machine here. The checker already has tests and is shared with generators, so naming the candidate only as the watcher's 'contract state machine' mixes an existing oracle with behavior that may still be argued and makes the survey population ambiguous.

  flag against `SetEvent`/`ResetEvent`; `windows-file-watcher`'s contract state machine;

CHECKLIST.md:253

• This deliverable will become another contract statement, but the existing disclosure is duplicated in both crates/windows-waitable-queues/src/lib.rs and README.md (and summarized in the design notes). Pointing only to “the existing section” leaves room to update one copy and recreate the restatement drift this milestone calls out; require all copies to be updated together.

  Put it where a reader deciding how much to trust the crate will meet it -- beside the existing
  "How far the memory orderings are verified, and how far they are not" section, which is already
  written in the right register.

CHECKLIST.md:193

• These paragraphs are rationale and historical context, not checklist actions. The repository's checklist hygiene requires CHECKLIST files to remain an actionable work queue; move this explanation to the design notes and keep only a short constraint/link in M23.

**Why now, and what this is not.** The workspace's concurrency is checked today by reasoning recorded
beside the code, an extensive unit suite, a sabotage suite that injects defects and requires each to
be caught, and a cargo-mutants sweep. That combination has found real bugs -- `D-15`'s lost wakeup
among them. It also has a measured blind spot:

CHECKLIST.md:265

• M23.4 moves work from the root source-component into windows-waitable-queues, but it does not include the required cross-component handoff naming the destination component and M31.6, nor require the reciprocal prerequisite in the new crate checklist. Add those callouts when creating the destination checklist so the dependency order is explicit.

  Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or
  neither), and make the design-note references point at it.

PLANS.md:19

• This summary is stale as written: the same change adds the live M23.4 item that schedules M31.6, so it no longer exists only in design notes with no live checklist item. Reword this as a pre-existing orphan that is now scheduled by M23.4.

| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M23: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) |

• Files reviewed: 2/2 changed files
• Comments generated: 2
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Copilot]

🟡 Changes recommended

Unresolved moderate documentation inconsistencies and link/formatting issues remain in both reviewed files.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (4)

Previously missed (1) — in code that hasn't changed since the last review.

CHECKLIST.md:280

• Add a blank line before ## M-inf. M30.5 is a multi-line checklist item, and the repository's checklist format requires a blank separator between such an item and the next milestone heading; without it the new milestone runs into the parked-work section.

CHECKLIST.md:192

• This new reference to the queue crate's D-15 should be clickable. Multiple D-15 decisions exist in the workspace, so the bare identifier is ambiguous; link it to the queue design decision at crates/windows-waitable-queues/DESIGN-NOTES.md#d-15.

be caught, and a cargo-mutants sweep. That combination has found real bugs -- `D-15`'s lost wakeup

CHECKLIST.md:260

• This new text mentions the queue crate's COMPLETED-CHECKLIST.md as a bare filename. Repository documentation requires references to project documents to be clickable relative links; please link the existing file so readers can open the archived checklist directly.

  repository -- the crate has only a `COMPLETED-CHECKLIST.md`. That is the "design notes are not a

CHECKLIST.md:260

• After this PR lands, M30.4 is itself a live checklist item, so the statement that there is "no live checklist item ... anywhere" is false. Reword it as a pre-M30.4 historical fact, and link the queue's existing COMPLETED-CHECKLIST.md as required for repository-document references.

  tells adopters it is planned before 1.0. There is no live checklist item for it anywhere in the
  repository -- the crate has only a `COMPLETED-CHECKLIST.md`. That is the "design notes are not a

• Files reviewed: 2/2 changed files
• Comments generated: 2
• Review effort level: Lite

[MikeGrier]

Response to this round (4 inline + 4 suppressed)

All eight addressed in d909c38, plus the PR metadata. Two of them were factual errors in the milestone's central argument, and correcting them made the argument stronger.

CHECKLIST.md:236 — "beyond any test" overstates, and names the wrong reason

Changed, and this was the best finding of the round. Both halves of the claim were wrong:

• The count is reachable. 2^32 pushes is about 37 seconds of sustained maximum-rate pushing on the host the queue crate publishes. That is far outside a unit suite budgeted in milliseconds, but it is not beyond a long integration test, so "beyond any test" overstated it.
• The count was never the reason. As you note, the crate's README records that reaching the wrap is necessary but not sufficient — a producer must also be stalled inside a window a few instructions wide. That is what no test can schedule.

The correction improves the item rather than weakening it. Parameter shrinking now earns its place for the right reason: it makes the interleaving exhaustive rather than sampled, instead of merely making a count small. A 37-second test would still only observe what one run happened to do — which is the same blind spot the milestone's opening paragraph is built on.

CHECKLIST.md:238 — capacity == 1 is the wrong shape

Changed — removed, and verified before removing. You are right on both counts. Every statement of the collapse in the crate attributes it to slotwise_mpsc's slot sequence arithmetic (three states distinguished by counting), recorded as D-12. It has nothing to do with reserving_mpsc's claim position.

It is also already resolved: slotwise_mpsc refuses a capacity below two, and sabotage.json carries an entry holding that. So it was not merely the wrong shape, it was a settled property with a test on it — pointing the one pilot there would have spent the milestone's single experiment on a closed question.

CHECKLIST.md:260 — an item asserting a fact its own existence falsifies

Changed. Correct and neatly put: M30.4 said no live checklist item for M31.6 exists anywhere in the repository, which stops being true the moment M30.4 lands. Reworded as the pre-M30.4 fact it is ("until this item, there was no...").

CHECKLIST.md:188 — PR metadata still said M23

Changed. This is my own drift: I renumbered the checklist in 4e94a3f when M23 turned out to collide with an archived milestone, and did not carry the change into the PR title or body. Title and body are now M30, and the body carries a short note explaining the renumber so the history is legible.

Worth flagging that this is the second time in two days that a PR description has been the last surviving copy of a corrected claim — it is prose that restates the work, but it is not a file in the tree, so no sweep or CI check reaches it.

The reference-hygiene four

• D-15 bare identifier — changed, and you were right that it is ambiguous: five crates in this workspace define a D-15. Now linked to the queue's, which is indeed the lost wakeup.
• COMPLETED-CHECKLIST.md — changed, now a relative link per the convention.
• Blank line before ## M-inf — changed; M30.5 is multi-line, so the format requires the separator.
• PLANS.md Design Notes cell — changed. It pointed M30 readers at the namespace-remoting anchor, which is unrelated. The cell now scopes that link to M19-M22 and says M30 has no decision recorded yet — which is not an omission but the thing M30.5 exists to produce.

---

What the round taught

The two substantive findings were both in the justification, not the plan. The five items were fine; what was wrong was the argument for why item 2 is worth doing — an overstated limitation and a mis-attributed example. A reader skimming would have taken both on trust, and the pilot would have been aimed at the wrong property by the item's own supporting text.

[Copilot]

🟡 Changes recommended

Unresolved review findings include a moderate metadata mismatch and additional checklist, model, and documentation gaps.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (8)

Previously missed (1) — in code that hasn't changed since the last review.

CHECKLIST.md:280

• M30.4's requested re-home is narrower than the references it leaves behind: src/doorbell.rs:107 and sabotage.json:4 also name M31.6, so completing this item as written would leave stale checklist identifiers even if the three design-note references are updated. Include all references in the sweep.

CHECKLIST.md:244

• The wrap-at-8 model is described as reaching the same interleaving and as exhaustive, but the item never requires establishing how that reduced model corresponds to the shipping Balanced implementation. Add an abstraction/refinement criterion, or state that the result is only a counterexample in a toy model; otherwise a passing sabotage run can validate a model that is not evidence about the code.

  window a few instructions wide, and no test can schedule that deliberately. A model whose position
  wraps at 8 makes the whole interleaving reachable in seconds and *exhaustive* rather than sampled,
  and yields a counterexample trace rather than a suspicion.

CHECKLIST.md:188

• The PR metadata calls this Queue M23 and describes M23.4, while the repository changes introduce M30 and M30.4. M23 is already the thread-ambient composite milestone, so please align the title and description with M30 (or renumber the entire change consistently) before merging.

## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked

CHECKLIST.md:267

• There are two copies of this section today: the public README at crates/windows-waitable-queues/README.md:216 and the crate-level docs at crates/windows-waitable-queues/src/lib.rs:167. As written, M30.3 can be completed by updating only one copy and leave the other disclosure stale; require both sites (or make one derive from the other) so the trust boundary is not split.

  Put it where a reader deciding how much to trust the crate will meet it -- beside the existing
  "How far the memory orderings are verified, and how far they are not" section, which is already
  written in the right register.

CHECKLIST.md:280

• Adding M30.4 opens queue-specific work, but crates/windows-waitable-queues/PLANS.md:6-9 still says No checklist is open against this crate. The component tracker now contradicts the root tracker and hides the new commitment; add the workspace checklist there (as the other crates do for root-owned checklists) or explicitly explain why this queue work is excluded.

- [ ] **M30.4** -- Re-home `M31.6`, which is currently orphaned.

  `windows-waitable-queues`' design notes reference `M31.6` in three places as the planned `loom`
  verification, and [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md)
  tells adopters it is planned before 1.0. Until this item, there was no live checklist item for it
  anywhere in the repository -- the crate has only a
  [COMPLETED-CHECKLIST.md](crates/windows-waitable-queues/COMPLETED-CHECKLIST.md). That was the
  "design notes are not a work queue" failure the repository instructions name: a public commitment
  that nothing will cause anyone to pick up.

  Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or
  neither), and make the design-note references point at it.

CHECKLIST.md:256

• A counterexample from the broken variant is necessary but not sufficient to show that the model represents the shipping protocol: an over-permissive or malformed model could also find that trace. Require the unmodified model to satisfy its invariant as well, while retaining the broken-variant counterexample as the anti-vacuity check.

  Success is a counterexample for a deliberately broken variant, not a green run on the correct one.
  A model that cannot produce the known bug when the bug is reintroduced has not been shown to be
  checking anything -- the same sabotage discipline the test suites here already follow.

CHECKLIST.md:294

• Because M30.5 explicitly allows adopting nothing, it must also reconcile the existing public promises that verification is planned before 1.0 (README.md:235-237, src/lib.rs:186-189, and D-31 at DESIGN-NOTES.md:1124-1127). Otherwise a valid no-adoption decision leaves contradictory documentation in place; make that contract sweep part of the item.

  So the decision has to answer: what keeps the model and the code in step, who re-runs it, and what
  happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome -- D-31 reached it
  once already on narrower grounds.

CHECKLIST.md:194

• This adds a multi-paragraph rationale/history block to the active checklist. The repository's checklist hygiene requires CHECKLIST.md to be action-only; move the "why now" and trust-boundary explanation to a design/rationale document (or the PR description), leaving only the milestone's actionable items here. Otherwise this queue becomes a second design record that can drift.

**Why now, and what this is not.** The workspace's concurrency is checked today by reasoning recorded
beside the code, an extensive unit suite, a sabotage suite that injects defects and requires each to
be caught, and a cargo-mutants sweep. That combination has found real bugs --
[D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup
among them. It also has a measured blind spot:

• Files reviewed: 2/2 changed files
• Comments generated: 2
• Review effort level: Lite

[MikeGrier]

Response to review 5216885070 (8 suppressed findings)

All addressed in 68ba242. Three were methodological gaps in the pilot's design and are the ones worth reading about; the rest were scope and hygiene. Every factual claim in the review was verified against the tree before acting, and all eight held.

CHECKLIST.md:244 — the reduced model was never tied to the code

Changed, and this is the sharpest finding of the round. The item asked for a model whose position wraps at 8 without ever requiring anyone to say why that is evidence about a 32-bit field. Shrinking a parameter is itself a claim — that the protocol's correctness does not depend on that width — and if nobody states it, a green run proves something about the model alone.

The item now requires the correspondence in writing: which constants were shrunk, why the protocol is uniform in each, and what a counterexample at 8 implies at 2^32. If that cannot be argued, the result is a counterexample in a toy model and must be reported as exactly that.

What makes this worth more than a wording fix: it is the same trap D-31 already names — stubbing SetEvent verifies a model of SetEvent rather than SetEvent — wearing a second costume. The milestone was built on that objection and then reintroduced it one level down, in its own pilot. The rationale note now names both costumes together.

CHECKLIST.md:256 — the success criterion was half a criterion

Changed. You are right, and the error was an overcorrection of mine. The item said success is a counterexample from a deliberately broken variant and explicitly not a green run on the correct one. But a counterexample from the broken variant can equally come from a malformed or over-permissive model that would find one anywhere — so it is an anti-vacuity check, not a property check.

Both halves are now required: the unmodified model satisfies its invariant, and the broken variant produces a counterexample. Neither alone is evidence.

CHECKLIST.md:294 — "adopt nothing" would recreate the failure M30.4 fixes

Changed. Verified: three public places promise machine-checked verification before 1.0 — README.md, src/lib.rs, and D-31 in the queue's DESIGN-NOTES.md. A no-adoption outcome left as-is would leave the crate promising adopters something no item will deliver, which is precisely the orphaned-commitment failure M30.4 exists to fix, recreated in the same crate by the milestone that fixed it. The sweep is now part of the item whichever way the decision goes.

CHECKLIST.md:280 — the M31.6 sweep was scoped to three of five references

Changed, and counted rather than assumed. M31.6 appears five times across three files: three in DESIGN-NOTES.md, one in src/doorbell.rs, one in sabotage.json. Completing the item as written would have left a stale identifier in a source file and in the sabotage manifest — fix-the-reported-site-not-the-class, written into the item that was supposed to fix a class.

CHECKLIST.md:280 — the component tracker contradicts the root tracker

Changed. Verified: crates/windows-waitable-queues/PLANS.md says "No checklist is open against this crate", which M30.4 falsifies. Adding that row is now part of the item rather than something a future reader has to notice.

CHECKLIST.md:267 — the disclosure has two copies

Changed. Verified: "How far the memory orderings are verified, and how far they are not" exists at README.md:243 and src/lib.rs:194. Updating one would leave the other telling an adopter something the crate no longer believes. The item now requires both — and notes that since the README is already a build input via #[doc = include_str!], deriving one from the other is available and is the option that cannot drift.

CHECKLIST.md:194 — rationale in an action-only file

Changed. Correct per the checklist-hygiene rule, and the reason given in the finding is the right one: left there, the checklist becomes a second design record able to drift from the first — in a milestone whose own M30.5 names drift-between-two-statements as the cost to watch.

Moved to DESIGN-NOTES.md under a new anchored section, with the checklist keeping a one-line pointer. The section explicitly states that no decision is recorded yet, so the absence of one reads as intentional rather than as an omission.

CHECKLIST.md:188 — PR metadata

Already fixed, before this review was submitted. The title and body have said M30 since the previous round, and the body carries a note explaining the renumber. Flagging the timing rather than claiming new work.

---

A note on link checking

This round's edits added cross-references, and one of them would have shipped broken: a link to a design-note anchor that exists only on PR #90's branch, not on this one. It passed a file-existence check and failed an anchor-existence check.

So before committing I checked all 105 relative links in the three root documents for file and anchor resolution. That is the second time in two days an anchor-level check has caught something a file-level check waved through — the same weaker-instrument failure as the M23 collision.

[Copilot]

🔵 Needs a closer look

Resolve the documented tracker, checklist-content, and path inconsistencies before approval.

Review details

Suppressed comments (5)

CHECKLIST.md:287

• This item correctly recognizes that adding M30.4 opens work for the queue crate, but the PR leaves crates/windows-waitable-queues/PLANS.md unchanged and it still says no checklist is open. Update that component tracker to link the root CHECKLIST.md and mark it not started; otherwise the plan indexes disagree and the newly re-homed work remains invisible from the crate.

  Opening queue work also obliges the component tracker:
  [crates/windows-waitable-queues/PLANS.md](crates/windows-waitable-queues/PLANS.md) currently says
  "No checklist is open against this crate", which this item falsifies. Add the row, as other crates
  do for root-owned checklists.

CHECKLIST.md:193

• The new section says its rationale belongs in DESIGN-NOTES.md, but the active checklist then carries explanatory context and revision history around the work items. Checklist files are action-only in this repository; move that rationale/history to the design notes (or remove it) and leave only the executable deliverables and acceptance criteria here.

Why this milestone exists, what it is not, and how it relates to
[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) are recorded in
[DESIGN-NOTES.md](DESIGN-NOTES.md#machine-checking-what-is-argued) rather than here, per the
action-only rule for checklist files.

CHECKLIST.md:306

• These links are resolved relative to the repository-root CHECKLIST.md, so they point to the root README.md and a nonexistent src/lib.rs, not the queue crate files described by this sweep. The item would direct the implementer to update the wrong file and cannot satisfy its own contract sweep; use the crate-qualified paths already used above.

  [README.md](crates/windows-waitable-queues/README.md),
  [src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and D-31 in

PLANS.md:19

• M30.4 is now a live checklist item in this same change, so the current-state clause saying M31.6 exists only in design notes with no live checklist item is false after merge. Describe it as previously untracked and identify that it is now queued as M30.4, otherwise the tracker reports the wrong state.

| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; M30 has no decision recorded yet, which is the point of M30.5 |

PLANS.md:19

• The M30 rationale now exists at DESIGN-NOTES.md#machine-checking-what-is-argued, but the Design Notes cell still links only to the M19-M22 anchor. Saying that M30 has no decision is accurate because M30.5 is pending; it does not explain where the current rationale lives. Add the M30 anchor, and change the tracker text to say the obligation has no live checklist item rather than that it exists only in design notes, since M30.4 itself documents source/manifest references.

| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; M30 has no decision recorded yet, which is the point of M30.5 |

• Files reviewed: 3/3 changed files
• Comments generated: 0 new
• Review effort level: Lite

[MikeGrier]

Response to this round (5 suppressed findings)

Four held and are fixed in 08cab0f. One does not, and I want to show the check rather than just disagree.

CHECKLIST.md:287 — do the tracker update, don't queue it

Changed, and you are right that the previous round got this wrong. I made updating crates/windows-waitable-queues/PLANS.md part of M30.4 instead of doing it. That is the same error M30.4's own text had one round earlier: the statement "No checklist is open against this crate" stops being true when the work is queued, not when it is completed. Deferring the fix to the item that creates the contradiction leaves the contradiction live for however long the item sits.

The row is added here, with the format taken from the four other crates that already index root-owned checklists. What M30.4 retains is keeping it accurate as the work proceeds.

CHECKLIST.md:193 — the history stayed behind

Changed, and this is a fair hit on last round's fix. Moving the milestone's rationale out left two "an earlier version of this item said..." paragraphs inside the items — the untestability mis-attribution and the half-criterion. That is still history in an action-only file, and the pointer paragraph I added made it look addressed, which is worse than not having moved anything.

Both are now in the DESIGN-NOTES.md section, under a heading that says why they are worth keeping at all: each was an error in the argument for the pilot rather than in the plan, so a reader taking them on trust would have aimed the pilot wrongly. The checklist keeps only the actionable residue — that capacity == 1 is not a candidate, and why.

PLANS.md:19 (both findings) — the row described a state this change ends

Changed. The row said M31.6 "currently exists only in design notes with no live checklist item", which this change falsifies twice: it is queued as M30.4, and the references were never only in design notes — one is in src/doorbell.rs and one in sabotage.json. Reworded to the past tense with the current location.

The Design Notes cell now also links DESIGN-NOTES.md#machine-checking-what-is-argued. The anchor existed after last round but nothing in the tracker reached it, so a reader following the plan index could not find M30's rationale — which is exactly what moving it out of the checklist was supposed to enable.

CHECKLIST.md:306 — declined, and here is the check

The finding says these three links resolve to the repository root rather than to the crate. They do not. The targets are:

crates/windows-waitable-queues/README.md
crates/windows-waitable-queues/src/lib.rs
crates/windows-waitable-queues/DESIGN-NOTES.md

All three resolve. What reads as a bare filename is the link text, not the target — and the repository convention is that link text is normally the document's file name, with any disambiguating qualifier as prose outside the link.

I verified rather than asserted this: every relative link in all four changed files, resolved from its own file's directory (which also exercises the crate PLANS.md's ../../ targets) — 115 links, 0 broken.

But the instinct is worth acting on, so I have. A bare README.md inside a root-level checklist genuinely does read as the root README, and this workspace has several. The link text is now qualified — "that crate's README.md", "its src/lib.rs" — at all five such sites. The finding's conclusion was wrong; the ambiguity it noticed was real.

---

What the round taught

Both real findings were defects in the previous round's fix, not in the original work. Deferring the tracker update to the item that creates the contradiction, and moving rationale out while leaving history behind, are the same shape: a fix that addresses the reported symptom and leaves the property it was supposed to establish still false. Worth watching for specifically in rounds that follow a round — the fix is newer than everything around it and gets less scrutiny for being fresh.

[Copilot]

🟡 Changes recommended

Unresolved checklist and planning consistency issues remain, including one moderate finding.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (4)

Previously missed (1) — in code that hasn't changed since the last review.

CHECKLIST.md:257

• #[doc = include_str!("../README.md")] only feeds the separate ReadmeDoctests item; it does not supply the crate-level section at src/lib.rs:167. Thus the proposed "make one derive" option is not available with the current mechanism, and choosing it as written would still leave the two disclosures able to drift. Either require both copies to be updated or first introduce a shared/generated fragment.

CHECKLIST.md:193

• The new section says the checklist is action-only and that rationale belongs in DESIGN-NOTES, but this milestone then embeds extensive historical rationale, model-selection argument, and drafting corrections in the checklist itself. That creates a second source of design context for future edits and conflicts with the repository's action-only checklist convention; keep the checklist to deliverables and acceptance criteria, and move the explanatory material to the design note.

Why this milestone exists, what it is not, and how it relates to
[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) are recorded in
[DESIGN-NOTES.md](DESIGN-NOTES.md#machine-checking-what-is-argued) rather than here, per the
action-only rule for checklist files.

DESIGN-NOTES.md:1895

• D-31's limitation is stated here as if every candidate model checker "covers atomics", but M30.1 explicitly includes TLA+/PlusCal, which has no Rust/C11 memory model and therefore does not cover atomics in that sense. The tool-independent point is only that the real SetEvent/ResetEvent calls are not modeled; qualify the atomic-coverage claim so the new survey does not start from a false premise.

[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31)**, which decided on considered grounds
that 0.1.0 ships without machine-checked orderings. D-31's reasoning is the starting point rather
than something to overturn, and its central objection survives any tool choice: a model checker
covers atomics and cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of
`SetEvent` rather than `SetEvent` itself. That is the "measures the model, not the thing" trap this

DESIGN-NOTES.md:1866

• This new section explicitly says no decision is recorded and then preserves drafting history in “Two corrections the milestone's own drafting needed.” DESIGN-NOTES.md is the current-decision tier; this queued rationale and historical record belong in the root DESIGN-RATIONALE.md or a design session, with only a pointer here if needed. Otherwise readers can mistake pre-decision context for an adopted contract before M30.5 runs.

## <a id="machine-checking-what-is-argued"></a>Machine-checking what is currently argued: why M30 exists and what it is not

Context for [CHECKLIST.md](CHECKLIST.md) -> `M30`. It lives here rather than in the checklist
because a checklist is an action queue, and this is rationale.

• Files reviewed: 4/4 changed files
• Comments generated: 1
• Review effort level: Lite

[MikeGrier]

Response to review 5217046983 (4 suppressed + 1 inline)

All five addressed in 601f98d. Two were claims I made about mechanisms without checking them, which is the part worth reading.

DESIGN-NOTES.md:1866 — pre-decision context in the current-decision tier

Changed. Correct, and the consequence you name is the right one: no decision has been taken — M30.5 produces it, and "adopt nothing" is a legitimate result — so queued context sitting in Tier 1 can be read as an adopted contract.

Moved wholesale to DESIGN-RATIONALE.md, which already exists at the root with design-sessions/ beside it, so the three-tier scheme was live and I simply used the wrong tier. DESIGN-NOTES.md is now back to its pre-M30 state — the diff is a pure removal with no additions, which I checked rather than assumed.

This is the second move for this material: checklist → Tier 1 → Tier 2. The first move was right that it did not belong in an action queue and wrong about where it went instead.

CHECKLIST.md:193 — the rationale left behind was the argument, not just the framing

Changed. Fair, and the distinction matters: last round I moved the framing paragraphs but left M30.1's tool taxonomy and M30.2's candidate argument, which are model-selection rationale. Leaving them made the checklist a second source of design context able to drift from the first — in a milestone whose own M30.5 names precisely that drift as the cost to watch.

M30.1 and M30.2 are now deliverables plus numbered done-when criteria. The acceptance criteria stay (they instruct); everything that argues is in Tier 2.

CHECKLIST.md:257 — "make one derive" is not available

Changed, and you are right on the mechanism. I checked it this time rather than reasoning from the existence of an include_str!:

#[cfg(all(doctest, windows))]
#[doc = include_str!("../README.md")]
struct ReadmeDoctests;

That is cfg(doctest) on a private item — it compiles the README's code as doctests and does not render its prose into the crate documentation. So the derivation I offered as "the option that cannot drift" does not exist, and choosing it would have left both copies able to drift while looking addressed, which is worse than not offering it.

The item now requires both copies, and states what making one derive would actually cost: a shared fragment both include, which is separate work.

DESIGN-NOTES.md:1895 — "a model checker covers atomics" is false for TLA+

Changed, and this one is the most embarrassing of the round. TLA+'s actions are atomic by construction and it has no memory model to cover atomics with — a point I had stated correctly elsewhere before writing the opposite into the note.

It matters beyond accuracy: TLA+ is the first tool class M30.1 surveys, so the survey would have started from a false premise about its own leading candidate, and the premise flattered it. The tool-independent part of D-31's objection is only the syscall boundary — no candidate models the real SetEvent/ResetEvent. How much of the atomics a given tool sees is exactly what M30.1 exists to determine, so asserting it in advance pre-empted the survey.

crates/windows-waitable-queues/PLANS.md:8 — a tracker that weakens an obligation

Changed. The checklist says either outcome obliges the contract sweep; the tracker said "may also oblige". A tracker that softens a required follow-up can be read as complete without it. Corrected to match — and it is worth noting the two were written minutes apart in the same commit, which is restatement drift at the shortest range I have seen it.

---

What the round taught

Repointing the rationale obliged more than the files the review named. Both PLANS.md rows cited the old DESIGN-NOTES anchor and would have broken on the move. Found by sweeping the anchor rather than by editing the named files — and then all 121 relative links across the five changed files were verified for file and anchor resolution.

Both mechanism findings were things I asserted from plausibility. "The README is a build input, so deriving is available" and "a model checker covers atomics" were each one check away from being known false, and I did not make the check because both sounded right. The rule I keep re-learning is narrower than "verify by execution": it is that a claim about how a mechanism works is exactly where plausibility is least reliable.

[Copilot]

🟡 Changes recommended

Review comments identify one moderate issue and seven nits requiring documentation, attribution, modeling-scope, and tracker updates.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (6)

CHECKLIST.md:194

• CHECKLIST.md is intended to be an action-only queue, but this milestone adds a large second copy of the rationale, tool survey, drafting history, and explanatory context that already lives in DESIGN-RATIONALE.md. Keeping these parallel narratives will make the active queue harder to scan and creates another place for the contract to drift. Please reduce the checklist to the actionable items and concise acceptance criteria, leaving the rationale in the linked Tier 2 document.

Rationale -- why this milestone exists, which tool classes are in scope and what each can see, why
`SH-14.1` is the pilot, and how this relates to
[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) -- is in
[DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued). No decision is recorded
yet; `M30.5` produces it.

CHECKLIST.md:254

• D-31 establishes the release timing and the limits of model checking, but it does not define the "both MPSC shapes or neither" scope stated here. That coverage obligation is recorded under D-29 (including the M31.6 paragraph), so citing only D-31 points implementers to the wrong decision for this acceptance criterion. Link D-29 here as the decision that owns the shape-coverage requirement.

  Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or
  neither), and repoint every reference at it. **There are five, not three**: three in

CHECKLIST.md:229

• The proposed “could not reach” list preclassifies every scheduler-dependent property as outside the pilot, but loom is specifically intended to explore scheduler interleavings, and the pilot rationale says the reduced model makes the stalled-producer interleaving exhaustive. Limit this to scheduler or environment behavior the selected tool cannot model (such as OS fairness or real-time timing), otherwise M30.3 can record a false gap.

  This is the item the milestone exists for. Expect the list to include: the memory orderings, if the
  tool has no memory model; every syscall boundary, including the doorbell's; anything whose
  correctness depends on the allocator, the scheduler, or real time; and the gap between the model
  and the code, which no tool closes.

DESIGN-RATIONALE.md:254

• loom does not execute the shipping std atomics or the Windows calls as written; synchronization must be replaced with loom's instrumented types and the resulting model is explored systematically. Calling this “actual Rust under the C11 memory model” overstates the guarantee and blurs the model/code gap that M30.2 and M30.3 require you to record. Describe it as an instrumented code-level model instead.

- **loom** -- actual Rust under the C11 memory model, which is exactly where the measured
  weakened-`Acquire` blind spot lives.

crates/windows-waitable-queues/PLANS.md:8

• This tracker repeats the same incorrect attribution: D-31 does not define the "both MPSC shapes or neither" scope; D-29 does. Retain D-31 if it is needed for the release-timing decision, but also link D-29 for the shape-coverage requirement so the component tracker leads to the design decision that actually owns it.

| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-31](DESIGN-NOTES.md#d-31) describes it -- both MPSC shapes or neither -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued) |

crates/windows-waitable-queues/PLANS.md:8

• The root PLANS.md identifies itself as the master tracker and enumerates the per-source-component PLANS.md files, but it still omits this newly active windows-waitable-queues tracker. Add this tracker to the root inventory so the row added here is discoverable from the master navigation.

| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-31](DESIGN-NOTES.md#d-31) describes it -- both MPSC shapes or neither -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued) |

• Files reviewed: 4/4 changed files
• Comments generated: 1
• Review effort level: Lite

[MikeGrier]

Response to review 5217404270 (6 suppressed + 1 inline)

All seven addressed in b1691ee. Two were wrong attributions, two overstated what a tool can see, and one was a trim I did by halves last round.

CHECKLIST.md:254 and PLANS.md:8 — the shape scope is D-29's, not D-31's

Changed at both sites, verified rather than taken. I located the sentence and walked back to its owning heading: "M31.6's loom verification covers both shapes or neither is verified" sits under D-29, in its "The obligation this creates" section. D-31 owns only the release timing — that verification gates 1.0 rather than 0.1.0.

This is worse than a mis-link because of where it sat: it was the acceptance criterion for M30.4, so an implementer following the citation would have opened the wrong decision precisely when trying to determine what "done" means. Both sites now cite D-29 for the scope and keep D-31 for the timing.

DESIGN-RATIONALE.md:254 — "actual Rust under the C11 memory model" overstates loom

Changed. You are right: loom runs the crate's logic, but the synchronization primitives must be substituted for loom's instrumented types, and the Windows calls are not executed as written. It is an instrumented code-level model.

What makes this more than imprecision: the overstatement undercut two items in its own milestone. M30.2's refinement criterion and M30.3's could-not-reach list both exist to record the model-to-code gap — and this line told a reader there wasn't one for loom.

Inline, DESIGN-RATIONALE.md:252 — "no memory model at all" is too absolute

Changed, and this is a correction to last round's correction. Last round I fixed the opposite error ("a model checker covers atomics") and overshot into a flat "TLA+ has no memory model at all".

The precise statement is narrower: TLA+ has no built-in hardware memory model, and its ordinary interleaved-action semantics is sequentially consistent — but a specification can model weak-memory reordering explicitly, with store buffers or a reordering relation written in. What it checks then is the modelled protocol rather than the emitted code, so the model-to-code gap survives either way.

Worth stating exactly because M30.1 uses this distinction to decide what the survey can cover, and a flat "no memory model" would have ruled out a legitimate approach before the survey began.

CHECKLIST.md:229 — preclassifying scheduler-dependence as unreachable

Changed. Sharp catch. loom explores scheduler interleavings deliberately, so listing "anything whose correctness depends on the scheduler" as out of reach would have recorded a false gap in the item whose entire output is the gap list. It now scopes the list to what the selected tool cannot model, and says that explicitly so a later reader does not re-introduce the general form.

CHECKLIST.md:194 — the trim was done by halves

Changed. Fair. Last round I trimmed M30.1 and M30.2 to deliverables plus done-when criteria and left M30.3, M30.4 and M30.5 carrying their full rationale — which made the checklist look action-only while three of five items were not. All five are now deliverables plus numbered done-when criteria.

PLANS.md:8 — the root inventory omitted the queue tracker

Changed, and sweeping it found a second omission you did not report. Rather than adding the named entry, I diffed the inventory against git ls-files '*/PLANS.md': 12 listed, 13 on disk. The other missing one was crates/windows-file-watcher-example-test-harness/PLANS.md — a pre-existing gap unrelated to this PR.

Both added; the inventory now lists 13 of 13, and the check that proves it is a set difference rather than a reading.

---

What the round taught

Two findings were errors in acceptance criteria, which is the worst place for them. The D-31/D-29 misattribution and the scheduler preclassification both sat in "done when" text — so each would have been consulted precisely by someone trying to determine whether the work was finished, and each would have sent them somewhere wrong. Rationale that is wrong misleads a reader; an acceptance criterion that is wrong misleads the implementer at the moment of decision.

All 123 relative links across the five changed files verified for file and anchor resolution.

[Copilot]

🔵 Needs a closer look

CHECKLIST.md has an unresolved moderate pilot-model contradiction and two additional alignment/wording findings.

Review details

Suppressed comments (3)

Previously missed (1) — in code that hasn't changed since the last review.

CHECKLIST.md:219

• The pilot is motivated by the stalled-producer overwrite, but SH-14.1 is already the shipping reserving_mpsc protocol's documented ABA defect: a producer can resume after a full claim-position wrap and overwrite a live slot. A faithful reduced model whose position wraps at 8 should therefore produce a counterexample in the unmodified variant, so requiring that variant to satisfy its invariant while only a deliberately broken variant fails is contradictory. Define a corrected reference model and its refinement to shipping code, or make the known unmodified counterexample the property result.

CHECKLIST.md:230

• The comma after doorbell's breaks the possessive phrase and makes this acceptance criterion grammatically incorrect; it should read the doorbell's real-time behaviour.

     Expect the syscall boundary including the doorbell's, real-time behaviour, and the model-to-code

CHECKLIST.md:219

• The PR description currently says pilot success is a counterexample from a deliberately broken variant rather than a green run of the correct model, but this checklist now requires both the unmodified-model property check and the broken-variant anti-vacuity check, explicitly saying neither alone is sufficient. Please align the description with this acceptance criterion (or change the checklist), so the advertised deliverable does not contradict the queued work.

  2. **The unmodified model satisfies its invariant** -- the property check.
  3. **A deliberately broken variant produces a counterexample** -- the anti-vacuity check. Neither
     2 nor 3 alone is sufficient.

• Files reviewed: 4/4 changed files
• Comments generated: 0 new
• Review effort level: Lite

[MikeGrier]

Response to this round (3 suppressed findings)

All three addressed in 8322487, plus the PR description. The first is the best finding this PR has had, and it was a logical contradiction rather than a wording problem.

CHECKLIST.md:219 — the success criterion was inverted

Changed, and you are exactly right. I verified the premise before acting: SH-14.1 is a live defect in the shipping protocol, described in reserving_mpsc's own rustdoc — a producer that resumes after a full wrap claims against a numerically identical but generations-later position and writes into a slot whose emptiness was decided long ago — and disclosed to adopters in the README.

So a faithful model of that protocol, at a position width small enough to wrap, must find it. "The unmodified model satisfies its invariant" could only be satisfied by a model that does not reproduce something this crate ships and documents.

The criterion was therefore backwards: it would have been failed by a correct model and passed by one that quietly failed to model the hazard — in a pilot whose entire purpose is to produce that counterexample.

Both checks survive, but they attach to configurations rather than to modified and unmodified code:

check	configuration	required result
faithfulness	wrap reachable, producer able to stall across it	reproduces SH-14.1 — otherwise the model is not modelling this protocol
anti-vacuity	wrap unreachable: pushes bounded below it, or one producer (no race to lose)	green — otherwise the model is over-permissive and the counterexample above proved nothing

The general form is now in the rationale, because it is not specific to this pilot: when the system being modelled has a known defect, a green run on the unmodified model is a failure signal, not a success.

Worth noting this is the second correction to the same criterion. The first replaced "counterexample only, never a green run" with "both halves" — right about vacuity, wrong about which artefact each half attaches to. Two rounds to get one criterion right, and the second error was subtler than the first because it looked like rigour.

CHECKLIST.md:230 — the elliptical possessive

Changed. The comma did break it. I have also taken the opportunity to fix the underlying imprecision rather than just the punctuation: your suggested reading, "the doorbell's real-time behaviour", would be wrong on the substance — the doorbell is a syscall boundary concern (SetEvent/ResetEvent), not a real-time one. The list now names the syscall boundary including the doorbell's SetEvent/ResetEvent, and keeps real-time behaviour as its own separate entry.

CHECKLIST.md:219 (second) — the PR description contradicted the checklist

Changed. Correct, and it now carries the corrected three-way criterion rather than the superseded one.

This is the third round in this PR where a corrected claim survived only in the PR description. It restates the work like any other document, so it rots the same way — but it is not a file in the tree, so no sweep, grep, or CI check can reach it. I have added checking it to what I do when answering a round; this round it was caught by the reviewer first, which is the wrong order.

---

What the round taught

The first finding is one no sweep would have found, and that is the interesting part. It was not a restatement, not a stale figure, not a broken link. It was two statements that were each locally reasonable — "SH-14.1 is a live defect we disclose" and "the unmodified model must satisfy its invariant" — held in different documents, whose conjunction is a contradiction.

That is a class my instruments do not cover: consistency between a plan and the facts it plans against. Grep finds repeated text; nothing finds a criterion that quietly assumes the opposite of what the crate documents three files away.

[Copilot]

🟡 Changes recommended

Unresolved moderate checklist and tracker issues must be addressed before approval.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (3)

CHECKLIST.md:280

• The item heading and PR scope require the adoption decision to state its cost, but the completion criteria only require the model/code maintenance answers and a contract sweep. A future completion can therefore satisfy M30.5 while omitting the runtime, tooling, or maintenance cost that this milestone is explicitly meant to surface; add that as a required criterion.

  1. **The decision answers three questions**: what keeps the model and the code in step, who
     re-runs it, and what happens when they disagree. "Adopt nothing, and say why" is a legitimate
     outcome.

CHECKLIST.md:233

• This is historical drafting context, not an action or completion criterion, and the correction is already recorded in DESIGN-RATIONALE.md. Remove it from the active checklist (leaving the explicit scope exclusion below) so CHECKLIST.md remains action-only.

  An earlier version of this item asked for (2) and (3) the other way round: the unmodified model to
  satisfy its invariant, and only a deliberately broken variant to fail. That could only be satisfied
  by a model that does *not* reproduce a defect this crate ships and documents.

PLANS.md:21

• The Design Notes column is now populated with a Tier 2 DESIGN-RATIONALE.md link for M30, but this tracker’s schema reserves that column for DESIGN-NOTES.md paths or N/A. Keep the M30 rationale link in the description and mark the M30 design-note portion N/A; otherwise tools/readers treating the column as a decision-note index will misclassify the rationale as a current design decision.

| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0: it was previously untracked, referenced from that crate's design notes, a source file and its sabotage manifest with no live checklist item anywhere, and is now queued as M30.4. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued) for M30's rationale (Tier 2, since no decision is taken yet) -- its decision is not recorded yet, which is what M30.5 produces |

• Files reviewed: 4/4 changed files
• Comments generated: 1
• Review effort level: Lite

[MikeGrier]

Response to review 5217500490 (3 suppressed + 1 inline)

All four addressed in 3c7e1c8.

CHECKLIST.md:280 — the criteria did not cover the item's own deliverable

Changed, and this is the sharpest of the round. M30.5's heading says "record the decision with its cost", and its done-when criteria asked only for the model/code maintenance answers and the contract sweep. A completion could have satisfied every criterion while omitting the cost entirely.

That is a specific and nasty shape: acceptance criteria that do not cover the item's own stated deliverable. The criteria look complete, they are checkable, and they quietly permit skipping the thing the item was written for.

Cost is now criterion 1, and it names what cost means here rather than leaving it to judgement: wall-clock and whose time, tooling added and who maintains it, and the standing cost this workspace already knows it pays — a specification is a second statement of the contract and can drift from the code with nothing to detect it, so a stale model that still passes is worse than no model. That paragraph previously sat in the item as prose; it belongs as a criterion, which is also where the action-only rule wants it.

CHECKLIST.md:233 and the inline at :194 — explanatory prose, again

Both changed. The drafting-history paragraph is gone, and the rationale pointer is now one line rather than five describing what the rationale contains.

Worth naming as a pattern rather than fixing quietly: this is the third round in which explanatory prose has had to be removed from this milestone. The mechanism is consistent — each correction I make arrives with its own justification attached, and I attach it where the correction happened. The justification belongs in Tier 2; only the work and its acceptance criteria belong beside the work.

PLANS.md:21 — a Tier 2 link in a column reserved for Tier 1

Changed in both trackers. Verified against the convention, which reads: "Design Notes column: Path(s) to DESIGN-NOTES.md file(s) that document the work, or 'N/A' if none exist."

Your reasoning for why it matters is the right one, and it is the same reason the rationale was moved out of DESIGN-NOTES.md two rounds ago: a Tier 2 link in a decision-note column invites a reader to take pre-decision rationale for a recorded decision. Fixing one placement while recreating the same misclassification one column over would have been no fix at all. The rationale link moves into the description; the column reads N/A for M30.

---

One thing I found and deliberately did not change

Sweeping the column rather than fixing the named row turned up two rows that predate this branch and also diverge from that convention: the root tracker cites mutation-sweeps/2026-09-02/README.md, and windows-platform-probes' tracker cites its own DESIGN-RATIONALE.md.

They are outside this PR's scope, and I do not think the right move is obvious: two independent authors reaching for a non-DESIGN-NOTES.md link in that column may mean the convention wants widening rather than the rows narrowing. Raising it rather than silently changing other people's rows, or pretending the sweep found nothing.

@MikeGrier — worth a decision at some point: should that column accept Tier 2 and other supporting documents, or stay strictly Tier 1?

[Copilot]

🔵 Needs a closer look

The loom implementation is not kept as a live obligation, and related checklist and documentation issues remain.

Review details

Suppressed comments (6)

Previously missed (1) — in code that hasn't changed since the last review.

CHECKLIST.md:253

• M30.4's completion criteria only rename/repoint the existing commitment; they never require implementing the loom verification itself. After this item is checked and the M30 group is archived, the both-MPSC-shapes verification will again have no live work item, recreating the orphan this milestone is meant to fix. Keep a separate unchecked item for the actual verification (or make M30.4's acceptance criteria cover its implementation), and use a separate bookkeeping step for the five reference updates.

CHECKLIST.md:257

• The repository text here assigns the both-shapes scope to D-29, but the PR description still says that scope comes from D-31. D-31's decision governs the 0.1.0-versus-1.0 timing (and disclosure), while D-29 is the both-MPSC-shapes decision; please update the PR description so the stated rationale and tracker do not disagree.

  1. **It has a live item in a live checklist**, scoped as
     [D-29](crates/windows-waitable-queues/DESIGN-NOTES.md#d-29) requires -- the loom verification
     covers both MPSC shapes or neither is verified. (D-29 owns that obligation;
     [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) owns only the release timing, that
     verification gates 1.0 rather than 0.1.0.)

CHECKLIST.md:231

• This reintroduces milestone rationale into the active checklist: the reason M30.3 is the milestone's deliverable already belongs in DESIGN-RATIONALE.md. Keep this item action-only so the checklist does not accumulate explanatory prose.

- [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. This is the item the milestone
  exists for.

CHECKLIST.md:211

• This four-line explanation is rationale for the pilot rather than an action or completion criterion, and it duplicates the Tier 2 discussion in DESIGN-RATIONALE.md. Remove it from the action-only checklist and keep the explanation in the rationale.

  **`SH-14.1` is a live defect in the shipping protocol, not a hypothetical**, and that inverts the
  usual shape of a success criterion. A faithful model of the shipping claim protocol, at a position
  width small enough to wrap, *must* find it. A green run on that model is therefore evidence the
  model is **unfaithful**, not evidence the protocol is sound.

crates/windows-waitable-queues/PLANS.md:8

• This component tracker likewise tracks only M30.4's re-homing/bookkeeping, not execution of the loom verification for both MPSC shapes. Once the referenced root item is completed, this row will no longer expose that future obligation; add a separate live implementation item/row or make the re-homing item remain open until verification is delivered.

| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-29](DESIGN-NOTES.md#d-29) requires -- both MPSC shapes or neither, which is D-29's obligation rather than [D-31](DESIGN-NOTES.md#d-31)'s; D-31 owns only the release timing -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. The milestone's rationale is in [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued), Tier 2, because no decision is taken yet. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-29), [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31) |

crates/windows-waitable-queues/PLANS.md:8

• The new tracker row refers to the repository document as plain text in its README promises adopters before 1.0. Project-document references are required to be clickable in these trackers; use a relative [README.md](README.md) link so this promise is navigable.

| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-29](DESIGN-NOTES.md#d-29) requires -- both MPSC shapes or neither, which is D-29's obligation rather than [D-31](DESIGN-NOTES.md#d-31)'s; D-31 owns only the release timing -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. The milestone's rationale is in [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued), Tier 2, because no decision is taken yet. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-29), [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31) |

• Files reviewed: 4/4 changed files
• Comments generated: 0 new
• Review effort level: Lite