Anthropic 用 Claude 证明 100+ 开源库汇编级安全属性，还揪出潜伏多年 bug
chrisrohlf · x · 2026-10-23
Anthropic 前沿红队与 Theorem 合作发表论文，展示 LLM 正让形式化软件验证首次具备大规模实用价值。
- 团队用 Claude 为超过 100 个真实开源软件库生成了 RISC-V 汇编代码层面的形式化安全证明，据称是首个在汇编级别对生产软件做大规模 AI 形式化验证的工作
- 形式化验证过去需要专家数年心血，难以用于真实项目；LLM 让大规模生成证明成为可能，使「已证明无 bug」可成为软件开发流程的一部分
- 写证明过程中 Claude 还发现了多年未被发现的 bug——尽管这些代码经历了数万亿次测试运行
- 作者认为随着模型能力提升，形式化验证将成为安全软件开发的核心环节；背景是 Linux 内核等重度测试的软件近期仍披露了 1000+ 漏洞，AI 已能轻易发现并串联漏洞
所属事件:Anthropic 用 Claude 为百余开源库完成汇编级形式化验证(4 条相关)→
「安全」频道最新
- FDA 批准个性化新抗原癌症疫苗：每位患者产品皆不同 — alex_peys · 2026-10-23
- Reddit 热议网络安全圈震荡：AI 驱动攻击让防御方措手不及 — Anen-o-me · 2026-10-23
- 爆料称去除护栏的 GLM-5.3、DS V4.1 开源模型已可被任意滥用 — khademinori · 2026-10-23
- AI 发现 PHP2Shell 高危漏洞,波及全球约 70% 网站 — AIFlow_ML · 2026-10-23
- 从业者评本周网络攻击事件:开源维护模式风险再受审视 — herbiebradley · 2026-10-23
- 仅 8% 云厂商支持 OIDC,开发者呼吁彻底告别长期 API 密钥 — cramforce · 2026-10-23