[Fix] Unit tests report teardown errors after Task cleanup

docs/architecture/task-cleanup-protocol-model.md

@@ -0,0 +1,33 @@
+# Task cleanup protocol model check
+
+Zoo Code checks the in-memory task cleanup protocol with a bounded explicit-state explorer. It runs under the umbrella command:
+
+```sh
+pnpm lifecycle:model-check
+```
+
+For focused debugging, run:
+
+```sh
+pnpm cleanup-protocol:model-check
+```
+
+This is a separate child model from the persisted task lifecycle and shared-store concurrency models. It follows the native tool-call parser model pattern: keep an independent bounded state space for an independent protocol, require every action and semantic landmark to remain reachable, and connect the abstract claims to focused production tests.
+
+## Bounds and environment actions
+
+The model uses two tasks and explores every reachable interleaving through depth 20, with an explicit 100,000-state budget. Abort, disposal, final-save, provider abort/drain phases, and shutdown-cursor state are modeled directly. Independent abort and disposal calls may interleave freely, while provider-initiated calls are gated to the current shutdown task. Cleanup and editor-reversion settlement or rejection are environment actions, so the explorer does not assume they eventually occur.
+
+The model checks these finite safety properties:
+
+1. repeated abort and disposal calls reuse their first logical handle and start each operation at most once;
+2. final message persistence, or the history-task save skip, cannot occur before editor reversion settles or rejects;
+3. abort may complete while ancillary output cleanup remains pending;
+4. disposal completes only after cleanup and reversion both settle or reject;
+5. provider shutdown advances through tasks only after each task's abort and disposal reach terminal states;
+6. shutdown advances through tasks in registry order and is complete exactly when every modeled task is drained; and
+7. abort, ancillary cleanup, or disposal-start rejection is isolated so shutdown can continue to later tasks.
+
+Named landmarks require abort completion during pending ancillary cleanup, contained cleanup rejection, final-save attempt after rejected reversion, a history-task final-save skip, two-task shutdown completion, and shutdown continuation after rejected abort, ancillary cleanup, or disposal start.
+
+These are bounded safety and reachability claims only. The model does not claim filesystem or editor Promise liveness, fairness, timing bounds, arbitrary task counts, or that cleanup can never remain pending. Deterministic Vitest coverage in `Task.dispose.test.ts`, `Task.spec.ts`, and `ClineProvider.spec.ts` exercises the corresponding production Promise identities, ordering, rejection handling, and multi-task shutdown behavior.

docs/architecture/task-lifecycle-model.md

@@ -63,6 +63,10 @@ The known-unsafe witnesses currently compare exact shortest action sequences. Th
 
 `TaskHistoryStore.realConcurrency.spec.ts` complements the abstract interleavings with one synchronized integration smoke check through the real `proper-lockfile` and filesystem rename path; broader VS Code E2E remains reserved for restart and extension-host behavior.
 
+## Task cleanup protocol model
+
+The umbrella command also runs a separate bounded child model for in-memory abort, disposal, and provider-shutdown ordering. It models cleanup settlement and rejection as environment transitions and makes no filesystem, editor Promise, fairness, or timing-liveness claim. See [Task cleanup protocol model check](./task-cleanup-protocol-model.md).
+
 ## Invariants
 
 The checker currently enforces:

package.json

@@ -13,7 +13,8 @@
 		"check-types": "turbo check-types --log-order grouped --output-logs new-only",
 		"test": "turbo test --log-order grouped --output-logs new-only",
 		"test:mutation-ci": "node --test scripts/stryker-diff.test.mjs",
-		"lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts",
+		"lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts && pnpm cleanup-protocol:model-check",
+		"cleanup-protocol:model-check": "tsx scripts/check-task-cleanup-protocol.ts",
 		"test:coverage": "turbo test:coverage --log-order grouped --output-logs new-only",
 		"format": "turbo format --log-order grouped --output-logs new-only",
 		"build": "turbo build --log-order grouped --output-logs new-only",

packages/types/src/task.ts

@@ -128,7 +128,7 @@ export interface TaskLike {
 	approveAsk(options?: { text?: string; images?: string[] }): void
 	denyAsk(options?: { text?: string; images?: string[] }): void
 	submitUserMessage(text: string, images?: string[], mode?: string, providerProfile?: string): Promise<void>
-	abortTask(): void
+	abortTask(): Promise<void>
 }
 
 export type TaskEvents = {