Claude大模型实现RISC-V机器码级形式化验证，首次穿透至x86硬件缺陷层

SmartHey10月23日消息，近日，Anthropic前沿红队联合Theorem Labs发布突破性研究报告：首次利用Claude大模型对真实运行的RISC-V汇编指令开展大规模形式化验证。在数周内完成123个开源代码库、239个测试入口的全覆盖验证，生成1.8亿行可通过Rocq证明检查器严格核验的数学证明代码，不仅高效发现传统测试难以触达的深层软件漏洞，更首次定位到x86处理器硬件层面的设计缺陷。

长期以来，模糊测试（如谷歌OSS-Fuzz）是安全领域的主流手段——通过万亿级随机输入触发程序崩溃以暴露问题。但其本质属概率性方法：受限于输入规模与路径覆盖盲区，大量高危漏洞长期潜伏。例如，某类漏洞仅在特定20MB二进制格式输入下才会触发，即便执行万亿次测试也极难命中。

本研究另辟路径，将每个程序入口转化为可证伪的数学命题：在明确约束条件（如任意≤64MiB输入）下，严格证明程序不会发生崩溃、内存越界、空指针解引用等任何未定义行为。该方法覆盖全部执行路径，无遗漏风险；一旦证明中断，即精准指向潜在Bug所在；Claude更可自主生成修复补丁，并立即重启验证流程，形成“发现—修复—再验证”闭环。

实验表明：研究人员在目标代码中预设7处漏洞，传统随机测试仅检出2个，而形式化验证实现100%检出。在一款主流PDF阅读器上，Claude单周发现的漏洞数量，相当于该软件过去一整年所有公开安全报告的总和。

尤为关键的是，本次验证直接作用于编译后的RISC-V机器码，而非高级语言源码。以轻量级CJSON解析库为例：其C语言入口仅391行，但配套的数学证明代码高达63万行——需完整建模进程启动、内存分配器、系统调用接口及底层运行时环境，其中与业务逻辑直接相关的证明仅占约10%，其余均为对硬件与操作系统抽象层的严密刻画。

项目总计尝试生成近10亿行证明，最终1.8亿行通过Rocq校验。单份证明的CPU核验耗时从数十分钟至数小时不等，体现其数学严谨性与工程挑战并存。

形式化验证曾因极高门槛而局限于极少数场景（如seL4微内核：2人年编码 vs 20人年验证）。而大模型正彻底改变这一格局——数周即可完成上百个开源库的验证，并进一步自主构建x86指令集的完整数学模型，复现Ubuntu用户态启动全流程，同时发现x86官方文档数百处矛盾与错误，甚至捕获CPU硬件本身存在的逻辑缺陷，真正实现从应用代码、系统软件到芯片指令集的全栈数学可信验证。

报告显示，该技术迭代迅猛：验证吞吐量约每两个月翻倍；证明片段支持跨项目复用，显著降低token消耗。以Nix软件生态为基准测算：完成OpenSSL一次端到端机器码验证成本约为22万美元；若分摊至其下游依赖的逾万个软件包，单个包验证成本仅约14美元。

按当前发展节奏推演，每年投入1亿美元，至2027年底累计约1.34亿美元，有望完成Nix生态95%机器码的形式化验证。对比全球每年数千亿美元的网络安全损失，这项技术具备显著的现实经济价值与战略安全意义。

近期重大网络攻击频发，漏洞爆发速度远超人工响应能力。目前，该项目首批25个开源库、60个验证入口的完整证明文件已开源至GitHub，支持全球开发者复现、审计与协作演进。

研究团队指出：大模型驱动的形式化验证，正从理论走向基础设施级实践，有望为互联网核心系统提供首个可验证、不可绕过的数学安全兜底层。