Anthropic 红队：用 Claude 对大型代码库做形式化验证
Anthropic 在 Frontier Red Team 博客发文，讲用 Claude 在大规模代码上做形式化验证。帖子说形式化验证能证明代码不含某些类型的 bug，但过去只适用于小代码库或要专家投入大量时间；后半句「有了 AI 模型……」在节选里被截断。
Anthropic@anthropicai原帖
为什么值得留
说明 AI 可能把「证明没有某类 bug」从小众手段变成常规工程选项。
可以从这里开始
打开博客原文，记下他们验证的是哪类性质、代码规模多大，再挑你项目里一个小模块的不变量试写规格。
阅读时留意
节选在关键处截断，没看到方法、规模和效果数字；形式化验证只能证明写进规格的性质，规格写错照样漏。
OnBalls 导读整理于 2026.10.25。只读收件箱保存的帖子节选，正文在「With AI models,」处截断；未打开博客原文。