News
Anthropic 报告：Claude 辅助验证 123 个开源库的限定安全性质
Anthropic 与 Theorem 报告，Claude 在 123 个开源库的测试入口上辅助生成形式化证明，验证特定模型和输入约束下不会出现崩溃等问题。成果不代表这些库已被完整证明无漏洞。
Anthropic 与 Theorem 发布形式化验证研究：团队利用 Claude 辅助生成证明，在 123 个开源库的相关可执行程序上验证特定安全性质。研究说明，证明覆盖的是被建模的单线程、静态编译 RISC-V 程序，在固定内存预算、输入小于 64 MB 等假设下不会发生内存安全错误或断言失败。
这不是对 123 个库全部功能、所有平台或所有漏洞的无条件安全保证。Anthropic 表示已公开部分证明，供外部核验和复用；其价值在于探索把形式化验证扩展到更多真实软件的工作流程。参考：研究说明。