三仓 TLA+ 形式化验证全景：从会话入队、Work 控制到本机单次副作用

三仓 TLA+ 形式化验证全景：从会话入队、Work 控制到本机单次副作用 由 Archify 生成的工作流图。 01 / aida-agent 服务端控制与契约模型 EX / aida-desktop 宿主与 aida-plugins 业务模型 会话入队与 Work 控制 写权限与插件读义务 本机单次效应与业务准入 服务端 TLA+ 规格 (TurnQueueFifo · WorkControl · ConfirmedWrite · PluginRead) 桌面与插件 TLA+ 规格 (ChatSlot · FileChange · PluginCallOnce · AdmissionOutcome) 1 TurnQueueFifo · 迁移 191 · 单活跃锁 · aida-agent 服务端控制与契约模型 › 服务端 TLA+ 规格 (TurnQueueFifo · WorkControl · ConfirmedWrite · PluginRead) › 会话入队与 Work 控制 · aida-agent 1 TurnQueueFifo 迁移 191 · 单活跃锁 aida-agent 2 WorkControl · C0/W0/O1/E0 · 冷重建 · aida-agent 服务端控制与契约模型 › 服务端 TLA+ 规格 (TurnQueueFifo · WorkControl · ConfirmedWrite · PluginRead) › 会话入队与 Work 控制 · specs/tla 2 WorkControl C0/W0/O1/E0 · 冷重建 specs/tla 3 ConfirmedWrite · 先验凭据后 CAS · aida-agent 服务端控制与契约模型 › 服务端 TLA+ 规格 (TurnQueueFifo · WorkControl · ConfirmedWrite · PluginRead) › 写权限与插件读义务 · WriteAuthority 3 ConfirmedWrite 先验凭据后 CAS WriteAuthority 4 PluginRead · 精确读才消费义务 · aida-agent 服务端控制与契约模型 › 服务端 TLA+ 规格 (TurnQueueFifo · WorkControl · ConfirmedWrite · PluginRead) › 写权限与插件读义务 · nextAction 4 PluginRead 精确读才消费义务 nextAction ChatSlot / Reply · 槽位状态与补证材料 · aida-desktop 宿主与 aida-plugins 业务模型 › 桌面与插件 TLA+ 规格 (ChatSlot · FileChange · PluginCallOnce · AdmissionOutcome) › 会话入队与 Work 控制 · aida-desktop ChatSlot / Reply 槽位状态与补证材料 aida-desktop FileChange · 本机文件修改单次执行 · aida-desktop 宿主与 aida-plugins 业务模型 › 桌面与插件 TLA+ 规格 (ChatSlot · FileChange · PluginCallOnce · AdmissionOutcome) › 写权限与插件读义务 · aida-desktop FileChange 本机文件修改单次执行 aida-desktop 5 PluginCallOnce · Journal 三相禁盲重放 · aida-desktop 宿主与 aida-plugins 业务模型 › 桌面与插件 TLA+ 规格 (ChatSlot · FileChange · PluginCallOnce · AdmissionOutcome) › 本机单次效应与业务准入 · aida-desktop 5 PluginCallOnce Journal 三相禁盲重放 aida-desktop 6 Admission 核验 · 零写入标 completed · aida-desktop 宿主与 aida-plugins 业务模型 › 桌面与插件 TLA+ 规格 (ChatSlot · FileChange · PluginCallOnce · AdmissionOutcome) › 本机单次效应与业务准入 · aida-plugins 6 Admission 核验 零写入标 completed aida-plugins FIFO 认领入 Work E0 写权限门禁 工具續办契约 派发 Host 调用 executionState 裁决 fs/change 委托 客户端槽位同步 图例 用户界面 Agent 逻辑 策略 上下文 / 追踪

服务端控制与写权限不变式 (aida-agent)

  • • TurnQueueFifo & WorkControl：单会话至多一个活跃执行，Stop 与迟到回执解耦（落账不唤醒）
  • • ConfirmedWrite & PluginRead：先查连接器凭据再 CAS markExecuting；仅精确成功读取才消费 nextAction 义务

桌面宿主单次副作用不变式 (aida-desktop)

  • • PluginCallOnce.tla：admitted→dispatched→settled；!dispatched 落盘失败抛 UNAVAILABLE，严禁重启重放已派发写操作
  • • FileChange.tla & ChatSlot/ReplyMaterials.tla：保证本机文件修改单次执行与会话槽位/补证材料状态无死锁

业务插件准入零写入不变式 (aida-plugins)

  • • AdmissionOutcome.tla：考勤计算在准入前（缺规则基线/缺连接）拒绝时 writes = 0，显式返回 executionState='completed'
  • • 与 Desktop PluginCallOnce 衔接：零写入确定性拒绝不会将任务误锁入 manual_recovery (unknown)