使用 Claude 对大规模软件进行正式验证

Anthropic的Frontier红队使用Claude对软件进行了正式验证，证明在规模超过历史极限的代码库中，代码不存在某些漏洞。

具体怎么做

团队将现有的 OSS-Fuzz 模糊测试转化为规范：编译后的 RISC-V 二进制文件在 64 MB 以下的任何输入下都不会崩溃。利用 Theorem 的 RISC-V 和 Linux 语义，Claude 编写了被证明器验证的 Rocq 证明。当证明出现错误时，Claude 会修复代码，重新生成规范，然后继续后续流程。补丁会被评估，并经过审查以确认是否存在作弊行为。

做到了什么

几周时间里，Claude在123个库中的239个入口点上实现了无崩溃运行，涉及约1.8亿行Rocq代码，同时还发现了数百个漏洞。这些验证仅涵盖单线程静态RISC-V二进制文件。

上手要点

证明内容每篇可能需要数亿个标记。在涉及36项任务的测试中，能够复制彼此证明内容的智能体使用的标记量减少了17%。