Show HN: Untyped – check recorded agent runs against a TLA+ spec

AI 摘要

开发者发布开源工具 Untyped，用 TLA+ 规范对 AI 智能体运行进行模型检查与轨迹验证。该工具将智能体框架与副作用工具之间的协议建模为 harness.tla，检查 AtMostOnce、ApprovalBeforeEffect、BudgetHeld 等安全不变量，并支持将真实系统录制的 JSONL 运行日志与同一规范比对，给出接受、违反或拒绝三种判定。项目以 MIT 协议开源，基于 Java 11+ 运行。