What TLA+ can and can't check

ID: 3f95e6f8
原文链接: https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/
作者: Hillel Wayne
日期: 2026-09-30
分类: coding
来源类型: article
标签: formal-methods、tla-plus、verification、ai-coding、agentic-software-development
质量评分: 4/5
抓取时间: 2026-10-03 (daily-intake-evening, Obsidian AK-RSS source note)

中文导读

Claude Code 发明者 Boris Cherny 提到 Opus 能用 TLA+ 找出代码中的竞态条件后，网上刮起「形式化方法终结 agentic 开发难题」的亢奋。作为 TLA+ 长期教育者，Hillel Wayne 泼冷水：要验证一个性质，前提是你得先把性质表达成逻辑公式——而很多重要性质根本不可表达。TLA+ 能查的是不变量（[]P）、动作性质（P'）与活性（<>P 组合，如 []<>P「最终稳定」、P ~> Q「P 导致 Q」）。查不了的：两步以上性质（「按删除再 undo 应回原状」「开机十步内完成」）、浮点与真实时间、可达性（「这局游戏存在赢法」——量词是「对所有行为」而非「存在行为」）、超性质（如「节能模式耗能恒不高于普通模式」需成对比较两个行为——覆盖大量安全性质与统计性质如 P95 延迟）、以及状态空间整体性质。辅助变量、自组合、TLC 的 REACHABLE 等都是可行 hack，但各有代价：毁掉 refinement、状态空间指数爆炸、模型失真。结论：TLA+ 摘的是不变量与活性这些低垂果实，用它检查 vibe code 有潜力也有坑，但「一劳永逸」是不存在的。

为什么值得关注

给「用形式化方法兜底 AI 写代码」的热潮划边界：验证的上限不在工具，而在性质能否被写成公式。

English Summary

After Boris Cherny (inventor of Claude Code) mentioned Opus used TLA+ to find race conditions, online euphoria claims formal methods will solve agentic software development. Hillel Wayne's correction: to verify a property you must first express it as a logical formula, and many important properties are inexpressible. TLA+ handles invariants ([]P), action properties (P'), and liveness (<>P compositions like []<>P and P ~> Q). It cannot natively express: multi-step properties ('delete then undo restores state', 'power on within ten steps'), floating-point or real-time properties, reachability ('this game is winnable' - quantification is over all behaviors, not 'there exists a behavior'), hyperproperties (cross-behavior comparisons like 'energy-saving mode never uses more power than normal mode', which cover many security and statistical properties such as P95 latency), or state-space-global properties. Auxiliary variables, self-composition, TLC's REACHABLE keyword are workable hacks with serious costs: ruined refinements, exponential state spaces, specs that no longer resemble the system. TLA+ picks the low-hanging fruit; it does not end the problem.

Obsidian 原文摘录（AK-RSS source note 头部）

FEED: Computer Things
TITLE: What TLA+ can and can't check
LINK: https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/
DATE: 2026-09-30T21:27:03+08:00
---

Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+ to find race conditions in code. And now everybody on the internet is talking about formal verification. As a long-time educator and advocate of TLA+, this is really exciting! As a long-time advocate of level-headedness, this new euphoria worries me.

Notes

Content grounded in the same-day Obsidian AK-RSS digest source note (full article text cached in the vault note) during daily-intake-evening.
中文导读 block is the entry's summary_zh (verbatim); 为什么值得关注 is the entry's one_liner; no claims beyond the fetched source text were added.
Source note: OpenClaw定时任务/AK-RSS-Digest（89源精选）/source/2026-10-03-hillel-wayne-tla-plus-can-and-cant.md