TechVerser (@realfxw) · 2026-09-23
Source metadata
- Author: TechVerser (@realfxw)
- Platform: X post (Chinese), quoting Boris Cherny (@bcherny)
- Date posted: 2026-09-23 (Wed, 23 Sep 2026 08:48:34 GMT)
- URL: https://x.com/realfxw/status/2102681516580991266
- Status ID:
2102681516580991266 - Engagement at fetch: Likes=90, Reposts=13, Quotes=0, Replies=3, Bookmarks=145, Views=18254
- Format: X post. Card teaser was not used as the source of truth. Full text from
x_thread_fetch(original Chinese) plus quoted @bcherny post. No blog / Substack / Medium essay linked. Quoted post includes a video; video binary not stored. - Quoted post: https://x.com/bcherny/status/2102543349102338309 (Tue, 22 Sep 2026 23:39:32 GMT; Likes=4856, Reposts=259, Quotes=224, Replies=405, Bookmarks=3913, Views=1344906)
- Quoted media (not stored): video https://video.twimg.com/amplify_video/2102541708466769920/vid/avc1/950x720/xAaHSTynCKfK_hRk.mp4
Post text (original Chinese)
AI 编程正在悄然迈入一个极其硬核的新阶段：形式化验证（Formal Verification）与大模型的深度结合。
今天 Boris Cherny 分享了一个令人惊艳的工程实践：他使用 Opus 5.5 对 Claude Agent SDK 进行了形式化验证，仅用几条简短的 Prompt，便直接产出了 16 个 PR，排查并修复了大量复杂的隐蔽 Bug 与竞态条件（Race Conditions）。
这项实践给开发者带来了几个非常重要的启示：
形式化方法的壁垒被彻底抹平形式化验证过去是典型的高门槛领域，Lean 和 TLA+ 等工具的学习曲线极为陡峭，通常仅见于航空航天、硬件芯片设计或核心分布式系统。Boris 直言自己并不精通这两种语言，但 Claude 却表现出惊人的建模能力——它直接构建了 6 个无 sorry 占位的 Lean 4 状态机模型（涵盖 stream、retry、engine、session phase 等），并成功在真实代码和追踪轨迹中复现了反例。
工具链分工明确在多状态与高并发场景下，组合拳效果显著：TLA+ 极度擅长排查并发时序、死锁与竞态条件，而 Lean 则擅长针对数据流与系统状态演进提供严谨的数学证明。两者结合，能精准发现人脑走查几乎不可能注意到的边界 corner cases。
破解 AI 代码信任危机的关键路径大家一直担心 AI 生成代码存在幻觉与边缘漏洞。但如果让 AI 将“自然语言规格”提升为“形式化数学规范”，用形式化验证充当严密的安全护栏，软件工程的质检方式将发生根本性变革。
当形式化验证的编写成本逼近于零，这项技术会成为未来编码与 Bug 排查的通用标配吗？
Quoted post (Boris Cherny, @bcherny)
I used Opus 5.5 to formally verify the Claude Agent SDK using Lean. A couple short prompts = 16 PRs fixing various bugs and race conditions. Video attached.
TLA+ also works well. I sometimes combine Lean and TLA+ to look for issues around data flow, concurrency, and state mgmt.
I don't know either language well, but Claude is excellent at both. This approach is super useful for formally modeling your code and finding bugs that a human probably wouldn't have spotted.
Is formal verification the future of coding (or at least, bug finding)?