TLA+ 追踪：先说清要验证什么，形式化方法才能给出有效结论
据 Hillel Wayne 的技术文章，TLA+ 教育者 Hillel Wayne 讨论了这种方法能直接表达哪些系统性质，以及哪些需求需要额外建模或其他工具。
作者：林岚｜OC 开发者生态编辑
据 Hillel Wayne 的技术文章，TLA+ 教育者 Hillel Wayne 讨论了这种方法能直接表达哪些系统性质，以及哪些需求需要额外建模或其他工具。
一句话结论：形式化验证能严格回答已经写成性质的问题，却不能替团队决定什么才是正确的需求。
此前 OC 已报道 TLA+ 被 AI 编程重新带火，重点是模型检查不等于代码认证。这次新增的讨论更靠前：在运行检查器之前，团队是否已经选对问题。
不变量可以表达系统不能出现的状态，活性性质可以表达某些进展最终会发生。这对并发与分布式设计很有帮助。但用户说“体验应该流畅”或“识别结果应该合理”，尚未构成可以检查的逻辑性质。
Wayne 特别提醒，比较多条行为、概率统计或真实时间指标，不能都当成普通 TLA+ 性质直接检查。这个边界也不是绝对禁止：辅助变量、组合建模与其他工具可以处理部分问题，代价是模型更复杂。
例如，模型证明队列最终会处理消息，不等于生产服务在五毫秒内处理完。现实耗时受到机器、网络和负载影响，仍需要测量。模型里的错误恢复也要对应到实际代码，否则检查的是另一套理想系统。
AI 可以帮助生成规格，但如果模型与代码共同误解了需求，两边一致仍可能一起出错。评审需要关注状态抽象、假设和所选性质，并用真实反例检查这些选择，而不只是查看一行通过提示。
关键事实
- 来源：Hillel Wayne 的技术文章。
- 核心信息：新增重点为性质表达边界；常见不变量与活性之外，有些问题需要额外建模或不同工具。
OC 判断
形式化方法的门槛包含需求精确化。AI 降低写规格的成本之后，团队更应投入到假设和性质的评审。
为什么重要
- 对开发者：把要保证的行为写清楚，并检查模型与实现之间的关系。
- 对企业：形式化检查、运行测试和性能测量需要各自承担明确职责。
- 对用户：验证通过应说明验证范围，不能当成整套产品无错误的承诺。
评论
围绕这篇文章补充信息、提出问题或分享观察。