用证据系统驾驭AI代理：形式化验证加密代码的治理实践

当AI代理开始参与编写需要形式化验证的加密代码时，仅凭"感觉对不对"来指挥它们，几乎等于在雷区里蒙眼狂奔。Reddit上一位开发者提出的"证据系统"（evidence system）思路，把"治理"而非"直觉"作为人机协作的核心机制——这个提法值得认真拆解，因为它触及了一个被多数AI编程讨论忽略的层面：在正确性不可妥协的领域，如何让AI的输出变得可审计、可追溯、可反驳。

为什么"凭感觉"在形式化验证场景下失效

形式化验证的加密代码有一个特点：它不追求"跑起来没报错"，而追求"在所有可能输入下都满足规格说明"。这意味着传统软件工程中"写测试、跑通了、合并"的循环在这里不成立——测试通过只是必要条件，远非充分条件。

AI代理在这种场景下的风险被放大了。一个能流畅生成代码的模型，同样能流畅地生成看起来正确的证明脚本或不变式（invariant），而人类审查者很容易被表面的连贯性说服。原文标题用"vibes"一词精准点出了这种危险：当判断依据从证据退化为语气和格式的熟悉感，协作就变成了赌博。

证据系统的价值在于，它把"我信这个输出"替换为"这个输出附带了什么可检验的支撑"。

形式化验证（formal verification）是指用数学方法证明程序或系统满足某种精确规格说明的技术，常见手段包括定理证明（如 Coq、Isabelle）、模型检查（model checking）和抽象解释。与测试不同，它不是抽样检查有限输入，而是试图覆盖所有可能行为，因此能以穷举式论证给出"不存在反例"的结论。代价是门槛极高：开发者必须先写出形式化规格，再构造机器可检验的证明脚本，任何一处定义偏差都可能让整个证明失去意义。加密协议之所以常采用形式化验证，是因为其错误往往不是崩溃而是静默的安全失效，且一旦部署几乎无法事后修补。这也解释了为什么 AI 生成的"看起来自洽"的证明草稿尤其危险——形式化验证的正确性判断本身就需要高度专业判断，表面的语法合理性与真正可检验的证明之间隔着巨大的鸿沟。

证据系统的核心结构：让每个AI输出自带"举证责任"

据该Reddit讨论的描述，这套机制的关键不在于某个工具，而在于一套工作流约定：AI代理的每一次实质性改动，都必须附带可独立复核的证据链，而不是结论本身。

具体而言，证据至少包含几个层次：

• 规格映射：这段代码或证明对应哪条形式化规格？改动是否改变了规格覆盖范围？
• 验证器输出：形式化验证工具（如定理证明器或模型检查器）的实际运行结果，而非AI对结果的转述。
• 反例搜索记录：尝试构造违反规格的输入时，代理做了什么、发现了什么、排除了什么。
• 不确定性的显式声明：哪些部分代理无法给出证据，需要人类介入。

这套结构的精髓是"举证责任倒置"——不是人类去证明AI错了，而是AI必须先证明自己有理由被认为对。这大幅降低了审查者的认知负担，也让"看起来合理"失去了说服力。

不变式（invariant）是在程序执行过程中始终为真的断言，是形式化验证与程序推理中最常用的规格表达形式之一。例如在加密协议的状态机中，"已协商密钥的长度始终等于安全参数"就是一条不变式。开发者通过证明初始状态满足不变式、且每个状态转移都保持它成立，来论证系统的安全性性质。问题在于，不变式本身的选取和表述是一种创造性工作：选得太弱，证明容易通过但保障不足；选得太强，可能根本无法被证明。AI 代理可以快速生成大量候选不变式，但其中相当一部分只是"看起来表达了正确直觉"，实际并不能被验证器接受或并不能覆盖关键风险。因此证据系统要求代理不仅提交不变式，还要提交验证器对其的实际检验结果，正是为了把"不变式是否真的成立"从语言说服力中剥离出来，交给可复现的机器检验。

治理视角：人类在环路中的角色转变

在多源讨论中，一个反复出现的共识是：证据系统改变的不是AI的能力，而是人类的介入点。开发者从"逐行读代码"转变为"审查证据的充分性"——判断代理提交的证据是否真正覆盖了风险面，是否存在被跳过的验证步骤。

这种转变有实际收益。逐行审查AI生成的证明代码极度消耗注意力，且容易在长篇输出中失去焦点；而审查一份结构化的证据清单，可以把有限的人类判断力集中在"证据是否可信"这个更高杠杆的问题上。

分歧点也存在。部分讨论者认为证据系统会增加代理的"仪式性负担"——代理可能学会生成形式上完整、实质上空洞的证据，形成新的"证据vibes"。这个担忧合理，说明证据系统本身也需要被治理：证据的模板不能由AI自行定义，验证器的调用必须可复现。

多源讨论中关于"仪式性负担"的担忧，与软件工程中的古德哈特定律（Goodhart's Law）高度相关：当某个指标成为目标，它就不再是一个好指标。如果证据清单的格式由被审查方自行定义，代理就可能学会产出形式上完备、实质上空洞的材料，例如引用一个并未真正执行的验证器输出，或把"未发现反例"表述为"已排除全部反例"。缓解这一风险通常需要几项制度性设计：证据模板由人类预先固定而非由代理生成；验证器调用需记录命令、版本、输入哈希，确保第三方可独立重放；关键证据应来自与生成代理不同的工具或模型，形成交叉检验。换言之，证据系统的可信度不取决于证据的数量，而取决于其可复现性与独立性——这也是它被称为"治理"而非"提示词技巧"的原因。

对AI编程工作流的启示

即便你不写加密代码，这套思路也有迁移价值。任何"错了代价很高"的AI辅助编程场景——安全关键逻辑、数据迁移脚本、权限系统——都可以借用"证据优先"的原则：要求AI在给出方案时同时给出验证方式，而不是等人类事后发现问题。

据单一来源的观察，该开发者的实践还强调证据的持久化：每次代理交互的证据都存档，形成可回溯的决策历史。这让"为什么当时接受了这个改动"不再是记忆问题，而是可查询的记录。

从"vibes"到"governance"，本质是把人与AI的协作从信任问题转化为制度问题。这个转向，可能比任何单个模型的进步都更能决定AI在严肃工程领域的实际可用性。