[JacobStephens2]

Summary

tests/pickup_model.rs                  # bounded Stateright protocol exploration
.agents/skills/
  verify-pickup/                       # rerun, coverage, request mapping, sync
  create-formal-verification-skill/     # imported Cursor pstack skill + MIT license
  maintain-formal-verification-skill/   # imported upkeep + MIT license

Models Pickup selection, origin reservation, Ready/Claim-history recheck, dispatch, Claim make/ending, reservation release, crashes and Day shift recovery. Stateright 0.31.0 is pinned as a dev dependency and runs in the existing Rust CI job. Product code is unchanged.

What holds: no two Runs or Spec runs complete Claim handling from the same Ready selection generation within the model's bounds. What fails: the literal dispatch promise has a pre-Claim counterexample, retained as an executable assertion and a counterexample regression. A green CI run does not prove the literal promise.

Bounds: three hosts, one issue, one attempt per host, at most three Claim applications; unique tokens; linearizable labels/origin requests; complete history within one page; other Ready gates fixed favorable. The Day shift confirms work stopped before hand-back or stale-reservation deletion. This is bounded exploration, not a proof for arbitrary host counts. Worktree disposal, Self-merge, direct Issue URL commands/other Pass writers, Stop/Sweep policies, pagination/consistency behavior and liveness remain outside it.

Test seams: Stateright's public Model/Checker interface over GitHub label requests and origin reservation requests. Local dispatch/crash markers remain separate so they cannot hide interleavings between requests.

Closes #881

Evidence

• Before (broken Claim-count recheck): removing the selected/current count comparison produces a 19-step counterexample: A dispatches generation 0 and makes its Claim; B had already selected generation 0; A ends and releases its reservation; the Day shift hands back; B reserves, refreshes without comparing counts, dispatches and completes Claim handling on its stale selection.
• Before (broken empty lease): unconditional reservation creation produces a 15-step counterexample: B replaces A's reservation; both refresh before A's Claim write; both dispatch and complete Claim handling because an existing Claim is accepted.
• After (real safeguards): cargo test --locked --test pickup_model -- --nocapture passes: 4 tests, 1 intentionally ignored assertion; 70,197 states for claimed-dispatch safety plus reachable crash recovery, failed-winner requeue and Day shift hand-back. Final focused execution: 1.37s. cargo check --tests --locked and cargo clippy --all-targets --locked -- -D warnings pass.
• Literal-property finding: A selects/reserves/refreshes, dispatches, fails before making a Claim and releases its reservation. B dispatches the same unchanged Ready generation. The explicit current assertion exits 101 with a 14-step counterexample. The property/model are retained; the normal suite records its discovery rather than asserting that it holds.

Reproduce each red assertion (expected exit 101):

cargo test --locked --test pickup_model assert_requested_property -- --ignored --exact --nocapture
PICKUP_MODEL_VARIANT=no-claim-count cargo test --locked --test pickup_model assert_requested_property -- --ignored --exact --nocapture
PICKUP_MODEL_VARIANT=no-empty-lease cargo test --locked --test pickup_model assert_requested_property -- --ignored --exact --nocapture

The two mutation commands assert claimed-dispatch safety so the known pre-Claim finding cannot mask safeguard sensitivity. All three commands were run and failed with their documented counterexamples.

Full-suite validation: CI's Rust job passed cargo test, formatting and Clippy for exact final head b93e63a17f9fa517f0753f4c4e1a918c168cc656 (job execution 10m39s, including compilation). All applicable CI and release-smoke checks passed.

Local /usr/bin/time -p scripts/affected-tests main selected the full Nextest suite. Per docs/testing.md's instruction to reuse successful CI for the exact head, that redundant local run was stopped after CI passed: 1,032 tests passed before interruption, four running cases received SIGINT, 1,210 were not run and 51 were skipped. Partial local wall time was 1,105.87s including 82s compilation; this is not claimed as a completed local full-suite pass. The final model target and all-target Clippy were separately rerun successfully after review edits.

Review coverage

Independent thirdshift-code-review axes used main (25ec54b) as the fixed point. Standards: two findings addressed (user-invoked descriptions and explicit promise enum), no unresolved findings. Spec: no actionable findings. Both axes read all nine changed files, including Cargo.lock and licenses. Generated exclusions: none. Changed files left unread: none.

Unaddressed findings

Standards

None; both review findings were addressed in b93e63a.

Spec

The existing literal dispatch counterexample remains unfixed in product code, tracked in #1068 with only needs-triage and no blocking links. Issue #881's acceptance criterion requires reporting a current-protocol counterexample while preserving the model/property, and its scope explicitly excludes any product-code changes. The explicit assertion above (exit 101 at final head b93e63a) and pass::dispatch calling Run startup before the Claim provide the evidence; the Day shift must decide the resulting product change or a deliberate change to the promise. This trace demonstrates two dispatches, without demonstrating simultaneous implementation sessions.

Security

None.

Security review outcome

No unaddressed introduced findings.

Merge Danger

Door: two-way

Revert the dev dependency, model and repository skills. No product behavior or stored data changes.

Blast Radius: verification

Adds roughly one second of model exploration to the Rust tests. A passing bounded model is evidence only under the recorded assumptions; the known literal-property failure is disclosed above.

Built with codex · gpt-6.1-sol · xhigh