先了解这件事
Anthropic于2026年10月22日发布研究,称Claude为开源库生成机器可检验的安全性质形式化证明。据Unite.AI报道,Anthropic与Theorem合作,Claude为123个开源库中239个fuzz测试入口在RISC-V汇编代码层面生成证明,并修补发现的漏洞;证明覆盖64 MB以下任意输入及建模的Linux系统响应与内存布局,总量约1.8亿行Rocq,典型证明约60万行。Anthropic表示部分证明及RISC-V与操作系统语义已在GitHub发布,但会保留可能暴露未修补漏洞的证明;Theorem通过OSS Verify计划向符合条件的开源项目免费提供同一流程。钛媒体报道称,该研究将验证推进到汇编指令层面,并指出形式化验证只能证明程序在特定假设和范围内满足预设性质。
AI 根据公开报道生成
最新动态 · 相关讨论
Vinod Khosla 参与了这场讨论事件进展
1 个已确认进展
- 来源：Unite.AI
报道与讨论时间线
按时间查看正式报道与传播讨论；两类内容的证据等级保持独立。
10月23日
钛媒体 · AGI
Anthropic 报告：Claude 生成 1.8 亿行 Rocq 证明，将形式化验证推进到汇编层
Anthropic 与 Theorem Labs 团队发布报告，称 Claude 针对 123 个开源软件库的 239 个程序入口生成约 1.8 亿行 Rocq 证明代码，并发现修复数百个 Bug。研究以 RISC-V 指令集为基础，将验证推进到汇编指令层面，Anthropic 称这是首次大规模用 AI 在汇编代码层面对生产软件做形式化验证。文章同时指出，形式化验证只能证明程序在特定假设和范围内满足预设性质，且攻防双方使用 AI 的成本并不对等。
Unite.AI精选
Anthropic 称 Claude 为 123 个开源库完成安全属性形式化证明
Anthropic 于 2026 年 10 月 22 日发布研究，称与 Theorem 合作，Claude 为 123 个开源库中 239 个 fuzz 测试入口在 RISC-V 汇编代码层面生成了机器可检验的安全属性形式化证明，并修补了发现的漏洞。证明覆盖 64 MB 以下任意输入及建模的 Linux 系统响应与内存布局，总量约 1.8 亿行 Rocq，典型证明约 60 万行，对应二进制中位长度 1.8 万条 RISC-V 指令。Anthropic 表示部分证明及 RISC-V 与操作系统语义已在 GitHub 发布，但会保留可能暴露未修补漏洞的证明；Theorem 通过 OSS Verify 计划向符合条件的开源项目免费提供同一流程。
Anthropic
Anthropic 用 Claude 对上百个开源库做形式化验证
Anthropic 前沿红队博客介绍，其与 Theorem Labs 合作，用 Claude 在数周内为一百多个真实开源库证明了安全属性。形式化验证能证明代码不存在某些缺陷，但过去只适用于小型代码库或需要大量专家时间，Anthropic 认为 AI 模型正在改变这一局面。完整研究见原文链接。
本事件热度走势
- 当前
- 16
- 区间峰值
- 41 10月23日 19:00
- 近 24 小时变化
- —
移动指针或点击图表可查看每小时热度；键盘可用左右方向键切换。