形式验证不再只属于专家：Claude在123个开源库的RISC-V汇编上写出安全证明
核心概要
形式验证过去需要多年专家投入，通常只用于航空电子等关键代码。与Theorem合作的工作让Claude把开源库已有的模糊测试改写成规格，再在编译后的RISC-V汇编上自动生成证明，覆盖123个OSS-Fuzz库中的239个入口点，并在此过程中修补了它发现的缺陷。这些证明假定程序是Linux上单线程、静态链接、内存预算固定的RISC-V二进制，输入上限为64 MB。
深度剖析
形式化安全证明现在可以由大模型在真实开源软件的机器码层面批量产出，而不再依赖少数专家逐个项目手工书写。 此前形式验证需要多年专家投入，例如seL4内核实现用了两人年，而形式验证用了20人年，因此只在空客航电这类任务关键场景中可行。 在与Theorem的合作中，Claude在数周内为123个OSS-Fuzz库中的239个入口点完成修补并证明任意不超过64 MB的输入都不会触发崩溃，证明总量约1.8亿行Rocq。
做法是把开发者已有的模糊测试当作规格：把“该测试永不崩溃”这条规则翻译成针对编译后RISC-V指令的命题，再让模型去证明它。 模糊测试靠大量半随机输入暴力搜索，无论跑多少次都不保证覆盖所有代码路径；而证明一旦成立，该入口点上的模糊测试就不再必要。 证明借助Theorem提供的RISC-V指令与Linux进程语义把汇编翻译成数学模型，典型证明约60万行，对应二进制的中位长度为18000条RISC-V指令。
证明过程本身还能暴露模糊测试难以触发的缺陷，模型被允许直接修补后重新生成规格并继续证明。 模糊测试通常只变异1 MB以内的小输入并依赖代码覆盖率引导，因此长期漏掉需要大输入或特定调用序列的路径。 在一个库的解压器副本中，Claude发现仅在约20 MB、具有罕见特定布局的输入上触发的计数器下溢和越界写；另有图像解码器的越界读需要64 MB输入和超过2 GB内存。
启示与展望
已展示的范围是Linux上单线程、静态链接、内存预算固定的RISC-V二进制，输入上限64 MB，且只覆盖各库中被验证的模糊测试入口点而非整个库。
证明成立不等于代码无缺陷：证明检查器无法判断规格是否与现实机器一致，ASan也不检测所有内存安全缺陷，调用方误用库仍可能造成内存破坏；此外单条证明可能消耗数亿token，成本仍是推广障碍。