Anthropic 用 Claude 证明 100+ 开源库汇编级安全属性
AxSaucedo · x · 2026-11-03
Anthropic Frontier Red Team 与 Theorem 合作发布报告，展示 LLM 让形式化软件验证首次具备大规模可行性。
- 用 Claude 为超过 100 个真实开源库写出机器可检验的安全证明，覆盖到 RISC-V 汇编代码层面，据称是首个 AI 对生产级软件做汇编级形式化验证的大规模实践
- 写证明过程中 Claude 发现了潜伏多年、即便万亿级测试运行也未曾暴露的 bug
- 论证背景：AI 让发现漏洞变得容易（如 Linux 内核近期披露上千个漏洞），传统防御手段已不足，需要「证明代码无 bug」的保证；形式化验证过去需要多年专家投入，如今可规模化
- 作者判断：随着模型能力提升，形式化验证将成为安全软件开发的标配环节
「安全」频道最新
- 曝 14T 参数 Anthropic "numbat" 泄露 checkpoint 系伪造：权重可由随机种子复现 — djcroman · 2026-11-03
- zkSNARK 可验证算力用途，或成 AI 监管的硬件审计工具 — teortaxesTex · 2026-11-03
- 调查：95% 亚太高管自认能解释 AI 决策，仅半数能还原过程 — mikeflache · 2026-11-03
- 英国政府发布 2026 企业 AI 采用调查报告：116 页全景数据 — mikeflache · 2026-11-03
- CERT-EU 演示 Agent 插件后门：一句 lgtm 即窃取凭据 — TechNadu · 2026-11-03
- 低价模型多次采样检出 80% 漏洞，成本仅前沿模型 13% — andreamichi · 2026-11-03