|
Anthropic与形式化验证团队Theorem公布了一项用Claude辅助证明软件安全属性的研究：他们在123个开源库的239个测试入口上生成了机器可检查的证明，覆盖部分编译后的程序在限定条件下不会崩溃或触发内存安全错误。
这项工作的关键点不只是让模型找漏洞，而是让Claude生成形式化证明，再由Rocq证明检查器验证。研究中，程序被编译为RISC-V二进制；结论针对特定入口、输入大小不超过64MB，并依赖单线程、静态二进制、固定内存预算及所建模Linux/RISC-V语义等前提。Anthropic还表示，尝试证明的过程本身发现了数百个问题，并修复后继续验证。
边界也很重要：这不是对123个库整体“无漏洞”的认证，未覆盖的功能、规格之外的问题以及可信模型本身仍需独立评估。它展示的是AI辅助形式化验证开始扩展到真实软件的一种路径。
官方研究：
https://www.anthropic.com/research/formal-verification |
0