work-queue/

---

title: Work Queue protocol model description: TLA+ model, safety proof argument, and bounded verification for the work queue.

Work Queue protocol model

The current design is the mandatory priority/fairness DAG protocol: one causal QueueCommit log, exact native Go/JavaScript scheduling conformance, immutable Claim arrays, verified Work Results and typed Issue/PR observations. Its implementation coverage table tracks unfinished runtime/verification work and user-deferred writer-restriction enforcement. Do not infer deployment-security completion from functional tests.

The original WorkQueue.tla is retained as historical model evidence for issue #64852. Its best-effort oldest-first selection, competing Claim arbitration and scalar worker behavior do not describe the new current protocol.

The design rationale and trade-offs are recorded in ADR-64955.

Current operator interface

The current operator commands and keyboard browser are documented in the queue reference. Policy installation is documented in the deployment guide. This directory retains executable specifications and formal evidence, not a second current user guide. The historical material below is model provenance, not supported deployment guidance.

Local stress simulator

Run the simulator from the repository root with Node.js 24 or later and Git. It uses temporary local Git repositories, concurrent worker threads and a simulated GitHub Git/Actions API; it does not contact GitHub or need credentials.

node --test .github/scripts/work-queue-stress.test.cjs
node .github/scripts/work-queue-stress.cjs --mode history --items 100000 --workers 2
node .github/scripts/work-queue-stress.cjs --items 1024 --workers 4 --queue-items 64 --seed 7
node .github/scripts/work-queue-stress.cjs --mode saturation --items 100000 --workers 4

The history profile counts retained Work plus Claim items, not successful worker completions. The lifecycle profile submits, grants, launches simulated original native runs, finishes Claims, verifies no-op delivery receipts and releases reservations. Its total workload is explicitly divided into bounded queue branches; --items 100000 is a long-running aggregate workload, not a promise that one queue admits 100,000 pending Work items. The saturation profile instead reports the first real admission refusal, accepted batch count and unattempted remainder without fabricating Claims or completions.

Seeded faults force competing real Git reference updates and lose one successful publication response. JSON diagnostics report CAS conflicts, recovered requests, native POST counts, ledger bytes, cold replay timings, memory and workload scope. Workers have bounded deadlines and fixtures are cleaned up on completion or failure. Canonicalization must preserve the complete causal history and projection.

The separate Work Queue Stress workflow runs on pull requests and main pushes changing actions/setup/js JavaScript, the simulator, its workflow or protocol fixtures. It runs the 100,000-item history profile, 1,024 live lifecycles and admission saturation independently. Its step summary reports profile outcomes, measured workload, elapsed time, throughput and peak memory, with phase timings and Git contention in a collapsible section. History validation throughput is separate from live Work completion throughput; failed or skipped profiles never imply successful completion. The summary and JSON diagnostics are uploaded even on failure. It uses read-only checkout credentials and does not dispatch actual GitHub workflow runs.

Render saved JSON diagnostics locally with node .github/scripts/work-queue-stress-summary.cjs stress-results. The command writes stress-results/summary.md and appends the same report to GITHUB_STEP_SUMMARY when that environment variable is set.

Runtime scaling and compaction

The JavaScript replay maintains private indexes for available Work, unfinished delivery barriers, open Claims, native reservations, graph membership and original run bindings. Scheduling copies only unfinished Work, its direct predecessors and held reservations, rather than cloning the entire ledger. Graph admission checks new nodes against indexed accepted graphs and traverses new edges iteratively. These indexes are derived from validated commits, never stored as authority. Detached public projections rebuild indexes when used again, so caller mutation cannot leave a stale scheduling cache.

The Git store parses and replays a read once, validates an appended candidate once, and serializes that checked history without another replay. Custom candidate generators still receive isolated copies. Multi-MiB base64 blobs use linear validation rather than a repeated-quartet regular expression that can overflow the JavaScript engine's stack.

Compaction remains canonical ordering and identical-commit deduplication only. It does not erase terminal Work, historical Claims, request identities, FIFO positions or scheduling debt. Native ledger, graph, pending-node and recovery bounds still apply; 100,000 submitted Work items are not interchangeable with 100,000 combined Work/Claim records. A workload that reaches admission limits must report that boundary, not raise policy ceilings or silently drop history.

Historical queue inspection and operator commands

[!WARNING] The commands, facts, storage backends and scalar assignments in this historical section are superseded. They are not compatibility modes of the current implementation. Use the current queue reference and the current command's help; old queues are rejected unchanged.

gh aw work-queue operates on a dedicated branch without using the current checkout. Supply --repo owner/repo; use --branch to select a different queue branch (default: gh-aw-work-queue). The experimental command uses authenticated GitHub Git APIs to read and validate work-queue.jsonl, create trees and commits, and publish changes with non-force reference updates. It needs neither a checkout nor a Git executable, and accepts GitHub repositories rather than local Git remotes. Rejected concurrent updates are retried against a fresh branch snapshot and replay. In an initialized repository, an absent queue branch is initialized with a parentless commit; other files in an existing queue branch are preserved. GitHub Git APIs cannot create the first reference in an entirely empty repository. Authentication uses the GitHub CLI configuration or GH_TOKEN/GITHUB_TOKEN, with repository contents write permission required for mutations. All subcommands support --json for machine-readable output. Workflows enable the read-only snapshot MCP server with tools.work-queue: true.

The current workflow runtime and operator CLI use Git exclusively. The workflow field tools.work-queue.storage has been removed and is rejected for every value, including git. Remove the field from existing workflows; no legacy selector support or automatic migration is provided. Issue and pull request dependencies do not change the queue's canonical Git authority.

Command	Arguments
replay	Display the projected Work and Claims
stats	Count Work, Claims, and distinct transactions
compact	Canonically order facts and remove only identical duplicates
submit-work	--file work.json (or --file - for stdin); derives an id from the canonical JSON object
claim	--run-id RUN [--work-id ID]; defaults to the oldest available Work
finish	--claim-id ID --attempt-id ATTEMPT [--outcome TEXT]
cancel-work	--work-id ID
cancel-claim	--claim-id ID

These are operator commands; finish writes a Completion fact, but is not a worker safe-output authorization mechanism and does not execute external effects. The caller must independently establish the provenance of --run-id and --attempt-id. Worker authorization and MCP/safe-output integration remain separate implementation obligations described in the ADR.

The historical operator transaction wire format was Transaction; it is no longer defined in the current transactions.tsp or accepted by the current embedded schemas. The historical workflow runtime used a separate work-queue branch and the versioned WorkQueueTransaction format: required fields version: 2, kind, work, claim, and attempt, plus optional enqueued on Work. Unused claim/attempt fields are explicitly null; identities are nonempty strings. The Git loader upgrades unversioned/version-0/version-1 workflow records through successive codemods before validation and replay. Version 1 remains the closed five-field format without enqueued; historical records with extra fields are rejected before upgrading. The 1-to-2 upgrade changes only the version, leaving historical Work at age zero without inventing enqueue metadata. The snapshot envelope version is independent of the transaction version. These formats are not interchangeable; the CLI branch also preserves Work payloads and run provenance, which the workflow fact format does not contain.

Trusted workflow assignments use the compiler-managed work_queue_claim workflow-dispatch input, containing work_id, claim_id, and the work payload object (WorkQueueAssignment). aw_context remains reserved for caller metadata. Activation checks that the Claim is currently effective before capturing the assignment. When tools.work-queue: true and safe-outputs.dispatch-workflow are both configured, a dispatcher can read an available identity with work_queue_read and pass work_queue: {work_id: "..."} to an allowed same-repository worker's dispatch tool. The worker enables tools.work-queue: true; the compiler adds its reserved work_queue_claim input so activation admission and completion reconciliation are compiled. Workflows must not declare aw_context or work_queue_claim themselves. Trusted safe-output processing refreshes the queue, publishes a new Claim for that identity, verifies it is effective, and injects the assignment with work: {id: work_id} through work_queue_claim. The work_queue selector is not forwarded as a workflow input. Dispatch errors attempt to cancel the Claim. An ordinary dispatch without a selection and a staged preview create no Claim; call-workflow does not create one either. Concurrent Claims may supersede an assignment before worker activation, so admission and completion still recheck the durable queue. The MCP tools are work_queue_read and work_queue_claim_finish; the latter records a WorkQueueFinishIntent containing only outcome: "completed" or outcome: "cancelled". Artifacts use work-queue.snapshot.json and work-queue.finish.jsonl; the Git-backed durable transaction file is work-queue.jsonl.

When the runtime prompt advertises work-queue under <mcp-clis>, invoke these tools as work-queue work_queue_read '{"work":"example"}' and work-queue work_queue_claim_finish '{"outcome":"completed"}'. The tool names are subcommands of the server's CLI wrapper, not standalone executables. Copilot advertises this wrapper when CLI mounting is active; other engines advertise it with tools.cli-proxy: true. Both tools return JSON serialized in MCP text content. The finish-intent file contains only the outcome and is readable by the runner artifact collector even when the MCP container runs as a different user.

Pre-rename aw_context.work_claim assignments are schema-checked and normalized to work_queue, not treated as unassigned. Existing runtime storage on dispatch-coordinator / dispatch-work-coordinator.jsonl is read and updated in place with the same checked publication protocol. It is not silently copied to an independent queue. Explicit migration requires quiescing all writers and old workflows, renaming the existing branch/log, and deploying recompiled workflows before resuming. Both branch names or both log filenames together are ambiguous and fail closed. Logs/audit retain read compatibility for historical artifacts.

Current wire contract and schema checks

transactions.tsp defines the current version-3 QueueCommit contract shared by the operator and workflow runtime. Historical Transaction, WorkQueueTransaction and scalar assignment formats above are not accepted by these schemas.

Optional immutable backing_issue, checked IssueLink/IssueComment operations, and installed Policy.projectors extend this closed version-3 contract. Git remains authoritative; protected activation/conclusion hooks mirror only their own admitted Work and original authenticated Claims. Upgrade every Go/JavaScript reader and deployment before enabling these records. The backing Issue reference documents scope, native fields, pending recovery, coordination, and API budgets. Local projection/parity tests are not evidence of live intended-token writes. IssueProjection.tla separately checks the abstract projector authority and recovery boundary; it does not modify queue scheduling or establish that the hooks, credentials, GitHub API, or codecs refine these actions.

The checked-in schemas are generated by the dependency-free, fail-closed TypeSpec-subset generator, not copied from the official emitter:

python3 specs/work-queue/generate_contract.py
python3 specs/work-queue/generate_contract.py --check

--check compares the complete generated schema set with pkg/workqueue/schema/ and fails on drift. A separate validation runs the genuine @typespec/compiler@1.16.0 and @typespec/json-schema@1.16.0 with file-type=json and seal-object-schemas=true into a disposable output directory. The fail-closed comparison below resolves references and compares validation constraints for the supported schema subset, including custom identity bounds. The current 45-schema set passes this comparison; this is not a general JSON Schema equivalence solver or a proof of runtime validation. Do not overwrite the checked-in schemas with the separate official output.

For official validation, TOOL_DIR denotes a disposable directory containing those two exact pinned packages, and OUT_DIR denotes a separate output directory:

cp specs/work-queue/transactions.tsp "$TOOL_DIR/transactions.tsp"
"$TOOL_DIR/node_modules/.bin/tsp" compile "$TOOL_DIR/transactions.tsp" \
  --emit @typespec/json-schema \
  --option @typespec/json-schema.file-type=json \
  --option @typespec/json-schema.seal-object-schemas=true \
  --output-dir "$OUT_DIR"
python3 specs/work-queue/verify_official_contract.py \
  --official-dir "$OUT_DIR/@typespec/json-schema"

The current wire profile restricts numbers recursively, including payloads: only plain safe integers are accepted. Other exact quantities require explicit strings. All accepted payload fields and decoded values are retained without coercion.

Historical arbitration model

The retained WorkQueue.tla model abstracts identities as integers; the historical CLI used stable string identities and canonical JSON Work payloads. Protocol versions and payload data are outside the model's arbitration abstraction.

Verification status: the module includes parameterized safety theorem statements and the inductive proof argument below. TLC exhaustively checks the supplied finite configurations. The theorem statements are not mechanically checked by TLAPS; bounded model checking is not an unbounded proof.

Historical model's concrete protocol choices

The model fixes arbitration and makes the worker lifecycle, publication guards, and terminal-state protection explicit:

Boundary	Modeled rule
Arbitration	The least stable, uncancelled Claim identity wins on nonterminal Work. A persisted Completion fixes the winner; WorkCancellation removes authority.
Queue selection	Stage a Claim for the oldest available Work in the dispatcher's local replay. Use an immutable enqueue-time key with stable Work identity as the tie-breaker; skip claimed and terminal Work.
Terminal Work	Reject new state-changing transactions for completed/cancelled Work. Identical physical records may be duplicated without changing the fact set.
Dispatcher	The activation job reads the queue branch and packages its log and branch version into the activation artifact. The work-queue MCP server reads only that immutable snapshot and never accesses Git; the view may be stale while the agent runs. Mutations are revalidated and published only by trusted safe_outputs; pending competing Claims may become durable on nonterminal Work.
Worker	Each worker has one immutable inbound Claim and one pass through safe-output processing; it records at most one distinct Completion. Finalize carries no authority parameters.
Authorization	The winning worker verifies its newly committed Completion before outputs. Finished, stopped, and failed workers cannot restart or receive authorization again.
Compaction	Canonicalize order and remove identical duplicate records only. Preserve the entire fact set, including cancelled/superseded Claim history. More aggressive compaction needs a separate proof.

These are protocol refinements, not claims that an implementation already enforces them. Claim ordering is by stable identity, not arrival time. Arrival order can change which transactions are accepted; it cannot change replay of the same accepted fact set.

WorkOf, Inbound, and Origin provide small, deterministic identity mappings for TLC. Inbound represents validated trusted context, not agent-selected input. Claims also identify their owning run; multiple worker attempts may share one Claim/run. Payloads are abstracted to stable Work identities, assuming collision-free canonical identity and idempotent submission.

Best-effort queue ordering

Each Work fact carries immutable enqueued metadata, set once at submission and preserved through retries, replay, and compaction. The finite model uses the Work integer as the rank of the (enqueue time, Work identity) key, not as a physical log position or a globally allocated sequence number.

JavaScript and Go represent enqueued as Unix milliseconds, restricted to nonnegative integers no larger than 9007199254740991 so both languages compare exactly. Both replay projections expose an oldest-first available identity list, with UTF-8 Work identity as the tie-breaker. Historical Work without metadata has age zero and sorts before timestamped Work; replay never invents timestamps from record position or the current clock. Repeated submissions preserve the first durable Work fact's age, while conflicting metadata already present in the durable log is rejected.

JavaScript callers construct Work with createWorkTransaction and select or stage Claims with oldestAvailableWork / claimOldestAvailableWork, passing their local view including earlier pending intents. Go callers use NewWork and OldestAvailable. gh aw work-queue claim --run-id RUN selects once from its initial view and retains that Work identity across publication retries; --work-id ID remains an explicit operator override. work_queue_read lists available Work first in enqueue order by default, includes enqueue metadata, and returns the snapshot's recommended next_work identity or null. Its optional work selector reads a single identity, while optional sort reorders available Work and the queue-wide next_work recommendation. sort accepts one to four ordered keys (id, enqueued, or id_length), each with a direction (asc or desc): {"sort":[{"key":"enqueued","direction":"desc"}]} recommends newest available Work. Later keys break ties, then the default oldest-first order does. ID length counts Unicode code points. Non-available Work remains after available Work. Sorting is read-only: it does not change Claim selection, safe-output dispatch authority, or publication order, and the recommendation is not durable authority.

OldestAvailable chooses the least key among Work whose replayed state is available. Stage applies that preference to the local view, including earlier pending intents, so a batch cannot repeatedly select the same Work. Claimed Work does not block selection of newer available Work; cancellation of its last active Claim makes it eligible again with its original age. Work and claim arbitration remain separate.

Publication deliberately does not enforce oldest-first ordering. Allowed continues to accept competing Claims on nonterminal Work, and a version-conflict retry replays already selected intents without moving a Claim to another Work. An older submission can become visible after a newer item was selected; concurrent workers can also complete out of order. The model's local view is current durable facts plus pending intents at staging, but even that view may be outdated before publication. Implementations selecting from immutable activation snapshots have the same limitation.

This is a queue preference, not strict FIFO, a bounded-overtaking guarantee, or a claim that reordering has a particular probability. Reordering should be uncommon with fresh views and prompt publication, but TLA+ explores adversarial schedules and does not measure frequency. No global sequence allocator, head-of-line lock, or completion barrier is introduced.

Historical model's state and job boundaries

log is the only authoritative durable state. head abstracts an opaque, non-reused Git branch version. Branch creation is a version-checked write against the initial absent-branch token. All successful mutations change that version; no force-push or reuse of an old version is permitted.

The activation artifact is an immutable snapshot of the queue log, branch version, and validated worker assignment read during activation. The MCP server mounts that snapshot read-only and derives its query results with shared replay; it has no Git client or repository credentials. Its only writable mount is the safe-output intent directory, where work_queue_claim_finish(outcome?) records an outcome without accepting Work or Claim identity. The snapshot is only an early view and can be stale by the time the agent asks a question or submits work. Any future local pending-intent view remains non-authoritative. Every trusted writer records both the source log and its branch version; CandidateDerivation verifies that the candidate was generated from that latest source, not from the activation snapshot.

Workers progress through activation snapshot capture/admission, execution, finalize/no-finalize, preparation, push, verification, and effects. Admission reads the immutable activation snapshot and is not retained authority: WorkerCandidate checks current ownership against the latest log again. A stale candidate must be regenerated. Missing finalize cancels an effective Claim without permitting outputs; losing attempts stop without effects. In the implementation, safe-output processing downloads the activation and agent artifacts, reconciles against the latest Git-backed log, and gates user steps and handlers until a Completion for the trusted inbound Claim is verified. The finish outcome cancelled and an absent finish intent both map to finalize = FALSE; completed maps to finalize = TRUE.

Each worker's inbound Claim is fixed by Inbound. SingleCompletionPerWorker bounds its distinct Completion facts, and WorkerOneShot makes finished, stopped, and failed phases absorbing. The former reauthorization example added an impossible restart transition; it was not a reachable protocol failure and has been removed.

Compaction and recovery have independent prepared snapshots and bounded retries. Recovery cancels unresolved Claims whose owning runs terminated, including superseded Claims on nonterminal Work. Compaction discards stale snapshots and rebuilds from current facts.

terminalHistory records each Work item's complete fact set at its first terminal decision. It and authorizations/effects are observer histories, not additional queue files or decision-making state. Authorization/effect histories are sequences, so repeated execution of the same record cannot disappear through set deduplication. One ExternalEffect represents entry into one attempt's ordinary safe-output batch, not one GitHub API call.

Apply abstracts explicit rejection and idempotent no-op outcomes as no append. The model admits an identity-based Work resubmission with different enqueue metadata as idempotent and checks that staging it does not change replayed facts or the first durable Work age. Other exact duplicate intents are abstracted as no append; the model does not track implementation diagnostic counts. To keep the finite search bounded, each exact intent can be staged at most once per dispatcher.

JavaScript applyTransactions returns the candidate transactions, invalid intents in rejected, and an idempotent count. Exact duplicates of every kind and identity-based Work resubmissions are idempotent, not rejected, even when resubmitted Work carries a different enqueue time. Publication logs count requested intents as new, rejected, or idempotent on each attempt, independently of duplicate physical records in the source log. Retry outcomes describe only the refreshed attempt, not accumulated counts. All-no-op publication skips writes unless the log needs a protocol upgrade or canonicalization.

Required protections

This section describes the retained historical WorkQueue.tla abstraction, not the current QueueCommit wire contract or batching algorithm.

Activation snapshot: the activation job reads the queue branch and validates any trusted inbound assignment before uploading the activation artifact. The queue MCP process receives a read-only mount of the packed snapshot plus a writable safe-output intent directory; it does not receive a Git client or repository token. Snapshot queries are informative, not authority, and may be stale.

Publication: publish only if the branch still matches the version originally read. Otherwise fetch the latest log, replay it, and regenerate the proposed changes.

All dispatcher, worker, recovery, and compaction pushes use Publish. It requires both snapshot.base = head and snapshot.source = log. Their retry actions capture the latest version/log and rebuild the entire candidate through replay; none reuse stale output or splice it into newer state. Retry exhaustion fails without publication or external effects.

Terminal Work: reject new state-changing transactions after Work becomes completed or cancelled. Late competing Claims cannot reopen the decision.

Allowed applies the nonterminal guard to every new transaction type. TerminalFreeze requires a terminal Work item's current fact set to remain identical to its recorded terminal snapshot. Physical duplicate records and compaction may change representation, but cannot change those facts.

Invariants

Predicate	Guarantee
TypeOK, ValidLog	Valid identities/references; at most one terminal transaction per Work; Completion belongs to the trusted inbound Claim and the selected claimant.
SnapshotValidity, SnapshotVersions, ActivationSnapshotValidity, CandidateDerivation	A matching writer snapshot contains the current source log and an exactly regenerated candidate; activation admission reflects its immutable artifact snapshot; no snapshot is based on a future version.
Serialization	Every locally proposed dispatcher transaction is serialized identically for safe-output processing.
TerminalPersistence	Previously committed Completion/WorkCancellation facts remain durable.
TerminalHistoryValid, TerminalFreeze	All facts for a terminal Work item are frozen; neither late Claims nor other new transactions can change the decision.
SingleCompletionPerWorker, WorkerOneShot	One fixed inbound Claim and at most one distinct Completion per worker; terminal worker phases never restart.
SingleEffectiveClaim	At most one effective Claim per Work.
QueueSelection (action property)	Every staged Claim selects the oldest available Work in the local view at that step, not necessarily the oldest at publication or completion.
WorkResubmissionNoOp (action property)	A same-identity Work resubmission with different enqueue metadata may be staged, but does not change replayed facts or the original Work age.
WorkerOrigin, FinishRequired	Worker mutations concern only the inbound Claim; authorization requires finalize.
AuthorizationSoundness, EffectSoundness	Authorization follows durable Completion; effects follow authorization.
LifecycleAccounting	Each attempt authorizes/emits at most once, without resetting its lifecycle.
SingleAuthorization, SingleEffect	At most one safe-output attempt per Work receives authorization or enters its output batch.

Inductive proof argument

The argument is parameterized by the identity-domain sizes and retry limit. It does not use MaxHead or MaxLog, which appear only in TLC's exploration constraint.

Replay and compaction lemmas

Replay(s) is defined as Projection(Facts(s)). Substituting equal fact sets gives ReplayDeterminism immediately; physical record order and duplicates have no influence.

For finite f, induction on its cardinality proves Facts(Canonical(f)) = f. The empty case returns the empty sequence. The nonempty case emits one chosen member and recursively emits exactly the remaining members. Thus CompactionEquivalence follows by the replay lemma.

For any intent list, induction on its length also shows that applying it to logs with equal fact sets produces equal resulting fact sets: Allowed depends only on facts, and append adds the same accepted fact in either case. Consequently the modeled compaction preserves future mutation decisions, not just current displayed state. It may change HEAD and provoke a retry, as any concurrent write can.

OldestAvailable also depends only on facts and immutable Work metadata. Equal fact sets therefore give the same next selection, and compaction preserves the ordering preference even when it rearranges physical records.

Accepted-extension lemma

Assume ValidFacts(f). One accepted transaction preserves it:

1. Work adds an identity without references.
2. Claim and ClaimCancellation require their existing references and nonterminal Work. No existing Completion can have its arbitration result changed.
3. WorkCancellation requires nonterminal Work, so it cannot coexist with a prior terminal decision.
4. Completion requires nonterminal Work, the current winner, and the trusted attempt/Claim binding. It becomes the sole terminal decision.

Duplicate records preserve the fact set. Induction over the serialized batch gives the same result for Apply.

Initial state and snapshot preservation

The empty log, empty histories, zero HEAD/bases, and initial phases satisfy Safety.

The activation artifact contains the then-current branch version and full replayable transaction log. The finite model abstracts this to the version and admission result for the worker's inbound Claim. Activate derives admission from the captured log and stores the snapshot version only for admitted workers; no later action changes that field. Consequently ActivationSnapshotValidity and the bound on activation snapshot versions are inductive, while later execution can observe a stale version. Worker preparation derives its candidate from the latest log, never the artifact. Preparing or retrying a dispatcher/worker/recovery candidate applies the accepted-extension lemma to the current log. Preparing a compaction uses the canonicalization lemma. Both the source log and its version are captured, and CandidateDerivation records their exact relationship to the regenerated candidate. Recovery also captures the observed terminated runs.

A local/read/lifecycle step does not change remote facts or HEAD. A successful write either leaves the log unchanged or increases HEAD. Existing snapshot versions cannot equal the new HEAD because SnapshotVersions bounds them by the old HEAD. Their matching-source implications become false. Newly prepared snapshots again satisfy those implications. Therefore snapshot validity is inductive.

Durable safety

A push requires equality with both its recorded source version and source log. SnapshotValidity and CandidateDerivation therefore supply a valid extension generated from actual current facts, not a stale projection. Compaction supplies exactly the current fact set. Neither removes a terminal fact, preserving ValidLog and TerminalPersistence.

When Work first becomes terminal, Commit records all its facts in terminalHistory. Any later Apply rejects new facts for that Work through the universal nonterminal guard; worker preparation also stops on terminal Work. Duplicate records and compaction preserve fact sets. The stored terminal snapshot therefore remains equal to current Work facts, proving TerminalFreeze. This applies to higher-ranked and lower-ranked late Claims alike.

The winner is a single-valued function: a stored Completion's Claim, no Claim for cancelled Work, or the unique minimum active identity. Valid references and terminal exclusion prevent ambiguity. Hence SingleEffectiveClaim.

Authorization and effects

WorkerOrigin restricts a fresh worker append to its own Completion or ClaimCancellation. A newly committed Completion requires finalize. A terminal/no-op candidate moves to stopped, not committed.

Inbound is immutable, and Completion(a) is one fixed fact for worker a, so SingleCompletionPerWorker follows. Workers cannot return to preparation after committing; finished, stopped, and failed phases have no outgoing restart transition. Inspection of every action and stuttering proves WorkerOneShot. Reauthorization is therefore unreachable, not an additional failure scenario.

Only VerifyCompletion extends authorization history. It requires the attempt's committed phase and its exact durable Completion. The phase becomes authorized; it cannot return to committed. A second attempt for the same Claim cannot newly append Completion to terminal Work. Thus authorization records are durable, finalize-bound, and unique per attempt.

ValidLog allows only one Completion record per Work. Since an authorization contains that exact attempt-bound record and each attempt authorizes at most once, SingleAuthorization follows.

Only ExternalEffect extends effect history. It requires authorized, then moves irrevocably to done. The effect is backed by its authorization and is emitted at most once per attempt. Together with SingleAuthorization, this proves SingleEffect.

Remaining actions

Agent staging changes only equal local/serialized logs. Only Stage extends these sequences, and its Claim guard selects OldestAvailable from the preceding local view; every other action leaves them unchanged. Thus QueueSelection holds without imposing a publication-order invariant. Activation snapshot capture and admission do not grant authorization; execution-time worker preparation rechecks current Git facts. Retry exhaustion changes phase to failed without writing or emitting effects. Run termination can stop a worker but neither invents nor removes a terminal fact or authorization. Maintenance uses the same guarded write lemmas. Every action in Next, and stuttering, therefore preserves the strengthened Safety predicate.

By induction on execution length, Spec => []Safety follows under the modeled assumptions. This is a reviewable proof argument, not a TLAPS proof certificate.

Reproduce verification

The 2026-10-07 source-bound review record contains exact model/configuration/runner hashes, tool identity, bounded-run verdicts and trace counts. The initial review ran all 60 registered configurations: 14 positive searches exhausted; all 33 negative controls and nine guarded witnesses produced their exact expected outcome; four searches were interrupted at explicit local resource budgets. WorkQueue, QueueOrdering, FairDAGFork and FairDAGGitHub were not passes in that initial run. An independent longer FairDAGFork rerun subsequently exhausted 70,602 states at depth 28 in 6m47s. It did not resume or add the earlier partial search. That review's per-configuration result was 15 exhausted searches, 42 exact expected controls/witnesses and three unfinished searches: WorkQueue, QueueOrdering and FairDAGGitHub.

The separate 2026-10-07 refinement record supersedes that status without rewriting the earlier capture. The registered suite now includes the projection-corruption control: 16 positive searches exhausted, 34 negative controls and nine guarded witnesses matched their exact expected outcomes, and two searches remain unfinished. FairDAGGitHub exhausted 1,055,182 distinct states at depth 20 in 8m39s, with zero states remaining and its original bounds, constraints and safety conjuncts retained. TLC uses 64-bit fingerprints; that run reports optimistic collision probability 5.2E-7 and actual-fingerprint estimate 3.2E-8, not mathematical certainty.

Both historical searches successfully restored complete, pinned local TLC checkpoints and continued for another 1,200 seconds. WorkQueue reached 38,640,894 distinct states at depth 22 with 7,079,332 queued; QueueOrdering reached 51,756,372 at depth 17 with 23,003,758 queued. Neither exhausted or passed. These are actual continuations, not sums of independent searches. Checkpoint recovery rolls back to the saved checkpoint, which can precede the last interrupted progress report. Local restore succeeded; portable checkpoint archives remain unvalidated. The earlier nominal 1,800-second searches actually ran about 2,226–2,227 seconds; the record preserves both budget and measured time.

The refined sources also produced 18 seeded simulations with 309 sampled states and nine exact guarded witness traces. Their model/configuration hashes still match after merging main at 303b4028106137af47924a4bc079b8d3fdd8884c. Earlier counts below remain historical evidence. Neither finite model checking nor sampled traces verify Go/JavaScript runtime or supported-host refinement.

Evaluation refinements without state-space reduction

WorkQueue now dispatches each actor's actions by its existing phase guard. Every action retains its original guard and update; the CASE branches merely avoid evaluating actions whose first guard is false. Run termination and duplicate-record publication remain separate alternatives. No variable, transition, bound, safety invariant or action property is removed.

In FairWorkQueue default mode, Class(w) and Key(w) are always 1. Consequently active classes/keys are either empty or {1}, and selecting among them cannot depend on their pass values. NextWork directly chooses the same oldest eligible Work. Normalize retains the exact class-1/key-1 wake-up clocks, inactive clocks and active-set updates using the simplified formulas. Weighted/strict selection is unchanged. The recursive DAG closure also evaluates its preceding finite set before reusing it; TLCEval(x) = x. There is no VIEW, symmetry reduction or extra exploration constraint.

projection is a deterministic, non-authoritative cache: initialization sets it to Replay(log), every nonstuttering action sets it to Replay(log'), and ProjectionSoundness independently checks complete replay equality in every state. Safety retains every preceding conjunct and adds this check. Normal, guarded-witness and deliberately broken protocol transitions all update the cache; a separate corruption control bypasses that update and must violate ProjectionSoundness. Scheduling, observations and accounting remain solely in log. This adds a functional state component, not an independent choice or a reduced state space. It avoids replaying the same log separately for each guard and projected-state invariant.

compare-evaluation.mjs independently instantiates the original and revised modules over shared protocol variables/constants, lifting the original relation with the same replay-derived cache update. It explores the union of their transitions and checks NextEquivalence on each edge, so a missing revised transition cannot disappear from the comparison. Both initial-state predicates and safety predicates must agree/hold; fair-model replay projections must be exactly equal, including accounting clocks. The five comparison configurations cover historical recovery, default batches, weighted/strict selection and typed external gates. Missing-transition and changed-clock mutations must produce the exact action-property/invariant diagnostics. Removing the deterministic cache maps each revised state to exactly one original state; complete replay reconstructs it uniquely. These finite comparisons supplement this extension/algebraic equivalence argument. They are separate from the larger searches above and do not prove runtime refinement. All five comparisons and both exact mutation controls passed; the default FairBatch graph still has 13,662 distinct states at depth 20.

To reproduce the comparison against the last unrefined source:

baseline="$(mktemp -d)"
git archive 4ae415cc7046e215b6056fed90c26e4b915ef06b specs/work-queue |
  tar -x -C "$baseline"
export JAVA_BIN=/path/to/java
export TLA2TOOLS_JAR=/absolute/path/to/tla2tools.jar
node specs/work-queue/compare-evaluation.mjs \
  "$baseline/specs/work-queue" \
  "$PWD/.queue-validation-cache/evaluation-comparison"

The comparison rejects changed configurations, an unexpected TLC checksum, timeouts, tooling failures and unexpected mutation diagnostics. Its manifest is a pass only when every case finished. Use a fresh results directory rather than overwriting an earlier capture.

The long-run collector .github/scripts/work-queue-formal-check.cjs accepts FORMAL_CONFIG=WorkQueue, QueueOrdering or FairDAGGitHub. It executes the model/configuration copies in its evidence bundle, not live checkout files, so concurrent source edits cannot change the inputs after their hashes are recorded. RESULTS_DIR and TLA2TOOLS_JAR must be absolute paths. A natural successful exit with an empty remaining queue is required for a pass; a timeout or unvalidated checkpoint never establishes exhaustion or resumability.

Successor: mandatory fair scheduling and batched workers

The priority/fairness specification defines the replacement protocol. FairWorkQueue.tla models its causal atomic Claim batches, FIFO defaults, two-level integer-pass selection, fresh selection after CAS conflicts, request deduplication, and independent Claim completion/effect authorization within one worker assignment.

Each Claim consumes a logical slot and one service charge. A worker group consumes one native slot until trusted termination/release; completing one member does not release that slot. Missing finish intent cancels only that member. Published Completions survive recovery, and effects require the same assigned Claim's authorization.

The model has first-class immutable Work dependency sets and normalized external Issue/PR gates. Only a verified-delivery Result releases a Work successor; Completion alone does not. Unknown/unavailable external observations block admission, and a closed-unmerged PR does not satisfy its merged predicate.

It abstracts a fixed policy epoch, one compatible worker profile, one request/group per dispatcher, native run identity as its group identity, and canonical causal log order. Work is seeded in the first commit; immutable graph edges and resolved resource identities are model parameters representing its admitted metadata. External resources abstract an authorized foreign Issue and PR as typed host/repository/number/identity references, with at most two observations each. Weighted cases abstract two classes and two accounting keys with 2:1 shares; default mode collapses both. Effect entry and trusted delivery verification are separate observer steps.

It does not model dynamic graph admission, multi-profile packing, policy edits, idempotency fingerprints/replayed transport responses, actual GitHub credentials, resource IDs, observation freshness, artifact delivery, JSON codecs, OTLP delivery, or unbounded fairness/liveness. Work positions are causal FIFO positions. The protocol review revision additionally specifies selection-before-packing, authenticated activation binding recovery, terminal DeliveryFailure/replacement rules, operational Control, batch trust domains, and replay/resource budgets. These are acceptance obligations, not behavior added to or verified by this model. In particular, DecisionValidity checks conformance to NextWork; it is not an independent proportional-service or eventual-grant assertion. The dedicated fairness release gate is specified in the validation plan. The preceding WorkQueue.tla checks remain regression evidence for the existing implementation, not an operational legacy mode in the replacement.

For a focused successor check, set TLC_MODEL_FILTER=FairWorkQueue. Omit this filter to run the complete original, successor, and Claim-scope suite. Set TLC_CONFIG_FILTER=FairBatch to run one named configuration; unknown or incompatible filters fail rather than returning a no-op success.

The same check.sh additionally runs:

Configuration	Expected result
FairBatch.cfg	Two dispatchers compete for a two-Claim worker batch; safety, independent logical/native limits, and per-Claim authorization hold
FairThreeClaim.cfg	One worker receives three Claims and independently completes, cancels, or omits members across crash/recovery interleavings
FairPriority.cfg	Weighted class/key decisions and Claim limits hold
FairStrict.cfg	Strict class selection with weighted keys holds
FairDAGChain.cfg	A dependent is admitted only after its predecessor's verified Result
FairDAGForward.cfg	An older child referencing a later-numbered parent waits while that ready parent runs
FairDAGFork.cfg	Siblings become independently schedulable after their common predecessor succeeds
FairDAGGitHub.cfg	A child needs its Work predecessor and both foreign Issue/PR conditions; bounded to one observation/resource plus checked boundary successors
FairGitHubDependencies.cfg	Both Issue-completed and PR-merged observations must satisfy the external gate
BrokenProjection.cfg	A cache-only forged completion must violate complete log-replay equality
BrokenBatchSelection.cfg	Deliberately bypass selection; DecisionValidity must fail
BrokenClaimEffects.cfg	Use another unfinished Claim's effects after one Claim completes; EffectAuthorization must fail
BrokenAssignmentHandle.cfg	Finish another worker's Claim; ClaimClosureAuthority must fail
BrokenBatchCAS.cfg	Overwrite from a stale batch snapshot after Completion; TerminalPersistence must fail
BrokenBatchRelease.cfg	Release a live group's native slot after only some Claims finish; RunReleaseAuthority must fail
BrokenDAGDependency.cfg	Claim a not-ready successor; DependencyAuthorization must fail
BrokenDAGResult.cfg	Publish a Result before delivery verification; ResultEffectSoundness must fail
BrokenDAGCycle.cfg	Cyclic constant graph is rejected during setup with exit 151 and the exact DAGValidity-is-FALSE diagnostic, not a parser failure
BrokenExternalDependency.cfg	Admit Work with unknown/unsatisfied external gates; ExternalAuthorization must fail
BrokenPRClosedAsMerged.cfg	Treat a closed-unmerged PR as ready; ExternalTruth must fail
BatchedAssignmentWitness.cfg	Guarded model reaches a multi-Claim assignment; the deliberately false NoBatchedAssignment fails
PartialCompletionWitness.cfg	Guarded model reaches one completed and one open member; the deliberately false NoPartialCompletion fails
DAGJoinWitness.cfg	A success-path subset of guarded actions, with fixed root/sibling/join dispatcher roles, reaches the join after both Results; false NoJoinClaim fails

Before the DAG extension, successor checks completed on 2026-10-05 at commit f50550e8dc with the pinned TLC 2.19/Java 21: FairBatch exhausted 4,902 distinct states at depth 17; FairThreeClaim exhausted 4,144 at depth 17; FairPriority and FairStrict each exhausted 283 at depth 14. All five negative controls produced their named violations; the guarded batching and partial-completion witnesses produced their expected counterexamples without a safety failure. These are bounded model checks, not an unbounded proof or runtime conformance result.

The current DAG/result/Issue/PR cases exhaust the following positive state spaces:

Configuration	Distinct states	Graph depth
FairBatch	13,662	20
FairThreeClaim	34,075	23
FairPriority	675	17
FairStrict	675	17
FairDAGChain	13,846	24
FairDAGForward	13,846	24
FairDAGFork	70,602	28
FairGitHubDependencies	9,749	14

Total exhausted: 157,130 distinct positive states. The ten negative controls require nine named invariant violations and one exact constant-cycle setup rejection. The three reachability witnesses demonstrate batching, partial completion, and a guarded diamond join. JoinWitnessSpec restricts to successful root/sibling/join roles while using only guarded actions; it proves reachability, not exhaustive coverage of all diamond failure/retry interleavings.

Full-suite verification is incomplete. Two additional exhaustive searches were stopped without reaching exhaustion on 2026-10-05:

Configuration	Distinct states explored	Last depth	Result
FairDAGGitHub	588,795	14	No violation observed; not a passed/exhausted check
Existing QueueOrdering	109,949,148	18	No violation observed; not a passed/exhausted check

These state-space-heavy cases remain in check.sh; their bounds were not reduced to manufacture a pass. Checkpoints/logs are retained in the session artifacts. The other original checks completed, including WorkQueue (59,444,361 distinct states, depth 35, resumed from its checkpoint), Recovery (147,542, depth 20), the original negative controls/witness, and traces.sh. Passing successor checks do not substitute for the two incomplete searches.

Re-run a named case with TLC_CONFIG_FILTER. To resume a retained TLC checkpoint, use the same jar/model/configuration and worker count with -recover /path/to/checkpoint-directory; the checks here used two workers.

Claim-scoped safe outputs and mixed DAG outcomes

ClaimScopedWorker.tla separately formalizes enforced output attribution and mixed outcomes. Its fixed trusted assignment contains one or three Claims. Omitted selectors normalize automatically only for an originally one-Claim assignment; explicit foreign handles and missing multi-Claim selectors are rejected. A multi-Claim assignment never becomes implicitly single-Claim when other members close.

flowchart LR
    Single["One-Claim assignment"] --> Auto["Omitted selector: attach sole handle"]
    Multi["Multi-Claim assignment"] --> Explicit["Explicit member handle required"]
    Auto --> Scope["Canonical Claim-scoped output"]
    Explicit --> Scope
    Scope --> Finished["Same Claim's verified Completion"]
    Finished --> Effects["Authorized effects and verified Result"]
    Cancelled["Cancelled Claim"] --> NoEffects["No effects or Result from this attempt"]
    Effects --> DAG["Only declared Result-dependent successors become ready"]

All closures and Results are facts in one abstract log. Safe outputs preserve their resolved Claim and original selector; effects require that same Claim's Completion. Cancelled Claims cannot emit effects or Results. The mixed witness finishes Claims 1/3, cancels Claim 2 despite its staged output, and admits the successor requiring Results 1/3 while the Claim-2-dependent successor waits. Cancellation is not batch failure or terminal WorkCancellation; the existing FairWorkQueue model separately covers returning that Work to availability.

Run this focused suite with TLC_MODEL_FILTER=ClaimScopedWorker, or select a single configuration with TLC_CONFIG_FILTER.

Configuration	Expected result
ClaimScopeSingle.cfg	Automatic/explicit one-Claim attribution, foreign-selector rejection, closure/effect/Result safety
ClaimScopeMixed.cfg	Three independently completed/cancelled/omitted Claims; scoped outputs and Result-only DAG admission
BrokenMissingClaimScope.cfg	Assign an omitted multi-Claim selector to the first member; OutputScope fails
BrokenForeignClaimScope.cfg	Replace a foreign explicit selector with the sole handle; OutputScope fails
BrokenLastOpenClaimScope.cfg	Infer an omitted selector from the last open member of a multi-Claim assignment; OutputScope fails
BrokenCancelledClaimOutput.cfg	Execute a cancelled member's staged output; EffectAuthorization fails
BrokenMixedDAGAdmission.cfg	Use Claim closure instead of verified Results to admit a successor; DAGAuthorization fails
SingleClaimScopeWitness.cfg	Guarded model reaches a sole-Claim effect with automatically attached scope; false NoAutomaticScope fails without violating Safety
MixedClaimDAGWitness.cfg	Guarded model reaches finished/cancelled/finished members, scoped effects only for 1/3, and the corresponding ready successor; false NoMixedDAGProgress fails without violating Safety

The two positive cases exhaust 144 and 120,832 distinct states respectively (depths 12 and 25), totaling 120,976 on 2026-10-05 with the pinned TLC/Java setup. The controls/witnesses require their exact named violations, not parser/tool errors. These checks do not substitute for the two unfinished searches above.

The model abstracts an already validated assignment/native binding, one required scoped handler batch per root, trusted delivery verification, and two fixed successor dependency sets. It does not model concrete output schemas, every handler type, no-write task contracts, temporary-ID codecs, Git CAS, retries in a new assignment, actual API delivery, fair scheduling, or liveness. Handler-wide enforcement remains a replacement runtime conformance obligation, not a deployed feature established by this model.

Independent recurring service evidence

QueueService.tla checks one sibling competition set with exact strides for weights 5:3:2, independently of the queue lifecycle model. Its count invariants do not compare a selector with itself: they check a three-grant prefix-deviation bound and exact shares over each ten-grant cycle. At a virtual threshold, each fixed-set stream differs from its ideal event count by at most one; summing those stream errors gives the stated conservative three-competitor bound. This justification and the finite checks apply to the stated fixed set, not arbitrary dynamic fairness intervals.

The dynamic case allows arbitrary membership changes and checks eventual grants for continuously eligible competitors under weak fairness of packable Grant. Each competitor's service bit must recurrently take both values; a stale last winner cannot satisfy the property without new grants. Relative pass clocks and discarded inactive past debt form a finite quotient of the anti-idle-credit rule. Inactive future debt remains; reactivation uses the specified clamp.

Configuration	Expected result	Evidence
ServiceFixed	Share/deviation invariants and eventual service pass	30 exhausted states, depth 30
ServiceDynamic	Eventual service under eligibility changes passes	60,360 exhausted states, depth 26
BrokenServiceShare	ServiceDeviation violation	Exact invariant diagnostic, exit 12
StrictServiceStarvation	Lower-priority eventual service fails	Exact temporal diagnostic, exit 13
UnfairServiceStarvation	Eventual service without fair opportunities fails	Exact temporal diagnostic, exit 13
UnpackableServiceStarvation	Eligibility without packable opportunities fails	Exact temporal diagnostic, exit 13

flowchart LR
    Eligible["Continuously eligible competitor"] --> Opportunity{"Packable recurring Grant?"}
    Opportunity -->|No| NoPromise["No eventual-service guarantee"]
    Opportunity -->|Yes| Policy{"Weighted positive shares?"}
    Policy -->|Strict lower class| Starvation["Starvation is permitted"]
    Policy -->|Yes, with service fairness| Service["Bounded model checks recurring grants"]

Reproduce this model alone with TLC_MODEL_FILTER=QueueService, using the Java and jar settings in the reproduction instructions. Full class/key composition, arbitrary weights, native publication/release and runtime refinement remain separate obligations. The new checks do not finish FairDAGGitHub or QueueOrdering, and the earlier interrupted dynamic exploration is not added to these exhausted counts.

Bounded launch, delivery and recovery evidence

QueueLifecycle.tla separates launch-boundary safety from fairness arithmetic. Its independent FIFO packing oracle uses profile order X/Y/X: one available dispatch admits the first X only; two dispatches permit X/X and Y without skipping the middle winner. Immutable assignments, one selected sender, activation recovery, conflicting bindings, attempt-1 effects, Controls, logical/native release, delivery outcomes and replacement admission are checked together.

Configuration	Expected result	Exhausted evidence
LifecycleRecurring	Safety across two fully drained epochs	496 states, depth 20
LifecyclePacked	Safety for the bounded packed assignment	207,612 states, depth 33

Eleven negative controls require the exact named violations for fair-prefix packing, one sender, binding authority, unauthenticated activation, reruns, premature release, conflict release, pause/preemption confusion, delivery exclusivity, replacement safety and delivery-verification budgets. Three guarded witnesses reach mixed DAG outcomes, recovered activation and retained capacity after conflicting activation. Witness violations are expected reachability diagnostics, not failures of the guarded safety properties.

flowchart LR
    Prefix["Independent X/Y/X packing oracle"] --> Assignment["Immutable group membership"]
    Assignment --> Marker["One sender marker"]
    Marker --> Unknown["Launch uncertain: retain native slot"]
    Unknown --> Activation["Checked activation recovers binding"]
    Activation --> Members["Independent Claim closures and delivery barriers"]
    Activation --> Conflict["Conflicting run: retain reservation"]
    Members --> Terminal["Exact terminal evidence releases shared slot"]
    Members --> DAG["Only verified Results unblock Work successors"]

Reproduce these checks with TLC_MODEL_FILTER=QueueLifecycle. The positive total is 208,108 exhausted states, not an unbounded proof or runtime test. Terminal, activation and receipt predicates abstract independently checked evidence; they do not verify real GitHub responses, credentials, artifact authenticity or resource targets. The model does not cover actual Git CAS, wire codecs, arbitrary graphs, the native scheduler, all handler types or a liveness theorem. These checks do not complete the two interrupted large searches or the supported-host integration gate.

Bounded backing-Issue projection evidence

IssueProjection.tla is a bounded authority/recovery model for one admitted Work, one Issue, one original Claim and one projector identity. It distinguishes exact pre-existing-Issue grants from a projector creation receipt, and checks that actual projection still requires the installed projector and original authenticated context. The admitted completion policy is captured once: later policy expansion cannot enable closure. Closure requires a verified Result, a non-PR delivery, and a bound authorized Issue. Human-authored content is invariant. An Issue creation accepted without a durable receipt stays uncertain under a held coordination fence; the model does not invent safe recovery or retry it.

Configuration	Expected result
IssueExisting.cfg, IssueCreated.cfg	Existing grants and receipt-backed creation preserve projection and closure authority
IssueDefaultOpen.cfg	Policy expansion after admission does not grant closure
IssuePRStaysOpen.cfg	PR delivery never closes the Issue
IssueBrokenUnowned.cfg	Deliberately unsafe admission violates AdmissionAuthority
IssueBrokenPayloadClose.cfg	Deliberately unsafe payload-driven closure violates ClosureAuthority
IssueBrokenRetry.cfg	Blind retry after an uncertain creation violates SingleCreation

Run the focused suite with TLC_MODEL_FILTER=IssueProjection. The positive configurations exhaust these finite states and the three negative controls require their named counterexamples. The model abstracts exact identity matching as booleans and does not prove queue replay, native API semantics, coordination implementation, creation-receipt authenticity, runtime refinement, or liveness.

Daily evidence collection

daily-work-queue-formal-verification.md collects FairDAGGitHub and QueueOrdering on separate parallel runners daily, with manual dispatch available. Each verification job has a five-hour limit. Its deterministic collector interrupts TLC after 4h40m, preserving time to finalize and upload the artifact instead of losing it to a job timeout.

Artifacts are retained for 30 days and named work-queue-formal-<configuration>-<run-id>-<attempt>. They contain exact model/config snapshots and hashes, Java/TLC provenance, command, raw log, normalized verdict/counts, and checkpoint inventory. A full state archive is included only when a checkpoint diagnostic and basic file presence checks pass and the state fits the 256 MiB uncompressed cap; otherwise the explicit omission reason is retained. Large state directories are never uploaded indiscriminately.

A read-only agent writes a separate work-queue-formal-handoff-<run-id>-<attempt> artifact for subsequent agents. It does not rerun the checker, modify the model, or reinterpret timeouts/partial searches as successful verification. Setup failures keep an explicit setup_incomplete record; artifact availability remains visible even if agent analysis fails. GitHub resource safe outputs are preview-only; the deterministic verification and handoff artifact uploads remain real.

Each daily run currently starts fresh; it does not resume a prior artifact. Repeated timeouts on identical sources do not accumulate verification coverage or prove exhaustion. Archives are labeled unvalidated_checkpoint_candidate, with resumable: false and recovery_validation: "not_attempted". Basic file presence and packaging do not validate model/worker checkpoint completeness or actual restore capability. The collector step uses continue-on-error: artifact collection/workflow success must be distinguished from the result.json verification verdict. The five-hour limit applies to each matrix job, not the whole workflow including later analysis. See the evidence contract for follow-up recovery and failure-signaling requirements.

Safety includes state types, single open owner per Work, causal history, recomputed selection, logical/native capacities, exact Claim charge counts, one dispatch request per group, assignment integrity, one effect authorization per Claim, per-handle closure and run-release authority, terminal persistence, and independent FIFO/strict-priority assertions. The DAG extension additionally checks graph acyclicity, readiness at each Claim's causal prefix, Result authority/verified delivery, and external condition truth/admission. Positive cases exhaust their bounded state space; a trace showing partial completion is reachability evidence, not a proof that arbitrary partial completions eventually happen.

Use Java 21 and the official tla2tools.jar v1.7.4, which reports TLC 2.19. Jar SHA-256:

936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88

TLA2TOOLS_JAR=/path/to/tla2tools.jar \
JAVA_BIN=/path/to/java \
bash specs/work-queue/check.sh

The runner checks every registered configuration across the six models, including the historical configurations below. Positive configurations require exhaustive successful termination; negative controls and guarded witnesses require their exact named diagnostic and exit status, not a parse/tooling failure. Use TLC_MODEL_FILTER and TLC_CONFIG_FILTER to select a subset; unmatched filters fail. Full reports are saved under a printed temporary path; set TLC_RESULTS_DIR to retain them at a chosen location. The historical controls below deliberately bypass branch-version, terminal-state or selection protection; those are not reachable behaviors of the guarded historical protocol.

Configuration	Scope / expected result
WorkQueue.cfg	One Work, two competing Claims, two dispatchers, three workers (two share a Claim), three branch changes, four records; Safety, WorkerOneShot, QueueSelection, and WorkResubmissionNoOp hold.
Recovery.cfg	One Work, two Claims/workers, one dispatcher, four branch changes, five records; Safety holds through recovery/compaction interleavings.
QueueOrdering.cfg	Two Work items, two Claims/workers/dispatchers, two branch changes, four records; Safety, WorkerOneShot, and QueueSelection hold across selection, retry, cancellation, and compaction interleavings.
BrokenCAS.cfg	Bypass the branch-version check and overwrite with a stale snapshot; TerminalPersistence fails.
BrokenTerminal.cfg	Bypass terminal protection and append a competing Claim after Completion; TerminalFreeze fails.
BrokenQueueSelection.cfg	Bypass oldest-available selection while retaining publication safety; QueueSelection fails.
WeakOrderingWitness.cfg	Under guarded Spec, a newer Work is claimed before an older submission becomes visible; the deliberately false NoOutOfOrderClaim invariant fails.

Earlier records reported three positive searches on 2026-10-02, checking Safety, WorkerOneShot and QueueSelection: 7,218,153 distinct states at graph depth 33 for concurrency, 49,087 at depth 19 for recovery, and 1,696,812 at depth 24 for two-Work ordering. These retained historical counts are not a fresh, source-bound verification verdict for the current checkout. The branch-version, terminal-state and queue-selection controls reported expected violations at depths 7, 10 and 4; the guarded weak-ordering witness reported an out-of-order Claim at depth 6. Use the dated current-source review evidence, not these older counts, to identify exhausted versus unfinished searches.

Bound constrains branch changes and physical log size, not execution depth. TLC also checks immediate successor states before pruning them. Deadlock checking is disabled because stopped/failed workflows are intentional; no fairness or liveness theorem is asserted.

Inspect execution traces

Generate bounded textual simulations of six configurations and nine reachable counterexamples to deliberately false witness invariants. WorkQueue is historical; the other models abstract parts of the current protocol:

TLA2TOOLS_JAR=/path/to/tla2tools.jar \
JAVA_BIN=/path/to/java \
TLC_TRACE_DEPTH=16 TLC_TRACE_COUNT=3 \
bash specs/work-queue/traces.sh

The script prints a temporary results directory (or uses TLC_RESULTS_DIR when set). simulation_* files are historical WorkQueue traces; current abstraction traces use prefixes FairBatch, FairDAGGitHub, ClaimScopeMixed, ServiceDynamic and LifecyclePacked. Each has at most TLC_TRACE_DEPTH states; TLC_TRACE_COUNT sets the number of seeded random simulations per configuration. The runner requires emitted traces and successful TLC termination, records Java identity/settings and SHA-256 hashes, and rejects source/tool drift.

These samples check configured invariants along the emitted trajectories. They are not exhaustive coverage, a liveness proof, native queue replay, or guaranteed occurrences of particular actions. In the 2026-10-07 run with depth 32 and count 3, all 18 traces were emitted: 272 sampled states across 15 current-abstraction traces and 31 across three historical traces. All nine guarded witnesses produced their exact expected diagnostic; no unexpected safety or tooling failure was accepted. sources-before.sha256 and sources-after.sha256 bind this evidence to unchanged model/configuration/runner sources and the TLC jar.

The root *Witness.log files contain the four historical model-checked counterexamples below. Current guarded witnesses are in current-witnesses/:

Configuration	Reachable current behavior
PartialCompletionWitness	One immutable assignment member completes while another remains open
MixedClaimDAGWitness	Per-Claim success/failure independently permits or blocks DAG progress
LifecycleMixedDAGWitness	Mixed lifecycle and delivery outcomes settle independent successors
LifecycleActivationWitness	Checked activation recovers an uncertain launch binding
LifecycleConflictWitness	Conflicting activation retains the native reservation

Each witness configuration also checks Safety; the script accepts only its named witness violation, not a safety violation or a TLC failure.

Witness	What to inspect in its counterexample
NoCompetingClaims	Two dispatchers select the same Work in their local views before either Claim is durable. Both Claims persist, but replay still selects one effective winner.
NoRecoveredOrphan	A run terminates, then recovery prepares and publishes its ClaimCancellation.
NoExternalEffect	A worker finalizes, commits Completion, verifies it, and enters its output batch.
NoOutOfOrderClaim	A dispatcher selects newer Work from its local view before staging an older submission; publication preserves the Claim rather than imposing strict FIFO.

These invariants are intentionally not protocol requirements: their violation demonstrates reachability of legitimate behavior under each guarded Spec. Unlike the deliberately unsafe Broken*.cfg configurations, the witness configurations do not add unsafe actions. Inspect the preceding states, not just the final state, to verify the ordering claimed by the ADR. Witnesses show that the model permits these paths; they do not establish that a runtime implementation follows them or that progress is guaranteed.

Runtime smoke coverage

The private .github/workflows/smoke-work-queue.md workflow is a read-only observer. It exercises snapshot read/explain tools through the compiled MCP mount and verifies that unassigned finish is unavailable or rejected without recording an intent. Its verification job rejects a finish artifact or failure report and requires a noop result. Ordinary reports use the observer's normal workflow authorization; they do not acquire worker or queue-control authority.

This smoke test checks observer wiring and unassigned-finish rejection. It does not establish dispatcher submission, native binding, verified worker delivery, recovery, or compaction.

Limits

Safety does not imply eventual dispatch, successful external effects, or eventual orphan recovery. Those require fairness, available workflows, and successful retries. A crash after Completion but before outputs can leave delivery uncertain; the current runtime retains independent barriers and reconciles Result or DeliveryFailure instead of replaying completed effects. This is not atomic or exactly-once delivery. The activation artifact is a snapshot, not a live subscription; reads can be stale and are never used as final authority.

The independent ESLint factory model compares the configured factory with executable observations of its real sources and ESLint behavior. It separates runtime enforcement from prompt assumptions and external queue installation; it is not proof that the factory automatically admits an Issue-to-Work DAG or that arbitrary agents follow their prompts.

The model does not prove GitHub authentication, aw_context provenance validation, payload canonicalization, parser behavior, transport errors, or the implementation's refinement of these abstract actions. These remain implementation obligations. It does not make arbitrary external API batches atomic or exactly-once.