上周，Boris Cherny，Claude Code 的发明者，提到 Opus 能够使用 TLA+ 来发现代码中的竞态条件。现在每个人都在谈论形式化验证。作为一名长期的教育者和 TLA+ 的倡导者，这令人兴奋。但这种新的狂热让我担忧。形式化方法不会一劳永逸地解决智能体软件开发的问题。

正确的设计不会自动转化为正确的代码。要验证一个属性，我们需要一个属性来验证。TLA+ 将系统划分为行为，每个行为是一个状态序列。在每个状态中，我们可以用三个时态运算符表达布尔表达式：`[]P`（总是 P），`P'`（下一个状态中的 P），和 `<>P`（最终 P）。

`[]P` 意味着 P 在每个行为的每个状态中为真，称为不变量。`[](x' >= x)` 是一个动作属性。这些是安全性属性：坏事永远不会发生。活性属性使用 `<>`：`[]<>P` 意味着在每个状态的至少一个未来状态中 P 为真；`<>[]P` 意味着 P 变为真并永远保持为真；`[](P => <>Q)` 意味着 P 最终导致 Q。