Anthropic 与 Theorem 合作、于10月22日发布的研究指向一种新工作流：AI 发现的缺陷在交付时附带已修复的数学证明，而不只是又通过一轮测试。
239个模糊测试入口——每一个如今都有机器验证的形式化证明背书。这是 Anthropic 于2026年10月22日发布的研究的核心结论：在这项工作中，Claude 为取自123个开源库的代码给出了安全属性证明。
这项工作与 Theorem 合作完成，其范围不同寻常：证明作用在 RISC-V 汇编代码层面，也就是内存安全缺陷真正存在的那一层。据 Anthropic 称，Claude 没有止步于发现缺陷，而是修补了自己找出的 bug，随后给出证明：对每一个小于 64 MB 的输入和每一种建模的 Linux 条件，修复后的程序都将始终正常退出——绝不触发内存安全错误或断言失败。
测试与证明之间的区别正是意义所在。模糊测试用大量输入去锻炼程序，并报告它恰好发现的问题；它永远无法说明程序在从未试过的输入上会有什么行为。相比之下，机器验证的证明是针对形式化规范进行机械验证的，覆盖规范所描述的整个输入空间——在这里即所有低于 64 MB 上限的输入以及建模的 Linux 环境。如果这一结论如所述成立，那么239个入口中的每一个都携带着任何规模的随机测试都无法提供的更强保证。
在汇编层面工作进一步抬高了门槛。基于源代码的推理可能遗漏编译过程中引入的缺陷；在 RISC-V 汇编上证明属性，意味着保证直接附加在处理器真正执行的指令上。
对涉事123个库的维护者而言，公布的结果描述了一个闭环——发现、修补与经验证的证明都在同一工作流内完成。这个闭环能否以普通软件维护的节奏和成本运转，是 Anthropic 的数据留下的开放问题，也将决定机器验证的安全证明究竟能成为常态，还是依旧罕见。
萬安算交所 AIXX · 萬安算交所 AIXX · 算力硬件实名会员制交易平台 · 进入货源大厅