TLA+ 突然火了，但写模型只是第一步

The internet discovers TLA+. Now what?

Boris Cherny 一条爆款推文让 TLA+ 这个三十多年的老工具重新进入大家视野。简单说，TLA+ 是一种描述系统能做什么、以及什么绝对不能发生的语言，比如“绝不能同时有两个 leader”。它自带的模型检查器 TLC 只能穷举有限实例，而且检查的是模型，不是真实代码，所以模型和实现之间天然有距离。Reasonable 团队把这件事往前推了一步...

推荐理由：Boris Cherny 一条推文让 TLA+ 这个老工具重新被讨论，文章顺势把时序规约、证明系统和 AI agent 的验证需求连成一条线，既有传播热度也有技术纵深。我会先打个折：TLA+ 本身门槛高，检查的是模型不是代码，离多数 AI 从业者的日常还有距离，但文章给出的工具链尝试和思考方向是实的，值得放进精选。