Anthropic 用 Claude 数周内形式化验证百余个开源库，前 OpenAI 员工自曝形式化验证宣言往事
ethanCaballero · x · 2026-10-24
两条线索交织的形式化验证（formal verification）故事：
- Anthropic 官方研究：与 Theorem Labs 合作，在 Frontier Red Team 博客发布新方法——不再要求开发者在 Rocq 或 Lean 中手写规范，而是用现有 fuzz harness 作为规范、让 LLM 生成机器可检验的证明。团队用 Claude 在几周内证明了 100 多个真实开源库的安全属性，首次把形式化验证扩展到大规模代码库。
- 前 OpenAI 员工 olegmurk 自述：被挤出 OpenAI 前三天，他在核心研究 Slack 发了「形式化验证宣言」，列出 OpenAI 各系统可从中受益的场景，唯一回复的是 Altman 且态度支持。作者借此呼吁 OpenAI 认真投入软硬件形式化验证。
- 技术边界：fuzz harness 只定义部分正确性属性，最简单情形下证明的是崩溃安全（crash-safety）而非完整功能正确性；作者呼吁建设社区维护的开源验证基础设施。
所属事件:Anthropic 用 Claude 数周完成百余开源库汇编级形式化验证(26 条相关)→
「安全」频道最新
- 单人用 AI 智能体攻破百余网站，每次入侵成本仅 50 美元 — OmarUFlorez · 2026-10-24
- USC 论文揭「马赛克泄露」：LLM Agent 拼合多份机密文档泄露敏感结论 — UniversityofSouthernCalifornia · 2026-10-24
- 「AI 找漏洞是诺贝尔奖级成就，不该被谴责」引热议 — chrisrohlf · 2026-10-24
- 安全老兵驳「AI 挖洞是labs的锅」：几十年安全债早就在那 — chrisrohlf · 2026-10-24
- 给 4 岁孩子自动生成睡前故事，如何兜住内容安全？ — Miserable-Shock3552 · 2026-10-24
- Anthropic 内部早称「漏洞末日」,前沿实验室已按网络攻击预期布局 — gerardsans · 2026-10-24