加载失败
TLA+ 是 Leslie Lamport 提出的形式化规格语言，主要用来描述并 model check 并发和分布式系统的状态与不变量，而不是直接写可执行业务代码。这个话题的背景是，Claude 这类 LLM 最近被拿来尝试自动生成 TLA+，甚至有人把它用于 Lean 4（一个 proof assistant 和函数式编程语言）中的系统建模。讨论里还对比了 SVA（SystemVerilog Assertions，硬件验证中的断言语言）和 Verus（一个把 Rust 风格实现与证明绑定的验证语言），反映出“通用形式化语言”与“领域专用验证工具”的路线之争。有人还提到 NVIDIA 曾赞助 TLA+ challenge，以及用 Raft、etcd 这类分布式系统代码反推规格的想法，说明大家在关注自动化能否真正缩短从代码到形式化验证的距离。
有人提到 Claude 最近在 TLA+ 上已经相当能用，甚至能把 Monopoly 规则建成一个看起来“像那么回事”的模型。虽然还没看到严格的 exhaustive checking 结果，但从外观和复杂度上看，LLM 已经能快速产出可读的规格草案。还有人补充 NVIDIA 之前赞助过 TLA+ challenge，说明这个领域并不是完全边缘化的冷门方向。
质疑点集中在：即使模型看起来复杂，懂 TLA+ 的人也未必能迅速判断它是否真的有效，尤其是面对像 Monopoly 这种规则并不算极简的系统。更进一步的担忧是，如果连设计和实现都交给 LLM，最后可能只得到一个“机器自洽”的产物，而不是人类真正想要的性质。有人指出，LLM 生成的 TLA+ 也许能被验证某些性质，但“验证的是不是对的东西”仍然必须由人来定义。
有评论表示自己已经不再用 TLA+ 单独建模真实系统，而是让 Claude 帮忙在 Lean 4 里写系统模型，并把证明和带数值类型的实现结合起来。另一个人正在为大型硬件项目比较 SVA、TLA+ 和 Lean，核心问题是该选更领域化的断言语言，还是更通用的 proof assistant。这里隐含的分歧是：通用工具更灵活，但 domain-specific formalisms 往往更贴近工程落地。
有评论把这场讨论理解成对 Verus 的侧面推荐：如果实现和验证是耦合的，就不太会出现规格和实际代码逐渐分叉的问题。支持这种路线的人显然更看重“代码即验证”的一体化，而不是先写 TLA+ 再手工对齐实现。这个观点把重点从“LLM 能不能写规格”转成“如何避免 spec 和 implementation 漂移”。
有人提出一个更实用的方向：先把 source code 给 LLM，甚至把 Raft、etcd 这些名字都遮掉，再让它生成 TLA+ spec。这个想法本质上是在做逆向抽象，把已有系统提炼成可检查的形式化模型。它也说明讨论不只是在问“自动写规格行不行”，还在问“能不能从代码中自动识别出系统协议和状态机”。
TLA+: Leslie Lamport 提出的形式化规格语言，用来描述并 model check 并发和分布式系统的行为。
Lean 4: 既是 proof assistant 也是函数式编程语言，常用于写形式化证明和可验证的程序。
Verus: 一种 Rust 风格的验证语言，把程序实现和证明绑定在一起，尽量避免规格与代码分离。
SVA: SystemVerilog Assertions，硬件验证里常用的断言语言，适合描述设计必须满足的时序和行为约束。