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 在这方面的进展。