Boris Cherny 详解 Claude 如何用形式化方法定位并修复代码缺陷

Claude Code 负责人 Boris Cherny 补充说明 Claude 在代码中做的事：先针对棘手状态机或易出现竞态的部分建立程序模型，再在模型中寻找反例作为疑似 bug，随后复现并修复这些 bug。他强调这并非整个代码库已被形式化验证，而是对最棘手的部分建模、检查反例并修复。