Anthropic 用 Claude 对开源库做数学级安全验证，几周完成 123 个库
精选理由
Anthropic 用 Claude 把测试变成数学证明，几周验证了 123 个开源库，还顺手修了上百个老 Bug，做安全的人可以看看思路。
Anthropic 联合 Theorem 公司，用 Claude 直接读取编译后的汇编代码，把常规测试用例转换成数学证明规范，自动编写证明代码并交由逻辑检查器核查。这套方案在几周内完成 123 个开源库的深度验证，证明 239 个测试入口在面对 64MB 以内任意输入时不会发生内存崩溃。验证过程中还揪出上百个陈年隐蔽 Bug，包括数万亿次传统自动化测试都没发现的内存溢出和逻辑漏洞。
原文 · Gorden Sun
Anthropic 利用 AI 实现了超大规模的软件安全数学级验证。
现在的软件哪怕经过成万亿次常规测试，内部依然潜藏着大量隐蔽漏洞，容易被黑客或恶意攻击者挖掘利用。
Anthropic 联合 Theorem 公司，利用旗下的大模型 Claude，直接读取编译后的底层汇编代码，把常规测试用例转换成数学证明规范，自动编写出证明代码并让逻辑检查器进行严密核查。
这套方案在几周内完成了 123 个开源库的深度验证，不仅证明了 239 个测试入口在面对 64MB 以内的任何数据输入时都绝对不会发生内存崩溃，还自主修复了在证明过程中顺带揪出的上百个陈年隐蔽 Bug，包括那些在数万亿次传统自动化测试中都没能发现的内存溢出和逻辑漏洞。
这可能是软件安全的解决办法。
