Anthropic称Claude为123个开源库完成形式化验证
热点事件持续更新
Anthropic称Claude为123个开源库完成形式化验证
2 篇报道2 个报道来源2 小时前更新
先了解这件事
AI 综述
Anthropic 发布研究称，与 Theorem 合作，用 Claude 将 OSS-Fuzz 模糊测试转化为规格，对 123 个开源库的 239 个入口点完成汇编级（RISC-V）形式化安全证明，生成约 1.8 亿行 Rocq 证明。 Anthropic 称，证明覆盖任意小于 64 MB 的输入及所建模的 Linux 系统响应和内存布局，程序总会正常退出，不触发内存安全错误或断言失败；前提是程序为单线程静态二进制、内存预算固定，运行在 RISC-V 1 CPU 的 Linux 上。Anthropic 表示已公开部分证明及 RISC-V 和操作系统语义，供他人验证和复用。 Anthropic 称，这突破了形式化验证过去仅适用于小型代码库、或需大量专家人工投入的限制。上述规模和效果均为 Anthropic 的说法。
AI 根据报道生成 · 2 小时前更新
最新进展10月23日 06:01
Anthropic 发布博客：用 Claude 大规模形式化验证开源软件安全性报道时间线
沿着报道，了解事件的不同侧面。
10月23日
- Anthropic精选Anthropic 发布博客：用 Claude 大规模形式化验证开源软件安全性
Anthropic 在 Frontier Red Team 博客发布研究，介绍用 Claude 大规模进行形式化验证的方法。与 Theorem Labs 合作，团队在数周内为超过一百个真实开源库证明了安全属性，突破了形式化验证过去仅适用于小型代码库或需大量专家人工的限制。全文见 https://www.anthropic.com/research/formal-verification。
10月22日
- Anthropic：Research精选Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明
Anthropic 与 Theorem 合作，用 Claude 将 OSS-Fuzz 模糊测试转化为规格，对 123 个开源库的 239 个入口点证明了任意 64 MB 以下输入不崩溃，生成约 1.8 亿行 Rocq 证明。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。