Show HN· damianabramov·· 29 天前精选AI 评分62
Untyped 发布：用 TLA+ 规范校验 Agent 运行记录
Show HN: Untyped – check recorded agent runs against a TLA+ spec
AI 导读
Untyped 开源了一个 TLA+ 协议模型 harness.tla，用于检查 Agent harness 与带副作用工具之间的协议，覆盖 AtMostOnce、ApprovalBeforeEffect、BudgetHeld 三条不变量。
推荐理由
原文给出了可复用的 TLA+ 协议模型与运行日志校验流程，读者可据此检查自家 Agent 的重试与审批设计。
来源：Show HN · github.com