大模型
x.com ·
@bcherny
Claude 对代码中高风险部分做建模、反例检测与修复
有开发者披露 Claude 的工作方式：先针对棘手的状态机或易出现竞态的代码段建立程序模型，再在模型中寻找反例（疑似 bug），随后复现并修复这些 bug。该描述强调并非整个代码库已完成形式化验证，而是对最复杂部分做建模、反例检查与修复。
AI推荐理由 来自 Claude Code 相关开发者账号，具体描述了 Claude 在形式化方法上的工作流程：对易出错的状态机或竞态代码建模、寻找反例、复现并修复 bug，并明确说明并非整个代码库已被形式化验证。信息密度较高，属于可验证的技术流程描述，但仅为单条推文，缺少可复现的案例或数据，且未提供发布时间以外的独立证据。
72
正文
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.