用途 该技能面向需要从产品规格从零构建 @statelyai/agent 状态机的场景。核心主张是：写在提示词里的规则不构成不变量，必须先把规则转化为状态机结构，再进行证明。整体流程为：不变量 → 状态机 → 场景测试 → 证明 → 崩溃/恢复 → 检查器 → 交付。当整个规格可以放入 JSON AgentWorkflowConfig（真值守卫、无计数器、无 spawn）时，应改用 generate-machine。
主要能力
- 列出不变量：把每条规格规则写成一句可被搜索证伪的话，例如某操作没有确认键就绝不运行、模型轮次最多 8 次；向用户询问规格中读不到的阈值和上限。
- 结构化为状态机：按规则形态映射结构——需要先审批则用等待状态；上限（轮次、重试、拒绝次数）用上下文中计数器并在越界转移中内联检查；阈值用转移函数中的内联守卫；任意时刻事件（取消、接管、中断）用根级 on 处理器指向最终状态或每个状态的作用域 on；等待并行工作用子任务加 join 计数；超时/SLA 用 after 转移；令牌预算用根级 @agent.usage 折叠加守卫。守卫内联编写、目标写在转移函数里，以便 describeMachine 读取；向 setupAgent 传入事件类型（含 events: {}）使内置事件获得类型。
- 场景测试：每条规则至少一个测试，覆盖正常路径与各失败模式；用脚本化执行器或 ai/test 的 MockLanguageModelV3 伪造模型；测试搜索看不到的运行时行为，如中止信号到达执行器、取消后迟到的模型回答。
- 证明：使用 @statelyai/agent/testing 的 canReach 与 explorePaths。为每个源列出至少两种输出加上错误，否则不会分叉；任意时刻规则需 interleave: "pending"；跨子任务规则需 children: "coupled"；结果需 complete: true，否则读取 unexplored 与 unexpandedEvents；对事件补 payload，对搜索爆炸用 dedupeBy。长生命周期机器无法完成，应报告有界证明（仅 max-depth 说明，并标明深度）。做变异检查：削弱每个守卫、确认证明能找到反例；记录无法证明的规则及原因。
- 崩溃与恢复：对每个场景调用 checkCrashRecovery，断言 report.failures 为空；它在每次日志追加后及每个效果执行中终止运行并从日志恢复，与不中断运行对比。执行器与假工具必须依据请求而非调用顺序作答；失败的模型调用不会重跑，进行中的会以相同 callKey 重跑；普通 actor 无 callKey，需从领域派生幂等键并在效果中去重；断言副作用账本而非仅最终状态。
- 检查：用 @statelyai/sdk 的 inspector.inspect 运行一个场景，每个 actor 注册一次、根状态按序到达；SDK 的 node-relay 需要安装 ws。
- 交付：给出不变量清单（各标注已证明/有界/仅测试及方法）、重跑测试与证明的命令、无法证明的内容及原因，然后转到 add-traces。
适用场景 需要从零构建规则必须可验证的智能体状态机；规格包含审批、上限、阈值、任意时刻事件、并行汇合、超时或令牌预算等约束；需要场景测试、可达性证明与崩溃恢复验证。
限制 依赖 @statelyai/agent、@statelyai/agent/testing、@statelyai/sdk 等包；长生命周期机器无法得到完整证明，只能给出有界结论；部分规则只能由测试覆盖；node-relay 需要 ws。其余细节暂未提供。