Anthropic与Theorem公布AI形式化验证研究，覆盖123个开源库
Anthropic在10月22日介绍与Theorem合作的研究：使用Claude验证123个开源库的特定安全性质，并公开部分证明。结论依赖明确的运行假设，不等于软件不存在任何漏洞。
Anthropic于2026年10月22日公布与Theorem合作的形式化验证研究。团队称，Claude为123个开源软件库生成了特定安全性质的证明，相关工作面向RISC-V汇编层级，并公开了部分证明及运行语义。
形式化验证用数学规则描述程序应满足的条件，再由证明检查器核验。它与反复运行测试不同，但保障范围仍由规则和模型决定。
该研究的主要结论受单线程、静态二进制、固定内存预算等假设约束，涉及的输入大小也有限制。因此，这不是对全部软件、全部运行环境或全部漏洞类型的无条件安全保证。研究展示的是AI辅助安全验证的一条路径。
配图：AI生成示意图。 来源：Anthropic研究团队 https://www.anthropic.com/research/formal-verification