# Anthropic 研究展示大语言模型如何扩大软件形式化验证规模

> 原标题：LLMs are making formal software verification feasible at a much larger scale

- 来源：Hacker News 首页
- 发布时间：2026-10-22T22:54:43.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/bjb3xiswjl4dw5wyapcrcowix
- 原文：https://www.anthropic.com/research/formal-verification

## 摘要

Anthropic 与 Theorem 使用 Claude，为 123 个开源库的 239 个测试入口完成 RISC-V 二进制级安全属性验证。研究将既有模糊测试转为形式化规格，由 Claude 修复发现的漏洞并生成约 180 million 行 Rocq，由 Rocq 检查器核验。

## 推荐理由

Anthropic 与 Theorem 将既有模糊测试转为形式化规格，再由 Claude 生成机器码级形式化验证，使验证流程无需重写整个代码库。

## 锐评

用 Claude 吐出 1.8 亿行 Rocq 证明，感觉总算给海量 token 找到了最合算的出路。

形式化验证以前全卡在人手不够，写证明耗时能达到写代码的十倍。把既有测试转成规格，让模型不断去试，写错没关系，只要有 Rocq 检查器在后面卡死就行。只要验证端有数学工具一票否决，就不怕大模型胡说八道。123 个开源库能这么测下来，为这种任务花再多算力我也觉得值。