AI 导读
给形式化方法爱好者们的更多细节——正在发生的事是 Claude 在做类似这样的事情： 1. 构建程序模型，针对代码中棘手的状态机或易发生竞态的部分 2. 在模型中寻找反例。这些是疑似 bug 3. 复现这些 bug 4. 在代码中修复这些 bug 并不是整个代码库都被形式化验证了（还早着呢！..），更多是代码中最棘手的部分被建模、检查反例并修复。
正文
More details for the formal methods people -- what's happening is Claude is doing something like:
1. Building a model of the program, targeting a tricky state machine or race-prone part of the code
2. Finding counter-examples in the model. These are suspected bugs
3. Reproducing the bugs
4. Fixing the bugs in the code
It's not that the whole codebase is formally verified (yet!..), more that the hairiest parts of the code are modeled, checked for counter-examples, and fixed.
来源：@bcherny · x.com