博里斯发推，互联网复制粘贴 本周，博里斯·切尔尼在TLA+这一超过30年的正式建模工具上发表了一条推文。他使用Opus 5.5在TLA+和Lean中建模了Claude Agent SDK的某些部分，互联网也如往常一样进行反应：约100万次观看，数千个书签，还有人问TLA+到底是什么。博里斯的帖子是一个很好的展示，增加了早期示例，表明在智能编码中使用TLA+是值得投资的：参见Datadog关于基于管道的代理的帖子。如果你是现在好奇TLA+是什么及其用途的人，你来对地方了。TLA+恰好是我们团队深入研究的一种正式技术。但我们关心它还有一个更大的原因。TLA+为我们提供了一种紧凑的语言，用于描述系统被允许做什么，以及必须始终或最终为真的内容。这是验证的一个有用起点，但并不是故事的终点。简而言之：TLA+描述了可能的系统行为以及这些行为应该满足的属性。TLA+本身并不完全验证实现。它检查软件的模型，而不是软件本身，其主要模型检查器只探索有限实例。现代证明系统可以让我们走得更远。在Verus中，规范、证明和Rust实现可以共存于同一种语言。人工智能已经能够自动化这一过程的一部分。我们建立了一个智能化的管道，将超过16,000个TLA+规范/属性对转化为3,000多个机器检查的Verus证明。那有趣的问题是，不仅仅是一个代理能否写TLA+，还有一旦代理能够在规范、证明和实际程序之间移动，能实现什么。我们在Reasonable的工作部分是训练模型，使代理能够做到这一点，始终如一、可靠、快速。 什么是TLA+ 我们的运行示例是下面的互动游乐场，三个计算机a、b和c需要就谁是领导者达成一致。数据库依赖于领导者选举的正确性。我们要求没有两个领导者同时存在。你可以通过游乐场点击学习TLA+的基础知识，经过游戏的五个级别。TLA+（动作的时序逻辑）是一种用于记录两种对象的语言： - 转移系统：系统可以执行的操作。状态是系统的快照（谁是候选者，谁为谁投票，谁是领导者）和动作是改变状态的单一步骤（“a开始选举”，“b为a投票”）。在互动游乐场中，你可以手动采取这些步骤，像测试者一样探索一个可能的运行。 - 时序属性是关于一个运行如何随时间发展的陈述。例如，“永远不会有两个领导者。” “最终选出一个领导者。” TLA+模型声明合法的系统状态及这些状态之间的允许过渡。例如，在选举中，a、b或c中的任何一个都可以从初始状态开始选举，并在此过程中为自己投票，b可以为a或c投票。它对过渡没有施加顺序限制，也不试图对不同事件发生的概率分布进行建模，这对于分布式系统而言是正确的抽象，在这些系统中，消息、超时和用户操作可以以多种不同的顺序发生。其基础数学很简单，使用集合、真/假语句和关系。从执行的运算符构建时序属性： □ P（始终P）：P在每个访问的状态中都成立。 ◇ P（最终P）：P在未来某个状态中成立。 P ⇝ Q（P导致Q）：每当P成立时，Q最终也成立。 两种属性特别重要。安全性：永远不会发生坏事。对我们的选举：□（永远不会有两个领导者）。在游乐场中，模型检查器探索每个可能的状态：所有38个状态对于三台计算机，并确认该属性。第二级更改了一项规则，使得一台计算机可以投两次。然后检查器返回一个六步执行，结束时有两个领导者。该执行是一个反例：模型违反该属性的具体方式。活性：某些好事最终发生。仅有安全性还不够。一个永远不做任何事情的系统是完全安全的。因此，我们也可能需要：◇（某人是领导者）。第三级显示了这为什么重要：一个拼写错误阻止任何事情发生，安全性检查仍然通过。活性需要公平假设，排除执行中一种行为永远可能发生但从不采取的情况。弱公平WF(A)表示一个保持启用的行为最终必须发生；强公平SF(A)涵盖无限次成为启用的行为。心理模型很简单：TLA+模型描述系统的可能执行次序，而属性则描述哪些次序是可接受的。验证问的是每一个可能的次序是否都可以接受。TLC，标准的TLA+模型检查器，通过枚举有限实例的可达状态来回答这个问题。