几条短提示，十六个修复的 PR

用 Opus 5.5 加 Lean 给 Claude Agent SDK 做形式化验证，几条短提示换回十六个修缺陷的 PR，这是 bcherny 摆出的做法。 路子摆开。Lean 那边跑得通，TLA+ 也行，两边有时合着用，一个盯数据流，一个盯并发和状态管理。他自己说两种语言都不熟，可 Claude 在这门上都拿得下，这办法对把代码建成模型、抓出人眼未必找得到的那类毛病，格外管用。 顺带抛出的问题是，形式化验证会不会成为编程的未来，哪怕只是找缺陷那半。 "我不懂这两门语言，可 Claude 都行"这半句是全场重心。前面两成提示词八成系统设计那篇讲的是系统要哪几件，这条把其中"验证"那件换成了一种更硬的手段。跟前面把你自己从瓶颈上移开呼应，那边讲的是把决定和检查挪进系统，这条讲的是检查那层直接换成数学那套。两篇凑起来，才是完整的手。跟前面会话是上游资产也接得上，提示词短而狠，正是会话攒到一定成色才写得出的。 十六个 PR 这个数我留意。短提示能换来这个量，说明难的从来不是敲那几行，是知道该去查哪里，形式化那层恰好把"该查哪里"写成了规则。 我留的疑问有三处。十六个 PR 里真正由验证逮住的占几成没拆；Lean 建模那步花了多少轮没说；这两门语言之外还能不能外推也没交代。 这周挑一个自己仓库里最怕出事的模块，让模型先把它的不变量写下来，再跑一遍，看能不能撞出人没发现过的那条。