让 Agent 的重试不再重复扣款：Untyped 用 TLA+ 检查真实运行记录完全指南
AI Agent 接入支付、退款、删除数据等工具后，最危险的故障往往不是模型答错，而是重试把同一个副作用执行了两次。网络超时、确认包丢失、运行时自动重试，都可能让 Harness 误以为上一次调用没有发生。untyped 是一个刚发布的 MIT 开源工具，它把 Agent Harness 与副作用工具之间的协议写成 TLA+ 模型，再用 TLC 模型检查器验证设计和已记录的运行轨迹。
它检查的不是模型，而是模型之外的边界
Untyped 的 README 给出的核心前提很现实：运行时可能丢失确认、重复投递同一次尝试、在工具运行前丢弃调用，也可能按 MaxRetries 重试。LLM 本身不在模型里；被检查的是 Harness 是否能在这些条件下满足三项保证：
- AtMostOnce：每个步骤的副作用最多发生一次；
- ApprovalBeforeEffect：破坏性操作必须先有记录在案的审批；
- BudgetHeld：工具调用总数不能超过预算。
这使它适合放在 Agent 的执行层做设计审计，而不是把它误解成一个“能证明模型永远正确”的测试框架。
安装：Java 11 加 Make 即可开始
项目当前 README 的快速开始方式非常短：
git clone https://github.com/untyped-ai/untyped && cd untyped && make all
官方说明要求 Java 11+，其余依赖由项目提供。make all 会运行模型和示例检查。输出中的 correct 配置应显示 no violation；故意存在问题的配置则会报告违反了哪条不变量。例如 bug_key_per_attempt 会触发 AtMostOnce violated，帮助你定位幂等键设计错误。
最容易踩坑：幂等键不能跟着重试次数变
README 用一个很典型的轨迹解释重复副作用：第一次调用成功执行，但确认包丢失；Harness 随后重试。如果幂等键按“尝试次数”生成，那么第二次调用拿到新键，工具端无法识别这是同一个逻辑步骤，于是退款可能再次发出。
make trace cfg=bug_key_per_attempt
修复方向不是简单地“少重试”，而是明确幂等键属于逻辑步骤还是单次尝试。Untyped 将这个设计暴露为 KeyMode 配置，可取 step、attempt 或 none。这样，团队可以把关键决策写进可审查的配置，而不是藏在几层重试代码里。
四个维度，覆盖一次真实运行的关键决策
一个具体 Harness 在 Untyped 中是配置，不需要为每个框架重新发明模型。README 列出的关键常量包括：
| 配置 | 作用 |
|---|---|
KeyMode | 幂等键按逻辑步骤、尝试次数还是不使用 |
OnApprovalTimeout | 审批超时后终止，还是继续执行 |
BudgetScope | 预算按整个运行，还是按每次尝试计算 |
Destructive | 哪些步骤必须先人工审批 |
再配合 MaxRetries 与 Budget，你可以明确写出“退款必须审批、总调用不超过 3 次、审批没人处理就终止”这类策略，并让模型检查器探索可能的交错顺序。
不只检查设计，也能检查 JSONL 运行记录
Untyped 支持把真实系统的运行记录保存为 JSONL。第一行描述配置，后续每行记录事件，例如审批、调用、超时和确认。官方示例使用如下命令验证一条轨迹：
make run TRACE=path/to/your.jsonl make validate
检查结果有三类：退出码 0 表示轨迹符合协议且没有违反不变量；退出码 12 表示轨迹属于协议，但触发了某条不变量；退出码 10 表示轨迹本身不符合协议，例如破坏性调用前没有审批。这个区分很重要：它能告诉你是“实现违反了安全保证”，还是“日志已经缺少协议要求的事件”。
适合放进什么工程流程？
如果你的 Agent 使用 Temporal、Inngest、Restate、DBOS、LangGraph，或者是自研的持久化运行时，可以先把工具调用边界抽象成事件，再用 Untyped 检查重试、审批和预算策略。对于支付、退款、发邮件、删除资源等不可逆操作，建议至少覆盖三组测试：确认丢失后的重试、审批超时、预算在重试后是否仍然有效。
但要记住它的边界：模型检查的是你提供的协议和有限范围，不是全部业务代码；它不是 LLM 模型的评测器，也不负责运行时拦截调用，更不是恢复丢失事件的工具。一个“从来不调用工具”的 Harness 可能看似满足安全性质，所以项目还提供 vacuity 检查，确认副作用确实可达。
对开发者来说，Untyped 最有价值的地方是把“Agent 应该安全重试”从口号变成了可执行的协议。先用模型检查设计，再用 JSONL 检查实际运行记录，最后把反例轨迹加入回归测试，这条路径比上线后再追查重复退款更便宜。
相关链接