Anthropic 用 Claude 为 100+ 开源库写下汇编级安全形式化证明
AnthropicAI · x · 2026-10-23
Anthropic Frontier Red Team 与 Theorem 合作发布研究：用 Claude 在数周内为 100 多个真实开源软件库在 RISC-V 汇编代码层面证明了安全属性，号称是首次用 AI 在汇编级对生产软件做大规模形式化验证。
关键点：
- 形式化验证能证明代码不存在特定 bug，但历史上只适用于小型代码库或需大量专家时间；LLM 让大规模形式化证明首次变得可行。
- 写证明过程中，Claude 还发现了多年来即使数万亿次测试都未暴露的 bug。
- 背景动机：LLM 越来越擅长将多个看似无害的漏洞链成关键利用（如 Linux 内核近期披露 1000+ 漏洞），传统防御不再足够。
- 作者判断：随着模型能力提升，形式化验证将成为安全软件开发的必备环节。
「模型」频道最新
- Boundless 推出去除拒答的 DeepSeek V4.1 Flash,专供防御性安全测试 — MoonL88537 · 2026-10-23
- 模型处于"恐怖谷"?研究者提醒:别大意,Agent 仍会删库跑路 — danielrock · 2026-10-23
- 社区发布 Qwen 3.8 Flash Next 去审查量化版，4-bit 附 Strata 全套文件 — jjusko20 · 2026-10-23
- 爆料称 Anthropic 正训练对标 OpenAI 内部模型的新模型 — imjustnewatai · 2026-10-23
- AI 研究者：Claude 替我完成了多年前放弃的繁琐研究任务 — MikePFrank · 2026-10-23
- Dream Labs 出 stealth:双手机器人基座模型 Dream-1,时租仅 3 美元 — scott_e_reed · 2026-10-23