AI生成的形式化证明通过检查器，并不等于整个软件已经没有错误。更准确的问题是：哪一个二进制、哪一个入口，在什么输入与机器模型下，被证明满足哪条属性？遗漏这些条件，“验证通过”就容易变成比证据更大的承诺。

Anthropic于2026年10月22日发布LLM辅助软件形式化验证研究。配套的公开证明与机器模型，让开发者有机会检查具体命题及其边界。下面结合固定项目版本和一个可运行的规格对照，解释怎样阅读这些证据。Read in English。

新闻带来的变化：模型写证明，检查器验命题

这里值得注意的分工，是把生成候选证明交给模型，再让独立的机械检查器判断证明是否符合给定命题。我们不必仅凭模型解释得是否流畅来接受正确性；但命题本身是否描述了需要的行为，仍然需要人检查。证明产出与规格设计，承担不同责任。

该版本的检查流程还会核对二进制哈希，把证明定理绑定到目标陈述，并审计使用的假设。因此，审阅证据不能只看“编译过一个证明文件”，还要看它是否证明了预定的命题。本文只查阅了这些步骤，没有实际运行该流程。

本篇技术依据固定到公开证明仓库的98e995d4版本，对应10月23日的项目快照。这个版本的README列出60个入口、25个库已有证明，使用Rocq 9.2.0。它是一个公开发布子集的状态，不拿它冒充全部研究规模，也不把“已经写出命题”当作“已经完成证明”。

以下工程细节与数量均按这个固定版本讨论，不混用后来更新的研究页面或项目统计。数字的用途是说明发布单位：库、入口、命题与证明并非一一对应。读者如果要评估自己的依赖，应该定位具体入口及对应产物，不能只看库名出现在列表中。

从一个入口，走到一条可检查的陈述

一个测试入口通常会接收输入、调用库函数，并在某些条件不成立时失败。尝试证明这样的入口，就是把“挑很多样本试试看”推进为“对声明覆盖的输入建立论证”。但覆盖集合和要排除的错误都必须先写清楚。它没有自动补出业务尚未定义的需求。

固定版本的构建记录说明将证明关联到特定RISC-V静态二进制。开发者审阅时应把构建产物标识、入口、属性和前提放在同一张记录里。换一个构建、改一段代码或者换运行方式后，应重新确认原论证是否仍适用，而不是沿用一个没有版本信息的“已验证”标签。

例如，假设某解码入口只要求输入处理过程中不触发规定的错误，它是否还要求每个像素都正确？是否比较了预期输出？这些是对规格的追问，不是对这项研究中的某个具体库提出缺陷指控。若期望的是业务结果正确，就需要在规格中表达这个结果与输入的关系。

八个输入，为什么能同时得到两种“通过”

下面的原创教学例子把业务要求设为返回输入本身。identity返回x，constant无论输入是什么都返回0。弱检查只要求返回一个0到8之间的整数且不抛异常。在0至7这八个输入上，两者都得到8/8；如果检查返回值等于输入，identity得到8/8，constant只有1/8。

这不是证明检查器出错，也不是说检查不报错没有价值。两套检查回答了不同问题。返回常数0满足弱要求，却没有满足我们另行提出的业务要求。修复方向是补足规格，而不是要求一个机械检查器猜出未写明的需求。

再看bounded_bug：当x小于8时返回x，其余返回0。只看0至7，它在强检查下也得到8/8；把输入集合扩展到0至8后，就得到8/9，反例是输入8、预期8、实际0。即使在一个集合上确实全部成立，也不能无条件推广到更大的集合。

完整可复现例子与它没有证明的事

程序只用Python标准语法，已在Python 3.15.0运行，八项检查均通过。它穷举两个明确的有限集合，用来展示属性强弱与输入范围；没有调用LLM、运行Rocq、检查公开证明或复现研究结果。这里的8/8不是模型评测分数，更不是现实软件的安全概率。

def identity(x):
    return x

def constant(x):
    return 0

def bounded_bug(x):
    return x if x < 8 else 0

def weak_check(fn, inputs):
    accepted = 0
    for x in inputs:
        try:
            y = fn(x)
        except Exception:
            continue
        accepted += isinstance(y, int) and 0 <= y <= 8
    return accepted

def strong_check(fn, inputs):
    return sum(fn(x) == x for x in inputs)

small = tuple(range(8))
large = tuple(range(9))
assert weak_check(identity, small) == 8
assert weak_check(constant, small) == 8
assert strong_check(identity, small) == 8
assert strong_check(constant, small) == 1
assert strong_check(bounded_bug, small) == 8
assert strong_check(bounded_bug, large) == 8
assert bounded_bug(8) == 0
assert identity(8) == 8
print('weak constant: 8/8')
print('strong constant: 1/8')
print('bounded bug, 0..7: 8/8')
print('bounded bug, 0..8: 8/9')
print('counterexample: input=8, expected=8, actual=0')
print('8 checks passed; finite enumeration, not a Rocq proof')

如果将这个方法用于代码审阅，可以先写一个明显错误但可能满足弱规格的替代实现，问规格能否将它排除。这个“错误实现对照”帮助发现规格遗漏；它不是对所有错误实现的完备搜索，也不能替代正式证明。本文的constant就是这样的对照，设计简单，读者可以直接逐项核对。

不报错，还需要补问是否结束

陈述文档将agreement与halts分开：前者不排除不结束的运行；固定发布版本的README也说明，已发布证明没有证明halts陈述。没有报错的执行，也可能一直运行而不给出业务结果。对一个必须响应请求的服务，内存安全、结果正确与最终返回是三个不同问题，不能因为解决其中之一就省去另两个。

本文没有真的启动一个无限循环来演示。逻辑上，“不存在错误状态”没有单独给出结束时间，也没有给出吞吐或服务延迟。如果工程目标包含响应，评审记录就要为终止、资源预算以及服务时限分别寻找证据。形式化属性与线上观测可以互相补充，但不能把证明标签换算成没有测过的延迟保证。

机器模型与部署现实之间的接缝

与证明配套的固定LPS范围说明明确列出了建模边界，包括单线程、部分进程与文件环境以及若干未检查的外部假设。因此，看到一个定理已被机械检查，仍要问部署环境是否落在它的前提内。证明检查器验证论证，不能直接验证所有模型描述都等于真实系统。

这里的工程做法可以很具体：为准备采用的产物填写三栏。第一栏是产物与版本；第二栏是入口和所证属性；第三栏是部署中是否满足其前提及如何判断。如果某一栏缺失，就把结论限制在已经确认的范围内。不要先把一个RISC-V模型下的结论贴到另一个架构、动态链接或多线程部署上，再事后找理由。

更换依赖以后，也应重新核对这三栏。源码版本、编译方式、证明文件与部署产物的关系需要可追溯；CI上一次绿灯不能独自说明当前产物受同一命题覆盖。本文没有对某个线上项目作这种对应检查，因此不宣称任何读者项目已经得到验证。

开发者现在能用这条新闻做什么

最直接的收益，是把审查问题从“AI写的代码可信吗”细化为“我正在接受什么可检查的主张”。先挑一个重要且边界明确的入口，写清输入、输出和失败条件，再判断现成测试是否表达了这些要求。证明成本可能变化，规格缺失却不会因为模型更强而自动消失。

实际试用公开工具前，可沿项目文档核对版本、构建产物和检查步骤；完整复核还需要相应环境与资源。本篇没有安装或运行其证明工具链，也没有提供性能或费用估算。它提供的是新闻背后的阅读方法和可运行的规格对照，帮助先识别值得检查的问题。

站内此前的AI搜索完成声明核验讨论任务完成需要什么证据。形式化验证把这个问题进一步具体到命题、产物与前提：检查通过的证据很强，但强在它真正检查到的范围内。

来源：10月22日Anthropic原报道、原计划前的公开证明版本及机器模型范围说明。本文依据研究说明与项目文档，没有独立重检Rocq证明；图形、有限穷举例子和审阅记录方法为原创。文章日期保留北京时间2026年10月23日16:00，实际于2026年10月28日补发。