TLA+ 因 Claude 团队一条推爆红：形式化验证遇上 Agent 编码
fhuszar · x · 2026-09-26
Reasonable 团队的长文背景：Claude Code 作者 Boris Cherny 的一条病毒式推文（约百万浏览）让 30 多岁的形式化建模工具 TLA+ 重新进入大众视野——他用 Opus 5.5 把 Claude Agent SDK 的部分逻辑建模成 TLA+ 和 Lean，Datadog 也发布过「harness-first agents」的类似实践。
文章给出 TLA+ 的实用入门：它用紧凑的语言描述系统允许的行为及必须/最终满足的属性，但 TLA+ 本身验证的是软件的模型而非实现，其主模型检查器只能探索有限实例。作者认为 TLA+ 只是起点，更大的图景是把时序规约、现代证明系统与 AI agent 结合：从建模系统行为，到生成可机器检查的证明，最终走向「规约—实现—验证」一体的软件开发闭环，并预告了 Reasonable 在这方面的进展。
所属事件:Claude 团队一条推文带火形式化验证工具 TLA+(2 条相关)→
「编程与Agent」频道最新
- 用 /doctor prompt-audit 清理 Claude Code 过时指令与冲突配置 — daniel_mac8 · 2026-09-26
- 老 M1/M2 当测试跑分机，脚本让闲置 Mac 变远程 CI 服务器 — jasonkneen · 2026-09-26
- DHH 宣布 37signals「放下笔」:月产 15 万行代码全靠 agent — Recent-Tangerine2745 · 2026-09-26
- Agent 时代核心手艺：Harness 工程全景解析 — techNmak · 2026-09-26
- 用 Gemini 把 PTX 手册转 Markdown，图片全变 ASCII 艺术 — bingxu_ · 2026-09-26
- Merge 实测：自研 MCP 连接器任务正确率持平或胜公共 MCP — shensi · 2026-09-26