微软研究院给 Agent 的代码做证明，然后自己写了四个限制

摘要

微软研究院 11 月 5 日公开的 PDD Kit，把开发者的自然语言意图转成 Verus 形式化规格，证明 Agent 写的 Rust 代码"对每个输入"满足规格，证明够不到的部分退回测试。它在一个约 5000 行的 Rust 商店应用上只验证了登录逻辑，并且明确写了四个限制：只支持 Rust、仍是研究原型、证明仍需真实投入、规格本身可能写错。这篇不复述产品介绍，而是把它拆成测试团队能用的三件事：怎么划证明与测试的分界、怎么用变异测试识别空转条款、怎么把证据分级写进 CI。含一份门禁分级表和一段可跑的变异检查脚本骨架。 

先说清楚一个容易被略过的细节：这套工具的名字叫 PDD Kit，官方解释是 Proof-Driven Development Kit，证明驱动开发。它做的事不是"让 AI 写得更准"，而是"让 AI 写完之后，有一台机器能检查它有没有偏离你批准过的话"。

微软研究院这篇博客里有一句话，我认为是整篇文章的价值所在：计划本该是你和编码 Agent 之间的契约，但没有任何东西强制 Agent 遵守它。Agent 可以漂移，实现一个稍微不一样的东西，然后写出对自己的实现能通过的测试。CI 因为测试数量和质量的失衡而膨胀，覆盖率看起来健康，而你要求的和实际交付的差距，一直藏到某份缺陷报告或者某个刁钻的边界用例出现。

做过评审的人对这段话应该有生理反应。因为这不是一个新问题，只是被放大了。

一个可以构造的现场

假设一个场景（业务推演，非任何公司真实事故）：你们团队要让 Agent 给一个订单结算模块加"优惠券叠加"能力。策划书三十行，说了五件事——券能不能叠加、叠加顺序、互斥规则、退款时怎么分摊、超出上限怎么办。Agent 交回来一万行代码，其中六千行是测试。

你打开 PR，看到四百多个测试用例，覆盖率报表漂亮。你抽查了三个用例，逻辑都对。你合了。

问题在于：那四百多个测试，是 Agent 照着它自己写的实现反推出来的。它如果一开始就把"互斥规则"理解成了"同类型券互斥"，测试就会全部围绕"同类型券互斥"来设计，而且每个都会通过。你抽查的三个用例，恰好也在它的理解框架里。

这就是官方那句话的工程含义：测试在验证"它建了什么"，不是在验证"你要了什么"。

他们怎么做的：把"能证的"和"只能信的"分开

PDD Kit 的运行环境是 GitHub Next 的 Chopin，一个多人实时协作的规划界面。流程分两半。

前半段是谈意图。团队成员用自然语言把要什么说清楚，工具扮演一个挑剔的评审者，问那些"细心的评审者会问的问题"，边问边解释相关代码，答案落进一份叫 intent artifact 的文档。这份文档是意图和规格之间的桥。可形式化的部分被写成 Verus 规格；不能形式化、只能靠信任的部分，被写成非形式规格，转成测试。官方明确说，全程不需要形式化方法背景。

前后两半之间有一道很关键的关卡：两个评审代理会对着推导出来的规格挑漏洞，直到评审者一致认为规格站得住；规格精炼在后台跑，同时吸收用户的实时反馈。最后由团队签字。

后半段是证明和收口。签过字的计划被拆成小任务（登录那个例子里是 7 个），每个任务走同一个循环：编码代理写实现和证明，Verus 对着形式规格检查；信任边界内的部分配计划里写好的测试；一个 LLM 验证器并排读计划、规格、结果，专门找"既没有被证明、也没有通过检查"的空档，找到了就退回编码代理，直到清零。如果空档出在规格本身（比如两条需求互相矛盾），它不硬修，而是作为一个决策退还给开发者。

真正让我觉得这套东西值得测试团队看的，不是"能证明"，而是它把边界画出来了。

登录那个案例里，签字的可信部件共六块：两次数据库查找（按邮箱找客户、按用户名找管理员）、密码校验封装、令牌签发、过期时间计算（读时钟）、数据库错误转 500、以及登录处理器外壳。官方原话是，其中两块承担最大的权重——密码校验关乎所有密码承诺，两次查找关乎"令牌指向哪个账户"的所有承诺。测试支持它们，但没有任何东西证明它们。

这句话翻译成测试语言就是：你团队里最该被重点测的那两块，正好是证明管不着的两块。

变异测试：识别"能验证但什么都没约束"的规格

这套流程里有一个设计我认为是专门防自欺的，值得单独拎出来讲。

模型自己写规格时，容易给出"弱的、能验证但几乎排除不了什么"的不变量。官方把这个叫 vibe verification，氛围验证。防法是：pdd-prove 在代码的临时副本里，针对每一条 ensures 条款各植入一个 bug——比如"拒绝所有人"、比如"先查用户名再查邮箱"——然后要求 Verus 在对应条款上拒绝这个变异体。如果有变异体通过了，说明那条条款什么也没兜住，它被当成缺口退回。

我建议任何做 AI 生成测试的团队把这个思路抄过来，成本极低，效果直接。下面这段不是 PDD Kit 的代码，是我按它的做法写的一个最小骨架，用来检查你自己的断言集：

import copy

def mutation_check(assertions, mutate, run):
    """
    assertions: 断言表达式列表（每项对应一条要检查的规则）
    mutate(i): 返回注入第 i 个错误的实现副本
    run(impl, expr) -> bool   # True 表示通过
    返回：哪些断言在注入错误后依然通过（即空转）
    """
    hollow = []
    for i, expr in enumerate(assertions):
        broken = mutate(i)
        if run(broken, expr):      # 实现被改坏了，断言还是过
            hollow.append((i, expr))
    return hollow

三个坑必须提前说清楚，不然这段代码会害人。

第一，mutate 必须真的能改坏实现。用"删掉一个参数校验""把余额加改成减""把超时从 60 秒改成 0 秒"这类语义级改法，比用字符串替换靠谱。字符串替换改坏的是语法，编译不过的变异体不算数。

第二，有些条款天生就"什么都没约束"，因为它约束的是另一个方向。官方专门讲了必须双向证的问题：只有"密码正确才给令牌"这一条，一个"拒绝所有人"的登录也能满足；你要再加一条"密码正确时必须给令牌"，这个变异体才被排除。所以空转不一定代表条款坏了，可能代表你只写了一个方向。

第三，变异检查跑在临时副本里，不能碰生产路径。这条听起来像废话，但我在真机上见过反例。

落回测试团队：证据分级门禁

把这个机制搬进 CI，最难的不是技术，是"什么算证据"这件事要重新定义。

官方的做法很值得抄：pdd-ship 把 Verus 检查接进 CI，和经验测试并列。此后无论人还是 Agent 改登录，"证明被破坏则构建失败，就像测试失败一样"。另一件事更反直觉——因为证明覆盖所有输入，它会剪掉那些只重复检查已被证明内容的测试，保留守护信任边界的测试。结果是 CI 同时变得更强、更精简。还有一个细节：证明的检查是确定性的，模型负责写规格、写代码、写证明，但只有 Verus 这次运行决定过不过。

我把这套东西整理成一张三档表，可以直接贴到团队的分级规范里：

表格里最容易吵的是 C 档。我见过团队把模型自评当成"额外的信心"，然后拿它替代 B 档的部分用例。这是把证据等级弄混了。C 档的正确定位是"发现问题的线索"，不是"发布放行的依据"。

这里有一条我认为比表格更重要的工程纪律：A 档不允许覆盖 B 档。 官方剪掉的只是"重复检查已证内容"的测试，保留的是守护信任边界的测试。你把它们剪掉的顺序反过来，就会出现"证明覆盖了登录但不覆盖 bcrypt"这种最危险的组合。

必须先说清楚的四个边界

这套东西不是万能钥匙，官方自己也写了限制，而且写得很直白。

只支持 Rust。原话是 PDD Kit 目前只验证 Rust，因为 Verus 就在 Rust 上工作。其他语言的代码可以移植到 Rust 再用同一套规格检查，非 Rust 项目可以通过绑定调用已验证的 Rust。对我们多数团队来说，这意味着短期内它更像一个"高价值小内核"的验证手段，不是全仓库方案。

仍是研究原型。官方在"What to Expect"一节里再次强调了这一点。

证明仍然要真投入。原话是证明仍然需要真实的投入，主要花在产出证明本身上。小模块通常几秒，较大代码库能到几分钟。这句话解释了为什么它先拿登录逻辑开刀——不是因为登录最重要，是因为登录足够小、边界足够清楚。

规格本身可能写错。这是我认为测试工程师最该记住的一条。证明只说明代码满足规格，不说明规格就是你的本意。官方因此强调需求显式化、歧义识别，以及开发者在验证之前参与规格评审。换句话说，它把评审从"看代码"挪到了"看意图"，而看意图这件事，本来就是测试最该参与的地方。

还有一个需要如实标注的观察：官方博客没有公布缺陷总数、没有公布被证明覆盖的代码行占比、也没有给出"用 PDD Kit 与不用"的对照结果。这几项缺失意味着它不能作为效果对比的基准，只能作为方法参考。第 04 篇会专门讲"博客里没公布的那几个数字"对一个评测设计意味着什么。

测试团队可以做的三件事

第一，画一次你自己的三层边界图。拿一个核心链路（登录、支付、下单都行），标出哪部分你觉得"逻辑上应该是对的"、哪部分是"我信这个库"、哪部分是"没人管"。第三类里通常藏着最大的洞。

第二，把现有断言跑一次变异检查。不用等证明工具，先用手工注入十个语义级错误，看有几个断言还是过。这一小时的收益比很多"覆盖率提升 3%"的项目高。

第三，在门禁规范里加上 A/B/C 三档的定义，明确"C 档不卡合并"。这件事不需要任何新工具，只需要一个下午的共识。

我在前面说过，真正稀缺的不是代码，是"这句话是不是你要的"这个判断。Agent 把判断的对象从代码挪到了意图，而测试团队一直是离意图最近的那批人。这是压力，也是位置的变化。