# 从「找漏洞」到「证明没漏洞」：Anthropic 用 Claude 为 123 个开源库写出机器可验证的安全证明
- 事件 ID：evt-20261023-04
- 日期：2026-10-23　截至：2026-10-23 08:30（北京时间）
- 证据等级：企业宣称、媒体报道
- 来自：https://www.newtoken.link/daily/2026-10-23#evt-20261023-04
为什么重要：10-22 那期的判断是安全的瓶颈从「找得到」变成「修得完」，这项研究给出了第三步：修完之后，能不能证明没有了。形式化验证过去贵到只有航空电子、操作系统内核才用得起，Anthropic 举的例子是 seL4 内核写代码用了 2 人年、验证用了 20 人年。如果模型能把这件事的成本降一到两个数量级，开源基础软件、金融和工业控制系统就可能第一次拥有「数学上保证不崩」的版本，这会改变软件采购和保险的标准。我的判断是，AI 安全竞赛的下一块高地是「可证明的安全」，谁先把它做成可复用的工具链和合规证据，谁就能卖给受监管行业。反方检验：证明只覆盖「不崩溃、不越界」这一类属性，不覆盖逻辑错误和权限设计问题；单线程、64 MB 以内等假设与真实服务器环境有差距；Anthropic 没有披露消耗的算力和成本。
## 来源（4 条）
- [Anthropic：LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification)（企业宣称）
- [研究附录](https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf)（企业宣称）
- [@AnthropicAI 帖文](https://x.com/AnthropicAI/status/2113390212911083894)（企业宣称）
- [Unite.AI](https://www.unite.ai/anthropic-says-claude-proved-security-properties-across-123-libraries/)（媒体报道）