AIDAWORK / WORKFLOW

Work 控制面四层平面与形式化安全不变式 (C0 / W0 / O1 / E0)

先看「视图」里的主路径；每条失败链都有同名成功对偶（fail-x ↔ ok-x）。

机制说明（SoT）图是辅读 · 结论以说明与证据为准

| 对象 | 写入权威 | 读取 / 投影 | 恢复依据 | |---|---|---|---| | Run | Agent agent_runs（可更新状态 + lease） | Chat SSE / 在办投影 | lease + recoverExpiredLeaseByConversation | | Interaction | InteractionKernel + PG store | 待办 / Desktop 展示 | settle / resume outbox | | Message Center | NotificationService 写 notifications | SSE 收件箱 |…

本页可直接往下读完整机制说明，不需要「演示 / 播放故事」。术语不熟先看术语表。

先读机制说明，结论以说明与证据为准 · 基于固定代码版本核验 · 部署状态另行确认

机制说明（全文）

状态权威矩阵

SoT 与读模型分开读

对象	写入权威	读取 / 投影	恢复依据
Run	Agent `agent_runs`（可更新状态 + lease）	Chat SSE / 在办投影	lease + `recoverExpiredLeaseByConversation`
Interaction	`InteractionKernel` + PG store	待办 / Desktop 展示	settle / resume outbox
Message Center	`NotificationService` 写 notifications	SSE 收件箱	读模型；不替代上游业务终态
LF Operation	Agent `local_file_operations`	Desktop 执行与回执	Operation + wake；路径只在 Main
Plugin receipt	Agent 绑定字段校验 `parseBoundPluginReply`	Host settle 回传	绑定 digest 不一致则拒绝
Desktop 本地投影	Main AtomicJsonStore（write-state / 授权夹）	Renderer 只读投影	不授权服务端工作；不跨设备
原工作（runtime-work-v1）	`agent_runs.command_envelope` + `original_root_run_id` + work 效果位置（C0 冻结）	workbench / 观察投影	`bindAdmittedWork` 准入；共同控制挂起/终态；补证不换 owner

权威写入在 Agent（及 Main 对本机文件事实）；Desktop 本地仓是装置级投影，Message Center 是通知读模型。恢复只读各自 SoT，不能用投影反写。普通 Skill 效果与业务任务受理已拆分：钉点 Agent e2adc9a3c325 删除了 userSkillBinding，skill_bound 只看 businessTaskBinding；不得用任务闭环假设套到无任务 Skill。

失败 / 崩溃读路径

acquireLease / takeOverExpiredLease：条件 UPDATE，仅 pending|running|pending_resume|suspended 且未 finished。
recoverExpiredLeaseByConversation：先保护 durable local-read / interaction 相关 run，再关闭只等过期卡的 legacy 任务树（见下节），然后对过期 lease 的父 run 做手动恢复；读路径仍以 agent_runs 为准。
崩溃后 Desktop 重连只拉取投影 / 续传回执，不重建服务端 SoT。

只等过期卡的任务树（钉点 e2adc9a3c325）

此前挂起（suspended / pending_resume）的顶层 Run 只要还在等一张已过期的卡，就一直占着会话，后续每轮都被 CONCURRENT_RUN 拒绝，而过期卡本身又不能再答。现在 closeRunsWaitingOnlyOnExpiredInteractions 负责收口：

调用点：ChatSubmissionStore 受理新消息时，在持有会话行锁的同一事务里、占用检查之前调用（带 actor）；recoverExpiredLeaseByConversation 也调用，但不带 actor，只处理 legacy 树。
fail-closed：只有树绑定到 expired 卡，且没有任何可答或结算中的卡（pending 卡、24h 宽限内的 authorize 过期卡、settlement attempt、resume outbox / command）、没有进行中的旁路查询、成员不归其他 owner（pending_interactions、ActionProposal、continuation、LF requested、已派发模型请求、business task 等）时才关；被别的事务锁住的根 SKIP LOCKED 跳过；钉点 e2adc9a3c325 起（ADR-0094，Agent 9a3e49ec1）还要先以不等待的方式锁住整棵成员树，任一成员被占用本次就不收口，留给下一次提交，持会话锁时不再阻塞等待已有 run。
两种收口：legacy 树（run_kind 为空）置 expired / INTERACTION_EXPIRED；Runtime Work 根不走 expired，由 stopRuntimeWorkSupersededByNewTurnInTx 以用户 Stop 收口（新一轮提交即 owner 的取代意图）。Desktop 侧的「结束原任务」见 desktop-client。

归属边与非目标

Owner：各 SoT 行的写入模块；投影层无写回权。
非目标：不展开 Message Center 扇出协议细节（见 message-center）；不替代 ledger-authority 的事件账本语义。
相关：ledger-authority、interaction-lifecycle、message-center、enterprise-task-e2e、storage-planes。

视图

main — SoT vs 读模型 / 本机投影矩阵图。
recovery — lease 过期与会话级恢复读路径。
fail-lease — recoverExpiredLease 成功分叉 vs 再 acquire 失败。
fail-concurrent — 并发写者 / 错绑定回执拒收。
ok-lease — 持有 lease 写终态并释放（对偶 fail-lease）。
ok-concurrent — 单写者 + 合法回执落账（对偶 fail-concurrent）。
work-control-planes — Work 控制面四层平面（C0 / W0 / O1 / E0）与形式化安全不变式。
stop-vs-late-receipt — Stop 抢占、未决目标绑定与迟到本机回执「落账不唤醒」并发冲突裁决。
tla-verification-matrix — 三仓 TLA+ 形式化验证全景：从会话入队、Work 控制到本机单次副作用与插件准入零写入核验。

Work 控制面四层平面与安全不变式（C0 / W0 / O1 / E0）

Runtime Work 的状态转移按四层平面解耦（见视图 work-control-planes）：

C0 命令平面（bindAdmittedWork / requestRuntimeWorkStop）：在受理事务中冻结 command_envelope 与初始 C0 效应（runtimeWorkEffects）；显式停止（requestRuntimeWorkStop）或新轮取代（stopRuntimeWorkSupersededByNewTurnInTx）精确指向原 rootRunId。
W0 编排平面（withRuntimeWorkRoot / activateRuntimeWorkFromAcceptedSettlement）：在 Root 行锁下串行化状态迁移并单调递增 control_revision；外部回执或交互结算仅在与当前活跃等待严格匹配时才能唤醒 Work（settleRuntimeWorkSkillReceiptInTx / activateRuntimeWorkFromAcceptedSettlement）。
O1 尝试与 Provider 回退平面（selectWorkProviderAttemptInTx / admitWorkProviderAttemptInTx）：每次模型或工具尝试绑定当前 claim fence，保证单次尝试至多下发一次请求；Provider 故障切换仅在拿到未发出或未响应证明（getWorkProviderAttemptObservation：not_dispatched / stopped_before_response）后才允许回退。
E0 外部效应与终态平面（finishRuntimeWorkCarrierInTx / readConditionalArtifactCompletionInTx）：外部写账本通过激活态 Run CAS（markExecuting）防重放，终态收口前复核条件产物与 Stop 状态，已停止或已终态的 Work 严禁再推进外部写入。

三大并发竞态与崩溃恢复深挖（`stop-vs-late-receipt`）

并发/故障场景	Desktop Main 持久化屏障	PostgreSQL 事务锁与状态跳变（`run-work-control.ts`）	为什么不会脑裂或丢账？
1. Stop 撞上在途提交或迟到本机回执（见视图 `stop-vs-late-receipt`）	`RuntimeWorkDelivery.stop` 先写 `prepareStop (phase='unresolved')`；若原提交尚未拿到 `acceptedBinding`，先调 `transport.query(submission)` 查回 `rootRunId`，再 `bindStopTarget (phase='prepared')` 冻结 `{stopCommandId, rootRunId, sourceRef}`，且不确定时只走 `queryStop` 绝不盲重发。	1) Stop 到达：`requestRuntimeWorkStopInTx` 锁 Root 写 `agent_runs.cancel_intent`，`convergeStoppedWorkInTx` 锁全树成员，将所有 `pending / running / suspended / manual_recovery` 载体置为 `status='cancelled', completion_outcome='cancelled'`，并取消未认领的 `conversation_interaction_resume_commands`。<br>2) 本机迟到回执随后到达：`settleRuntimeWorkSkillReceiptInTx` 仍执行 7 表 Join、写 `runtime_work_domain_facts`、插 `messages (role='tool')`、置 `continuation_requests.status='completed'`；但因 `canActivate = (root.cancel_intent === null && carrier.status === 'suspended')` 为 `false`，直接返回 `{ status: 'held' }`。	证据落账与执行唤醒完全解耦：迟到的真实副作用证据被完整记入账本并释放 Desktop 重传队列，但绝不撤销 Stop 或把 `cancelled` 载体重新改回 `pending`。
2. Worker 崩溃 / Lease 过期后的五路精确自愈	Desktop 观察流检测到 lease 过期或重连时只拉取 `view()`，绝不从客户端发起重跑。	`recoverExpiredWorkCarrier` 在 `lockRoot` 下检查 `lease_expires_at <= clock_timestamp()` 的 `running` 载体，依次探测 5 类可自愈证据：<br>① `expiredOriginalConsumerRecoveryCodeInTx`<br>② `expiredChildEffectRecoveryCode`<br>③ `expiredPluginActionRecoveryCode`（`resume_point='plugin_action_ready'` 且尚未生成 `continuation_requests`）<br>④ `expiredProviderAttemptRecoveryCode`（`runtime_work_provider_attempts.state === 'stopped'` 且 `nextProviderAttemptIndex` 在 `route_chain` 内）<br>⑤ `expiredModelRebuildRecoveryCode`<br>命中任一自愈码则 `requeue = true`（`status: 'running' -> 'pending'`, `replayable = false`）；若均不命中（如 `model_request_state='dispatched'` 但 Provider 状态未知），则 fail-closed 置为 `status = 'manual_recovery'` 并写入 `explainWorkBlockInTx`。	只允许在已证实未产生未知外部副作用的精确断点冷重建（Cold Reconstruction）；一旦模型请求处于未知在途态，严禁盲目重发导致双倍扣费或重复工具调用。
3. 跨载体分段续跑（Carrier Handoff）	对客户端透明，客户端始终锚定不变的 `originalWorkRef.rootRunId`。	当一次交互或后台阶段需要切换执行载体时，先锁前驱载体 `lockCarrier(predecessorRunId)`，验证 `predecessor.original_root_run_id === rootRunId` 且 `status === 'pending'`，将前驱置为 `status = 'completed', completion_outcome = 'continued'`（注意：`continued` 仅代表执行分段结束，绝非原工作成功），再插入新 `agent_runs`（`original_root_run_id = rootRunId, continuation_predecessor_run_id = predecessorRunId`）与继承 `continuation_context` 的新 `runtime_invocations`。	Root 身份与执行分段（Carrier Segment）分离：无论历经多少次挂起、唤醒或子阶段移交，Stop、配额、领域事实与条件产物校验始终收敛在同一个 `original_root_run_id` 下。

成功对偶（与失败链入口相同）

ok-lease：acquireLease/renewLease 成功 → 终态 completed → releaseLease；Desktop 只读投影。
ok-concurrent：唯持有者写入；parseBoundPluginReply 返回合法 reply 后落账。

失败链（深挖）

fail-lease：会话 recover → 保护集外 manual_recovery|failed；随后 acquireLease null → BUSY。
fail-concurrent：条件 UPDATE 拒第二写者 → CONCURRENT_RUN/BUSY；Desktop 无写 agent_runs；parseBoundPluginReply null 拒错 SoT 回执。

证据与范围

aida-agent · packages/agent/src/session/run-store.ts L651–681 · acquireLease · e2adc9a3c325
aida-agent · packages/agent/src/session/run-store.ts L1933–1968 · recoverExpiredLeaseByConversation · e2adc9a3c325
aida-agent · packages/agent/src/session/expired-interaction-closure.ts L4–55 · Fail-closed · e2adc9a3c325
aida-agent · packages/agent/src/session/expired-interaction-closure.ts L223–261 · INTERACTION_EXPIRED · e2adc9a3c325
aida-agent · packages/agent/src/session/chat-submission-store.ts L541–556 · closeRunsWaitingOnlyOnExpiredInteractions · e2adc9a3c325
aida-agent · packages/agent/src/runtime/work/run-work-control.ts L1724–1735 · stopRuntimeWorkSupersededByNewTurnInTx · e2adc9a3c325
aida-agent · packages/agent/src/interaction-kernel/kernel.ts L226–258 · InteractionKernel · e2adc9a3c325
aida-agent · packages/agent/src/interaction-kernel/kernel.ts L776–811 · settle · e2adc9a3c325
aida-agent · packages/agent/src/notifications/service.ts L26–56 · NOTIFICATION_NOTIFY_CHANNEL · e2adc9a3c325
aida-agent · packages/agent/src/session/local-file-operation-store.ts L214–245 · LocalFileOperationStore · e2adc9a3c325
aida-agent · packages/agent/src/runtime/local/plugin-tool-receipt.ts L33–64 · parseBoundPluginReply · e2adc9a3c325
aida-desktop · apps/desktop/electron/local-files-v4/write-record-store.ts L46–77 · WriteRecordStore · 4346d79eb364
aida-agent · packages/agent/src/gateway/unified-entry.ts L2773–2813 · CONCURRENT_RUN · e2adc9a3c325
aida-agent · packages/agent/src/gateway/unified-entry.ts L1948–1978 · RUN_LEASE_BUSY · e2adc9a3c325

结论来自固定版本的静态源码与合同阅读；实现存在、默认开关和生产启用分别判断。本站代码证据面板列出声明状态与具体限制。

会话 turn 队列（钉点 e2adc9a3c325）

迁移 191：conversation_turn_queue FIFO；会话仍有活跃执行时新 turn 入队（加密载荷），不放宽一会话一活跃索引。
ChatSubmissionStore 负责 insert / claim / mark admitted / fail / cancel；与 ADR-0098 可回访卡不同——队列是执行中的新消息缓冲，不是 parked 卡模型。

Agent 最新增量：条件产物（2026-10-29）

条件产物满足与否由 Work owner 从原请求、Kernel receipt、settlement fact 和原模型工具调用重建，并在原 claim fence 下再次核验。最近结果为 not_applicable 且没有任何产物时，可关闭条件产物要求；独立原文件读取仍必须完成。若有产物则须有对应读取证据，空列表、succeeded 外壳或模型终稿不能单独证明完成。此分支不是新增 RunStatus。

aida-agent · packages/agent/src/runtime/work/run-work-conditional-artifact.ts L47–152 · 7f2e519936b5
aida-agent · packages/agent/src/runtime/work/run-work-carrier-terminal.ts L10–28 · 7f2e519936b5

三仓 TLA+ 形式化验证全景（视图 `tla-verification-matrix`，2026-11-03）

三仓围绕「状态唯一权威与单次外部副作用」沉淀了跨服务端、桌面宿主与业务插件的 TLA+ 形式化规范矩阵：

仓库与平面	TLA+ 模型路径	核心安全不变式（Safety Invariant）
aida-agent（会话与控制面）	`TurnQueueFifo.tla`（本仓 `.agents/skills/formal-verification/`）<br>`specs/tla/work-control/WorkControl.tla` & `WorkRecoveryEligibility.tla`	单会话至多一个活跃执行；排队 turn 严格按 `queue_seq` FIFO 认领；Stop 抢占与迟到回执解耦（落账不唤醒）；仅在已证实无未知外部副作用的精确断点允许冷重建。
aida-agent（写权限与插件读续办）	`specs/tla/confirmed-write/ConfirmedWrite.tla` & `ConfirmedBatch.tla`<br>`.agents/skills/aida-plugin-read-continuation-verify/model/PluginRead.tla`	服务端连接器写入必须先核验凭据可用再执行 `markExecuting` CAS；插件续办待执行步骤（`pendingPluginToolCall`）仅在身份匹配且精确成功读取后才消费 `continuation` / `nextAction` 义务，写操作或缺参不释放义务。
aida-desktop（宿主单次副作用与槽位）	`.agents/skills/aida-desktop-plugin-call-once-verify/model/PluginCallOnce.tla`<br>`.agents/skills/aida-desktop-file-change-verify/model/FileChange.tla`<br>`.agents/skills/aida-desktop-chat-state-verify/model/ChatSlot.tla` & `ReplyMaterials.tla`	`PluginCallJournal` 在 `admitted → dispatched → settled` 下若 `!dispatched` 落盘失败显式抛 `PLUGIN_CALL_JOURNAL_UNAVAILABLE`，已派发非只读调用崩溃重启绝不二次重放；`FileChange.tla` 保证本机文件修改单次执行；`ChatSlot` / `ReplyMaterials` 保证桌面槽位与补证材料绑定无死锁。
aida-plugins（业务插件准入零写入）	`.agents/skills/aida-attendance-admission-verify/model/AdmissionOutcome.tla`	考勤核算在准入前（无规则基线、未采用草稿、缺少连接）确定性拒绝时 `writes = 0`，显式返回 `executionState = "completed"`，与 Desktop `PluginCallOnce` 衔接避免未发生副作用的业务拒绝被误判为 `unknown`。

aida-agent · .agents/skills/aida-plugin-read-continuation-verify/model/PluginRead.tla L1–31 · MODULE PluginRead · 7f2e519936b5
aida-agent · specs/tla/work-control/WorkControl.tla L1–40 · MODULE WorkControl · 7f2e519936b5
aida-desktop · .agents/skills/aida-desktop-plugin-call-once-verify/model/PluginCallOnce.tla L1–55 · MODULE PluginCallOnce · 4346d79eb364
aida-desktop · .agents/skills/aida-desktop-file-change-verify/model/FileChange.tla L1–50 · MODULE FileChange · 4346d79eb364
aida-plugins · .agents/skills/aida-attendance-admission-verify/model/AdmissionOutcome.tla L1–35 · MODULE AdmissionOutcome · a33ce3733365

状态权威矩阵

SoT 与读模型分开读

对象	写入权威	读取 / 投影	恢复依据
Run	Agent `agent_runs`（可更新状态 + lease）	Chat SSE / 在办投影	lease + `recoverExpiredLeaseByConversation`
Interaction	`InteractionKernel` + PG store	待办 / Desktop 展示	settle / resume outbox
Message Center	`NotificationService` 写 notifications	SSE 收件箱	读模型；不替代上游业务终态
LF Operation	Agent `local_file_operations`	Desktop 执行与回执	Operation + wake；路径只在 Main
Plugin receipt	Agent 绑定字段校验 `parseBoundPluginReply`	Host settle 回传	绑定 digest 不一致则拒绝
Desktop 本地投影	Main AtomicJsonStore（write-state / 授权夹）	Renderer 只读投影	不授权服务端工作；不跨设备
原工作（runtime-work-v1）	`agent_runs.command_envelope` + `original_root_run_id` + work 效果位置（C0 冻结）	workbench / 观察投影	`bindAdmittedWork` 准入；共同控制挂起/终态；补证不换 owner

失败 / 崩溃读路径

acquireLease / takeOverExpiredLease：条件 UPDATE，仅 pending|running|pending_resume|suspended 且未 finished。
recoverExpiredLeaseByConversation：先保护 durable local-read / interaction 相关 run，再关闭只等过期卡的 legacy 任务树（见下节），然后对过期 lease 的父 run 做手动恢复；读路径仍以 agent_runs 为准。
崩溃后 Desktop 重连只拉取投影 / 续传回执，不重建服务端 SoT。

只等过期卡的任务树（钉点 e2adc9a3c325）

调用点：ChatSubmissionStore 受理新消息时，在持有会话行锁的同一事务里、占用检查之前调用（带 actor）；recoverExpiredLeaseByConversation 也调用，但不带 actor，只处理 legacy 树。
fail-closed：只有树绑定到 expired 卡，且没有任何可答或结算中的卡（pending 卡、24h 宽限内的 authorize 过期卡、settlement attempt、resume outbox / command）、没有进行中的旁路查询、成员不归其他 owner（pending_interactions、ActionProposal、continuation、LF requested、已派发模型请求、business task 等）时才关；被别的事务锁住的根 SKIP LOCKED 跳过；钉点 e2adc9a3c325 起（ADR-0094，Agent 9a3e49ec1）还要先以不等待的方式锁住整棵成员树，任一成员被占用本次就不收口，留给下一次提交，持会话锁时不再阻塞等待已有 run。
两种收口：legacy 树（run_kind 为空）置 expired / INTERACTION_EXPIRED；Runtime Work 根不走 expired，由 stopRuntimeWorkSupersededByNewTurnInTx 以用户 Stop 收口（新一轮提交即 owner 的取代意图）。Desktop 侧的「结束原任务」见 desktop-client。

归属边与非目标

Owner：各 SoT 行的写入模块；投影层无写回权。
非目标：不展开 Message Center 扇出协议细节（见 message-center）；不替代 ledger-authority 的事件账本语义。
相关：ledger-authority、interaction-lifecycle、message-center、enterprise-task-e2e、storage-planes。

视图

main — SoT vs 读模型 / 本机投影矩阵图。
recovery — lease 过期与会话级恢复读路径。
fail-lease — recoverExpiredLease 成功分叉 vs 再 acquire 失败。
fail-concurrent — 并发写者 / 错绑定回执拒收。
ok-lease — 持有 lease 写终态并释放（对偶 fail-lease）。
ok-concurrent — 单写者 + 合法回执落账（对偶 fail-concurrent）。
work-control-planes — Work 控制面四层平面（C0 / W0 / O1 / E0）与形式化安全不变式。
stop-vs-late-receipt — Stop 抢占、未决目标绑定与迟到本机回执「落账不唤醒」并发冲突裁决。
tla-verification-matrix — 三仓 TLA+ 形式化验证全景：从会话入队、Work 控制到本机单次副作用与插件准入零写入核验。

Work 控制面四层平面与安全不变式（C0 / W0 / O1 / E0）

Runtime Work 的状态转移按四层平面解耦（见视图 work-control-planes）：

C0 命令平面（bindAdmittedWork / requestRuntimeWorkStop）：在受理事务中冻结 command_envelope 与初始 C0 效应（runtimeWorkEffects）；显式停止（requestRuntimeWorkStop）或新轮取代（stopRuntimeWorkSupersededByNewTurnInTx）精确指向原 rootRunId。
W0 编排平面（withRuntimeWorkRoot / activateRuntimeWorkFromAcceptedSettlement）：在 Root 行锁下串行化状态迁移并单调递增 control_revision；外部回执或交互结算仅在与当前活跃等待严格匹配时才能唤醒 Work（settleRuntimeWorkSkillReceiptInTx / activateRuntimeWorkFromAcceptedSettlement）。
O1 尝试与 Provider 回退平面（selectWorkProviderAttemptInTx / admitWorkProviderAttemptInTx）：每次模型或工具尝试绑定当前 claim fence，保证单次尝试至多下发一次请求；Provider 故障切换仅在拿到未发出或未响应证明（getWorkProviderAttemptObservation：not_dispatched / stopped_before_response）后才允许回退。
E0 外部效应与终态平面（finishRuntimeWorkCarrierInTx / readConditionalArtifactCompletionInTx）：外部写账本通过激活态 Run CAS（markExecuting）防重放，终态收口前复核条件产物与 Stop 状态，已停止或已终态的 Work 严禁再推进外部写入。

三大并发竞态与崩溃恢复深挖（`stop-vs-late-receipt`）

并发/故障场景	Desktop Main 持久化屏障	PostgreSQL 事务锁与状态跳变（`run-work-control.ts`）	为什么不会脑裂或丢账？
1. Stop 撞上在途提交或迟到本机回执（见视图 `stop-vs-late-receipt`）	`RuntimeWorkDelivery.stop` 先写 `prepareStop (phase='unresolved')`；若原提交尚未拿到 `acceptedBinding`，先调 `transport.query(submission)` 查回 `rootRunId`，再 `bindStopTarget (phase='prepared')` 冻结 `{stopCommandId, rootRunId, sourceRef}`，且不确定时只走 `queryStop` 绝不盲重发。	1) Stop 到达：`requestRuntimeWorkStopInTx` 锁 Root 写 `agent_runs.cancel_intent`，`convergeStoppedWorkInTx` 锁全树成员，将所有 `pending / running / suspended / manual_recovery` 载体置为 `status='cancelled', completion_outcome='cancelled'`，并取消未认领的 `conversation_interaction_resume_commands`。<br>2) 本机迟到回执随后到达：`settleRuntimeWorkSkillReceiptInTx` 仍执行 7 表 Join、写 `runtime_work_domain_facts`、插 `messages (role='tool')`、置 `continuation_requests.status='completed'`；但因 `canActivate = (root.cancel_intent === null && carrier.status === 'suspended')` 为 `false`，直接返回 `{ status: 'held' }`。	证据落账与执行唤醒完全解耦：迟到的真实副作用证据被完整记入账本并释放 Desktop 重传队列，但绝不撤销 Stop 或把 `cancelled` 载体重新改回 `pending`。
2. Worker 崩溃 / Lease 过期后的五路精确自愈	Desktop 观察流检测到 lease 过期或重连时只拉取 `view()`，绝不从客户端发起重跑。	`recoverExpiredWorkCarrier` 在 `lockRoot` 下检查 `lease_expires_at <= clock_timestamp()` 的 `running` 载体，依次探测 5 类可自愈证据：<br>① `expiredOriginalConsumerRecoveryCodeInTx`<br>② `expiredChildEffectRecoveryCode`<br>③ `expiredPluginActionRecoveryCode`（`resume_point='plugin_action_ready'` 且尚未生成 `continuation_requests`）<br>④ `expiredProviderAttemptRecoveryCode`（`runtime_work_provider_attempts.state === 'stopped'` 且 `nextProviderAttemptIndex` 在 `route_chain` 内）<br>⑤ `expiredModelRebuildRecoveryCode`<br>命中任一自愈码则 `requeue = true`（`status: 'running' -> 'pending'`, `replayable = false`）；若均不命中（如 `model_request_state='dispatched'` 但 Provider 状态未知），则 fail-closed 置为 `status = 'manual_recovery'` 并写入 `explainWorkBlockInTx`。	只允许在已证实未产生未知外部副作用的精确断点冷重建（Cold Reconstruction）；一旦模型请求处于未知在途态，严禁盲目重发导致双倍扣费或重复工具调用。
3. 跨载体分段续跑（Carrier Handoff）	对客户端透明，客户端始终锚定不变的 `originalWorkRef.rootRunId`。	当一次交互或后台阶段需要切换执行载体时，先锁前驱载体 `lockCarrier(predecessorRunId)`，验证 `predecessor.original_root_run_id === rootRunId` 且 `status === 'pending'`，将前驱置为 `status = 'completed', completion_outcome = 'continued'`（注意：`continued` 仅代表执行分段结束，绝非原工作成功），再插入新 `agent_runs`（`original_root_run_id = rootRunId, continuation_predecessor_run_id = predecessorRunId`）与继承 `continuation_context` 的新 `runtime_invocations`。	Root 身份与执行分段（Carrier Segment）分离：无论历经多少次挂起、唤醒或子阶段移交，Stop、配额、领域事实与条件产物校验始终收敛在同一个 `original_root_run_id` 下。

成功对偶（与失败链入口相同）

ok-lease：acquireLease/renewLease 成功 → 终态 completed → releaseLease；Desktop 只读投影。
ok-concurrent：唯持有者写入；parseBoundPluginReply 返回合法 reply 后落账。

失败链（深挖）

fail-lease：会话 recover → 保护集外 manual_recovery|failed；随后 acquireLease null → BUSY。
fail-concurrent：条件 UPDATE 拒第二写者 → CONCURRENT_RUN/BUSY；Desktop 无写 agent_runs；parseBoundPluginReply null 拒错 SoT 回执。

证据与范围

aida-agent · packages/agent/src/session/run-store.ts L651–681 · acquireLease · e2adc9a3c325
aida-agent · packages/agent/src/session/run-store.ts L1933–1968 · recoverExpiredLeaseByConversation · e2adc9a3c325
aida-agent · packages/agent/src/session/expired-interaction-closure.ts L4–55 · Fail-closed · e2adc9a3c325
aida-agent · packages/agent/src/session/expired-interaction-closure.ts L223–261 · INTERACTION_EXPIRED · e2adc9a3c325
aida-agent · packages/agent/src/session/chat-submission-store.ts L541–556 · closeRunsWaitingOnlyOnExpiredInteractions · e2adc9a3c325
aida-agent · packages/agent/src/runtime/work/run-work-control.ts L1724–1735 · stopRuntimeWorkSupersededByNewTurnInTx · e2adc9a3c325
aida-agent · packages/agent/src/interaction-kernel/kernel.ts L226–258 · InteractionKernel · e2adc9a3c325
aida-agent · packages/agent/src/interaction-kernel/kernel.ts L776–811 · settle · e2adc9a3c325
aida-agent · packages/agent/src/notifications/service.ts L26–56 · NOTIFICATION_NOTIFY_CHANNEL · e2adc9a3c325
aida-agent · packages/agent/src/session/local-file-operation-store.ts L214–245 · LocalFileOperationStore · e2adc9a3c325
aida-agent · packages/agent/src/runtime/local/plugin-tool-receipt.ts L33–64 · parseBoundPluginReply · e2adc9a3c325
aida-desktop · apps/desktop/electron/local-files-v4/write-record-store.ts L46–77 · WriteRecordStore · 4346d79eb364
aida-agent · packages/agent/src/gateway/unified-entry.ts L2773–2813 · CONCURRENT_RUN · e2adc9a3c325
aida-agent · packages/agent/src/gateway/unified-entry.ts L1948–1978 · RUN_LEASE_BUSY · e2adc9a3c325

结论来自固定版本的静态源码与合同阅读；实现存在、默认开关和生产启用分别判断。本站代码证据面板列出声明状态与具体限制。

会话 turn 队列（钉点 e2adc9a3c325）

迁移 191：conversation_turn_queue FIFO；会话仍有活跃执行时新 turn 入队（加密载荷），不放宽一会话一活跃索引。
ChatSubmissionStore 负责 insert / claim / mark admitted / fail / cancel；与 ADR-0098 可回访卡不同——队列是执行中的新消息缓冲，不是 parked 卡模型。

Agent 最新增量：条件产物（2026-10-29）

aida-agent · packages/agent/src/runtime/work/run-work-conditional-artifact.ts L47–152 · 7f2e519936b5
aida-agent · packages/agent/src/runtime/work/run-work-carrier-terminal.ts L10–28 · 7f2e519936b5

三仓 TLA+ 形式化验证全景（视图 `tla-verification-matrix`，2026-11-03）

三仓围绕「状态唯一权威与单次外部副作用」沉淀了跨服务端、桌面宿主与业务插件的 TLA+ 形式化规范矩阵：

仓库与平面	TLA+ 模型路径	核心安全不变式（Safety Invariant）
aida-agent（会话与控制面）	`TurnQueueFifo.tla`（本仓 `.agents/skills/formal-verification/`）<br>`specs/tla/work-control/WorkControl.tla` & `WorkRecoveryEligibility.tla`	单会话至多一个活跃执行；排队 turn 严格按 `queue_seq` FIFO 认领；Stop 抢占与迟到回执解耦（落账不唤醒）；仅在已证实无未知外部副作用的精确断点允许冷重建。
aida-agent（写权限与插件读续办）	`specs/tla/confirmed-write/ConfirmedWrite.tla` & `ConfirmedBatch.tla`<br>`.agents/skills/aida-plugin-read-continuation-verify/model/PluginRead.tla`	服务端连接器写入必须先核验凭据可用再执行 `markExecuting` CAS；插件续办待执行步骤（`pendingPluginToolCall`）仅在身份匹配且精确成功读取后才消费 `continuation` / `nextAction` 义务，写操作或缺参不释放义务。
aida-desktop（宿主单次副作用与槽位）	`.agents/skills/aida-desktop-plugin-call-once-verify/model/PluginCallOnce.tla`<br>`.agents/skills/aida-desktop-file-change-verify/model/FileChange.tla`<br>`.agents/skills/aida-desktop-chat-state-verify/model/ChatSlot.tla` & `ReplyMaterials.tla`	`PluginCallJournal` 在 `admitted → dispatched → settled` 下若 `!dispatched` 落盘失败显式抛 `PLUGIN_CALL_JOURNAL_UNAVAILABLE`，已派发非只读调用崩溃重启绝不二次重放；`FileChange.tla` 保证本机文件修改单次执行；`ChatSlot` / `ReplyMaterials` 保证桌面槽位与补证材料绑定无死锁。
aida-plugins（业务插件准入零写入）	`.agents/skills/aida-attendance-admission-verify/model/AdmissionOutcome.tla`	考勤核算在准入前（无规则基线、未采用草稿、缺少连接）确定性拒绝时 `writes = 0`，显式返回 `executionState = "completed"`，与 Desktop `PluginCallOnce` 衔接避免未发生副作用的业务拒绝被误判为 `unknown`。

aida-agent · .agents/skills/aida-plugin-read-continuation-verify/model/PluginRead.tla L1–31 · MODULE PluginRead · 7f2e519936b5
aida-agent · specs/tla/work-control/WorkControl.tla L1–40 · MODULE WorkControl · 7f2e519936b5
aida-desktop · .agents/skills/aida-desktop-plugin-call-once-verify/model/PluginCallOnce.tla L1–55 · MODULE PluginCallOnce · 4346d79eb364
aida-desktop · .agents/skills/aida-desktop-file-change-verify/model/FileChange.tla L1–50 · MODULE FileChange · 4346d79eb364
aida-plugins · .agents/skills/aida-attendance-admission-verify/model/AdmissionOutcome.tla L1–35 · MODULE AdmissionOutcome · a33ce3733365

Work 控制面四层平面与形式化安全不变式 (C0 / W0 / O1 / E0)

机制说明（全文）

状态权威矩阵

SoT 与读模型分开读

失败 / 崩溃读路径

只等过期卡的任务树（钉点 e2adc9a3c325）

归属边与非目标

视图

Work 控制面四层平面与安全不变式（C0 / W0 / O1 / E0）

三大并发竞态与崩溃恢复深挖（stop-vs-late-receipt）

成功对偶（与失败链入口相同）

失败链（深挖）

证据与范围

会话 turn 队列（钉点 e2adc9a3c325）

Agent 最新增量：条件产物（2026-10-29）

三仓 TLA+ 形式化验证全景（视图 tla-verification-matrix，2026-11-03）

三大并发竞态与崩溃恢复深挖（`stop-vs-late-receipt`）

三仓 TLA+ 形式化验证全景（视图 `tla-verification-matrix`，2026-11-03）