❯ Anthropic 与 Theorem 为 123 个开源库生成安全证明，扩大 AI 形式化验证范围

把测试要求变成数学证明Anthropic 在 10 月 22 日发布的研究中介绍，与 Theorem 合作用 Claude 为 123 个开源库的 239 个入口生成安全属性证明。团队将程序及测试编译为 RISC-V 指令，模型负责写证明，再由 Rocq 证明检查器核验是否满足所定义的要求。

覆盖范围由条件决定普通模糊测试通过不断输入数据寻找崩溃，形式化验证则尝试证明规定范围内的输入都不会导致特定错误。本次证明依赖单线程静态二进制、固定内存预算、所建模的 Linux 行为等条件，输入上限为 64MB。它覆盖相应的内存安全和断言要求，并未证明整个软件在所有环境下都无漏洞。

检查器承担最终核验这套流程把模型擅长生成大量代码与证明的能力，接到独立检查器上。开发者仍需确认规格、底层语义和检查器可信，但无需逐行人工审阅全部证明。随着同类规格和模型被复用，为更多软件提供特定安全保证所需的工作，有望更集中于定义清楚“究竟证明了什么”。

▮ SIGNALAI 生成与独立检查器结合，让部分软件安全要求获得可检查的证明，也把规格定义的重要性进一步提高。