hardbyte · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -14,7 +14,7 @@ members = [
 exclude = ["awa-python", "spike"]
 
 [workspace.package]
-version = "0.6.15"
+version = "0.6.16"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 description = "Postgres-native background job queue — transactional enqueue, heartbeat crash recovery, SKIP LOCKED dispatch"
@@ -25,11 +25,11 @@ categories = ["database", "asynchronous", "web-programming"]
 
 [workspace.dependencies]
 # Internal crates
-awa-model = { path = "awa-model", version = "0.6.15" }
-awa-macros = { path = "awa-macros", version = "0.6.15" }
-awa-metrics = { path = "awa-metrics", version = "0.6.15" }
-awa-worker = { path = "awa-worker", version = "0.6.15" }
-awa = { path = "awa", version = "0.6.15" }
+awa-model = { path = "awa-model", version = "0.6.16" }
+awa-macros = { path = "awa-macros", version = "0.6.16" }
+awa-metrics = { path = "awa-metrics", version = "0.6.16" }
+awa-worker = { path = "awa-worker", version = "0.6.16" }
+awa = { path = "awa", version = "0.6.16" }
 
 # Database
 sea-orm = { version = "=2.0.0-rc.38", default-features = false, features = ["sqlx-postgres", "runtime-tokio-rustls", "with-chrono", "with-json"] }

diff --git a/README.md b/README.md
@@ -390,7 +390,7 @@ All coordination through Postgres. The Rust runtime owns dispatch, leases, heart
 | [0.5 → 0.6 upgrade](docs/upgrade-0.5-to-0.6.md) | Step-by-step operator checklist for the staged storage transition |
 | [0.6.9 → 0.6.10 upgrade](docs/upgrade-0.6.9-to-0.6.10.md) | Rolling patch upgrade, rollback, and optional runtime privilege tightening |
 | [0.6.14 → 0.6.15 upgrade](docs/upgrade-0.6.14-to-0.6.15.md) | Rolling patch upgrade: bounded worker finalization, the claim batch index and the batch compatibility insert |
-| [0.6.15 → 0.6.16 upgrade](docs/upgrade-0.6.15-to-0.6.16.md) | Rolling patch upgrade: operator prune halt, and batch compatibility inserts that give way to per-row producers instead of deadlocking |
+| [0.6.15 → 0.6.16 upgrade](docs/upgrade-0.6.15-to-0.6.16.md) | Rolling patch upgrade: bounded rescue drains of abandoned claims, batch compatibility inserts that give way to per-row producers, new-lane provisioning order, the operator prune halt and its grants, and claim batch index fixes |
 | [Configuration reference](docs/configuration.md) | `QueueConfig`, `ClientBuilder`, Python `start()`, env vars |
 | [HTTP workers and callbacks](docs/http-callbacks.md) | Serverless dispatch, callback receiver endpoints, signature verification |
 | [Lifecycle hooks](docs/lifecycle-hooks.md) | React to job start/finish/retry/callback events for metrics, alerting, cleanup |

diff --git a/awa-cli/Cargo.toml b/awa-cli/Cargo.toml
@@ -14,7 +14,7 @@ path = "src/main.rs"
 [dependencies]
 awa-model.workspace = true
 awa-worker.workspace = true
-awa-ui = { path = "../awa-ui", version = "0.6.15" }
+awa-ui = { path = "../awa-ui", version = "0.6.16" }
 axum.workspace = true
 sqlx.workspace = true
 tokio.workspace = true
@@ -28,5 +28,5 @@ hex.workspace = true
 uuid.workspace = true
 
 [dev-dependencies]
-awa-testing = { path = "../awa-testing", version = "0.6.15" }
+awa-testing = { path = "../awa-testing", version = "0.6.16" }
 assert_cmd = "2"
diff --git a/awa-cli/pyproject.toml b/awa-cli/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "maturin"
 
 [project]
 name = "awa-cli"
-version = "0.6.15"
+version = "0.6.16"
 description = "CLI for the Awa Postgres-native job queue (migrations, admin, serve)"
 readme = "README.md"
 requires-python = ">=3.10"

diff --git a/awa-cli/src/control.rs b/awa-cli/src/control.rs
@@ -8,17 +8,22 @@ pub(crate) enum ControlCommands {
     Status,
     /// Stop new reclamation and housekeeping; let admitted work drain.
     Halt {
+        /// Control to halt; only `maintenance.prune` is supported
         #[arg(long, default_value = "maintenance.prune")]
         scope: String,
+        /// Halt mode; only `drain` is supported
         #[arg(long, default_value = "drain")]
         mode: String,
+        /// Why the halt is requested, stored with it and shown by `status`
         #[arg(long)]
         reason: String,
     },
     /// Lift exactly the named current halt, without waiting for drain completion.
     Resume {
+        /// Control to resume; only `maintenance.prune` is supported
         #[arg(long, default_value = "maintenance.prune")]
         scope: String,
+        /// UUID of the current halt (`halt_id` in the `halt` or `status` output)
         #[arg(long)]
         halt: Uuid,
     },

diff --git a/awa-python/Cargo.lock b/awa-python/Cargo.lock
diff --git a/awa-python/Cargo.toml b/awa-python/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "awa-python"
-version = "0.6.15"
+version = "0.6.16"
 edition = "2021"
 
 [lib]
@@ -12,8 +12,8 @@ default = ["cel"]
 cel = ["awa-model/cel"]
 
 [dependencies]
-awa-model = { path = "../awa-model", version = "0.6.15" }
-awa-worker = { path = "../awa-worker", version = "0.6.15", features = ["__python-bridge"] }
+awa-model = { path = "../awa-model", version = "0.6.16" }
+awa-worker = { path = "../awa-worker", version = "0.6.16", features = ["__python-bridge"] }
 pyo3 = { version = "0.29", features = ["macros", "abi3-py310", "chrono"] }
 pyo3-async-runtimes = { version = "0.29", features = ["tokio-runtime"] }
 sqlx = { version = "0.8", features = ["runtime-tokio-rustls", "postgres", "chrono", "json"] }

diff --git a/awa-python/pyproject.toml b/awa-python/pyproject.toml
@@ -5,7 +5,7 @@ build-backend = "maturin"
 [project]
 name = "awa-pg"
 requires-python = ">=3.10"
-version = "0.6.15"
+version = "0.6.16"
 description = "Postgres-native background job queue — Python SDK with async/sync workers, transactional enqueue, and progress tracking. Install awa-pg[ui] to add the bundled web dashboard."
 readme = "README.md"
 license = {text = "MIT OR Apache-2.0"}
@@ -34,7 +34,7 @@ classifiers = [
 #
 # Kept opt-in so the default `awa-pg` install stays small — workers and
 # producers don't need the ~10 MB UI bundle.
-ui = ["awa-cli==0.6.15"]
+ui = ["awa-cli==0.6.16"]
 
 [project.urls]
 Homepage = "https://github.com/hardbyte/awa"

diff --git a/awa-python/uv.lock b/awa-python/uv.lock
diff --git a/awa-seaorm/Cargo.toml b/awa-seaorm/Cargo.toml
@@ -14,6 +14,6 @@ serde_json.workspace = true
 sqlx.workspace = true
 
 [dev-dependencies]
-awa-testing = { path = "../awa-testing", version = "0.6.15" }
+awa-testing = { path = "../awa-testing", version = "0.6.16" }
 serde = { workspace = true, features = ["derive"] }
 tokio = { workspace = true, features = ["macros", "rt-multi-thread"] }
diff --git a/awa/Cargo.toml b/awa/Cargo.toml
@@ -20,7 +20,7 @@ awa-macros.workspace = true
 awa-worker.workspace = true
 
 [dev-dependencies]
-awa-testing = { path = "../awa-testing", version = "0.6.15" }
+awa-testing = { path = "../awa-testing", version = "0.6.16" }
 sqlx.workspace = true
 serde.workspace = true
 serde_json.workspace = true

diff --git a/correctness/README.md b/correctness/README.md
@@ -48,7 +48,7 @@ What is intentionally not modeled:
 - `storage/AwaSegmentedStorageRaces.tla` / `storage/AwaSegmentedStorageRaces.cfg` / `storage/AwaSegmentedStorageRacesSafe.cfg`: focused race-exposure spec that splits `Claim` into `BeginClaim` / `CommitClaim` to model the claim path's cursor-read-without-lock behaviour. The race config produces a counterexample trace (claim snapshots segment, rotate+prune fire, commit lands lease in pruned segment — simultaneously the claim-vs-rotate race and the prune check-then-act race). The safe config uses a checked commit and passes. Production uses CAS on ring state plus child-partition locks and busy checks, not `FOR SHARE` on `lease_ring_state` — see `storage/MAPPING.md` for the full analysis.
 - `storage/AwaShardedPrune.tla` / `storage/AwaShardedPrune.cfg` / `storage/AwaShardedPruneBroken.cfg`: focused ADR-025 regression model for queue-ring prune across enqueue shards. The passing config requires ready rows to match done rows by `(enqueue_shard, lane_seq)` before prune can drop a sealed queue slot. The broken config intentionally ignores `enqueue_shard` and produces the historical counterexample: shard 0 has a done row at `lane_seq = 1`, shard 1 still has a pending ready row at `lane_seq = 1`, and broken prune drops both.
 - `storage/AwaPartitionedQueueRouting.tla` / `storage/AwaPartitionedQueueRouting.cfg` / `storage/AwaPartitionedQueueRoutingBroken.cfg`: focused ADR-031 routing model for `PartitionedQueue`. Partitioned queues remain client-side routing over ordinary Awa queues, so this spec checks the refinement boundary above storage: abstract key hashes route to their selected partition, the same base hash still determines the enqueue shard inside that partition, lane sequence identity stays scoped to `(partition, shard)`, and the configured hash domain reaches every shard from every partition. The broken config reuses the base hash modulo at both routing levels and demonstrates the correlated-hash defect.
-- `storage/AwaStorageLockOrder.tla` / `storage/AwaStorageLockOrder.cfg` / `storage/AwaStorageLockOrderDeadlockDemo.cfg` / `storage/AwaStorageLockOrderOldStripedClaimDeadlock.cfg`: lock-ordering protocol spec. Models each storage-engine transaction (enqueue, claim, complete, close-receipt, rescue-receipts, ensure-running, cancel, rotate, and prune) as an ordered sequence of Postgres lock acquisitions with a shared/exclusive compatibility matrix. The striped enqueue path takes multiple physical queue lanes in stable order; the current striped claim path takes at most one physical stripe per transaction. Checks `NoDeadlock` via a waits-for cycle detector. The demo configs use a deliberately cycle-creating plan pair and the historical old striped logical-claim plan to prove the detector catches real cycles.
+- `storage/AwaStorageLockOrder.tla` / `storage/AwaStorageLockOrder.cfg` / `storage/AwaStorageLockOrderDeadlockDemo.cfg` / `storage/AwaStorageLockOrderOldStripedClaimDeadlock.cfg` / `storage/AwaStorageLockOrderOldLaneProvisioningDeadlock.cfg`: lock-ordering protocol spec. Models each storage-engine transaction (enqueue, first enqueue to a new lane, claim, complete, close-receipt, rescue-receipts, ensure-running, cancel, rotate, and prune) as an ordered sequence of Postgres lock acquisitions with a shared/exclusive compatibility matrix. The striped enqueue path takes multiple physical queue lanes in stable order; the current striped claim path takes at most one physical stripe per transaction. Checks `NoDeadlock` via a waits-for cycle detector. The first enqueue to a new lane takes its `queue_lanes` row, then its provisioning lock, then its enqueue lock, in every producer. The demo configs use a deliberately cycle-creating plan pair, the historical old striped logical-claim plan, and the historical `QueueStorage` lane-provisioning order (provisioning lock before the row) to prove the detector catches real cycles.
 - `storage/AwaCanonicalUniqueRescue.tla` / `storage/AwaCanonicalUniqueRescue.cfg` / `storage/AwaCanonicalUniqueRescueBatchOnly.cfg`: focused model for the canonical rescue sweeps versus the unique-claim trigger. A unique job with a pending-only `unique_states` mask is stuck running while a duplicate holds the claim; the batched rescue is blocked forever (BatchOnly config: expected `Convergence` liveness counterexample — the production wedge fixed in 0.6.1), while the per-row fallback rescues the innocent job and cancels the superseded one (main config passes, `ClaimConsistency` holds in both).
 - `storage/AwaStorageTransition.tla` / `storage/AwaStorageTransition.cfg` / `storage/AwaStorageTransitionCurrentGate.cfg`: focused model for the 0.5.x-to-0.6 storage transition control plane. It covers prepare, schema readiness, mixed-transition entry, canonical backlog drain, queue-storage routing, finalize, and abort interlocks. The desired config matches the v014 entry gate and v040 finalization gate: a live queue-storage target is required before routing flips, while drained pre-flip auto runtimes may remain idle through finalization. The `CurrentGate`-named config is a historical pre-v014 regression witness for the old capability-only entry gate.
 - `storage/AwaSegmentedStorageTrace.tla` / `storage/AwaSegmentedStorageTrace.cfg` / `storage/AwaSegmentedStorageTraceReceiptRescue.cfg` / `storage/AwaSegmentedStorageTraceLostClaimAdvance.cfg` / `storage/AwaSegmentedStorageTraceRunningCancel.cfg` / `storage/AwaSegmentedStorageTraceReceiptOnlyCancel.cfg` / `storage/AwaSegmentedStorageTraceCallbackWait.cfg` / `storage/AwaSegmentedStorageTraceDlqRetry.cfg` / `storage/AwaSegmentedStorageTraceDlqPurge.cfg` / `storage/AwaSegmentedStorageTraceBroken.cfg`: trace-validation harness. Takes hand-transcribed sequences of queue-storage runtime events and verifies each transition is accepted by the storage spec. Current positive traces cover snooze, receipt rescue, running cancel, receipt-only cancel, callback wait/resume, DLQ retry, and DLQ purge. A deliberately-broken variant trips deadlock at traceIdx = 2 to confirm the checker rejects invalid sequences.
@@ -108,6 +108,7 @@ Expected counterexample or positive-witness configs:
 ./correctness/run-tlc.sh storage/AwaPartitionedQueueRouting.tla storage/AwaPartitionedQueueRoutingBroken.cfg
 ./correctness/run-tlc.sh storage/AwaStorageLockOrder.tla storage/AwaStorageLockOrderDeadlockDemo.cfg
 ./correctness/run-tlc.sh storage/AwaStorageLockOrder.tla storage/AwaStorageLockOrderOldStripedClaimDeadlock.cfg
+./correctness/run-tlc.sh storage/AwaStorageLockOrder.tla storage/AwaStorageLockOrderOldLaneProvisioningDeadlock.cfg
 ./correctness/run-tlc.sh storage/AwaStorageTransition.tla storage/AwaStorageTransitionCurrentGate.cfg
 ./correctness/run-tlc.sh storage/AwaShardedPrune.tla storage/AwaShardedPruneBroken.cfg
 ```

diff --git a/correctness/run-tlc-suite.sh b/correctness/run-tlc-suite.sh
@@ -32,6 +32,8 @@ AwaSegmentedStorageTrace.tla   ;; AwaSegmentedStorageTraceDlqPurge.cfg    ;; Dlq
 AwaSegmentedStorageTrace.tla   ;; AwaSegmentedStorageTraceBroken.cfg      ;; Deadlock reached ;; broken trace rejected
 AwaStorageLockOrder.tla        ;; AwaStorageLockOrder.cfg                 ;; pass ;; lock ordering
 AwaStorageLockOrder.tla        ;; AwaStorageLockOrderDeadlockDemo.cfg     ;; NoDeadlock is violated ;; deadlock detector witness
+AwaStorageLockOrder.tla        ;; AwaStorageLockOrderOldStripedClaimDeadlock.cfg ;; NoDeadlock is violated ;; old striped-claim order witness
+AwaStorageLockOrder.tla        ;; AwaStorageLockOrderOldLaneProvisioningDeadlock.cfg ;; NoDeadlock is violated ;; old QueueStorage lane-provisioning order witness
 AwaDeadTupleContract.tla       ;; AwaDeadTupleContract.cfg                ;; pass ;; architectural reclaim contract
 AwaStorageTransition.tla       ;; -                                       ;; pass ;; transition control plane + #456 reschedule drain
 AwaQuiescedTransition.tla      ;; -                                       ;; pass ;; quiesced routing flip serializes snapshot evidence