一句话定位：这不是"Agent 写的代码能不能跑"，而是"你能不能说清它满足了什么、又在哪里没人给你担保"——被测对象是规格本身与证明覆盖的边界，不是某一条用例。同样的方法可迁移到订单退款的状态机、权限变更的准入判定、审批流的分级会签、发布开关的降级条件。
摘要
微软研究院 2026 年 11 月 5 日公开了 PDD Kit 的一份实验记录：在一个约五千行的 Rust 全栈应用里，只用两句话描述登录需求，由 Verus 对 login_flow 等函数体做全输入证明，证明够不到的地方退回到测试，并在 PR 描述里逐条标注"这是证明"还是"这是检查"。这篇不复述工具用法，只做一件事：把它的"证明边界"翻译成测试团队能直接用的验收动作——怎么写出一条不会被"拒绝所有人"这种实现骗过的规格、怎么识别只约束了一半的断言、以及为什么"通过"这两个字在证明体系里要降级成"证据"。核心结论一句：先划出没人担保的那一圈，剩下的证明才有意义。
一个登录页要满足两条要求：只有密码对才发 token，只有管理员账号才发管理员 token。
这两句话听起来已经足够。微软研究院的团队把它们交给 Agent，由 Agent 写实现、写证明，最后合并进一个叫 Pet Store 的 Rust 全栈应用——后端 Axum 加 SQLite，前端 Leptos 编译成 WebAssembly，约五千行 Rust。整个过程中，开发者只审阅了意图，没有逐行读生成的代码。
听起来像是"Agent 自己把自己验证了"。但原文里有一句更值得注意的话：计划本该是人和 Agent 之间的契约，可没有任何机制强制 Agent 遵守它。
这句话是那篇 2026 年 11 月 5 日博客的开篇命题。它不是在说 Agent 不可靠，而是在说一件更麻烦的事：我们过去靠"人读 diff"建立的信任，在代码量以万行为单位产生的时候失效了。原文给的判断很直白——读完整份 PR 的每一行，"doesn't scale to this new way of work"。
我关心的是它给出的替代方案里，有一个东西是测试工程师可以直接拿走的：它把"通过"分成了两个等级。
两句话的规格，为什么会漏掉一半
先看那条登录需求最容易被写成什么样。
"只有密码正确才发 token"——如果只写这一条，一个拒绝所有人登录的实现完全满足它。谁都没拿到 token，所以"只有密码对的人才拿到"这个条件从未被违反。
原文把这一步单独拎出来讲，做成一张决策卡：只证明一个方向是不够的，必须把逆命题补上——密码正确时也一定能拿到 token。两条合起来才是"当且仅当"。
这是测试用例设计里一个老问题的新面孔。我们写断言时习惯写"错误输入应被拒绝"，很少同时写"正确输入应被接受"，因为后者在手工测试里是默认动作：测试员会用正确密码登一次。可一旦断言交给 Agent 写，那条"默认动作"就不存在了——原文对这个的描述是，Agent 写的测试"usually check what it built, rather than what you asked for"。
我在团队的用例评审里见过太多次同类问题：一条断言只覆盖了禁止路径，没有覆盖放行路径，测试通过，覆盖率涨了，风险还在。这不是 Agent 带来的新问题，是 Agent 把它从"偶尔疏忽"变成了"系统性默认"。
下面这张图就是那个"一个方向 vs 两个方向"的差别，以及它怎么落到登录这个具体动作上。
证明到哪一步就停了，这是必须写进验收的字段
第二个可以拿走的东西更硬：它要求把"证明覆盖到哪、哪里只是被信任、哪里只是被测试"画出来，并且在开发者确认之前就画出来。
PDD Kit 的做法是拆成三档。Proved：login_flow、login_core、lookup_target、decide_login、issue_token 的函数体对所有输入满足契约。Trusted and tested：两个数据库查询、bcrypt 的 check_password、时钟、token 签名、数据库错误信息、请求解包——六项，由开发者逐条接受，再由计划里写好的测试去检查。Assumed：Verus、Rust 编译器、Z3 工具链以及 Verus 标准库。
原文自己承认这是最薄弱的地方："Tests support them, but nothing proves them."
这句话值得抄进任何一份 LLM 辅助开发的验收模板。因为我们平时写的"已验证"三个字，实际含义可能是这三档里的任意一档，而下游读者无法分辨。一个"登录已验证"的结论，可能是"核心逻辑对所有输入成立"，也可能是"六个依赖被接受之后、由几个测试抽查过"。这两种说法的风险量级差着好几倍。
我建议把这个字段做成必填：这一版证明覆盖了什么、哪些部件是被接受的、接受它们的人是谁、哪几条测试在兜底、兜底测试覆盖到什么粒度。 少了最后一项，前四项都不可审计。
这两张图放在一起看，会发现它们回答的是同一个问题的两个方向：一张说"你的规格可能只覆盖了一半场景"，另一张说"你的证明可能只覆盖了一半代码"。测试团队常见的工作方式刚好卡在中间——不加区分地把两者都叫"验证通过"。
把边界写下来之后，工作方式会变
原文给了一条具体做法：pdd-plan 先读代码、提问，生成一份给人看的意图工件（intent artifact）；pdd-prove 把批准的计划拆成小任务图，登录这个例子是七个任务，每个任务循环执行"写实现和证明 → Verus 校验 → 写可信边界的测试 → 由 LLM 校验器对照计划和规格找缺口"；pdd-ship 把 Verus 检查塞进 CI，证明失败即构建失败。
还有一处细节我特别喜欢：每一条 ensures 子句都会被植入一个 bug 做变异检查，Verus 必须拒绝它。如果拒绝了，说明这条子句真的有约束力；如果没拒绝，这条子句就是装饰。
这一条可以直接搬到任何断言体系里，不需要形式化工具：把手上的每一条关键断言，手动改坏一次，看测试会不会红。 不会红的断言，不管写得多像样，都是文字。
真实工作中更常见的困难在这里：很多团队根本没有一份可执行的规格。原文对此的说法是"计划本该是契约"，但计划常常只活在对话里，没人再打开它。如果连契约都不存在，所谓"证明"就无从谈起——这也是我读完这篇之后最想说的一句：形式化验证真正的成本不在工具，在把意图写成可判定的句子这件事上。
换到订单退款上，这套东西长什么样（业务推演）
以下是推演，不是任何公司的真实实践。
假设你的团队让 Agent 改一版退款状态机。意图写下来大概是三句话：未支付的订单不能退款；已退款的订单不能再退；退款成功必须留下一条流水。
用"两个方向"的思路检查第一条：只写"未支付不能退"是不够的，必须同时写"已支付且未退款的订单可以退"。少了后半句，一个把退款按钮全部禁掉的实现也能通过。
用"三档"的思路检查 check_password 的类比物：支付网关的签名校验通常是外部库，证明够不到，只能被接受、被测试。那么验收模板里就该写清楚：签名校验这一环没有证明，只有两条测试，一条正常签名、一条篡改签名。如果下游读者拿到的是"退款状态机已验证"，他不会知道这一层。
用"变异检查"检查第三条：把"写流水"那一行注释掉，看断言会不会红。如果只是断言了状态变成"已退款"，流水缺失依然通过——那这条断言同样没有约束住你想要的东西。
这个推演里没有出现任何新的技术名词，但它把一篇读起来很"研究院"的文章，落到了测试团队能排期的事情上。
它解决不了的，原文自己说了
必须把这一面写清楚，否则会变成又一篇吹工具的文章。
第一，只管 Rust。Verus 只支持 Rust，其他语言要么移植，要么通过绑定调用。多数团队的主力栈不是 Rust。
第二，规格对不代表意图对。原文写得很克制："A proof shows the code meets the spec, not that the spec is what you meant." 规格本身写错，证明只会更确定地把你送到错误的地方。
第三，它不承诺"会不会完成、多快完成"。规格只说"若登录返回则如何"，请求挂住或者查询很慢，都不违反任何子句。
第四，也是最要命的一条：证明的强度取决于那六个被信任的部件，其中 check_password 和两个查询承担了大部分重量。原文说得很直白——测试支撑它们，但没有任何东西证明它们。
所以这篇文章的结论不该是"上形式化验证"，而是：无论你用什么方法，验收结论必须带上它的覆盖边界。 没有边界的"已验证"，比没验证更危险，因为它让人停止追问。
下周可以做的三件事
不必等工具链就绪。
一，挑一条你团队最依赖的断言，检查它有没有写反方向。只有"异常输入被拒"而没有"正常输入被放行"的，全部补上。做完之后你会发现有些用例一直是空转的。
二，给现有的"已验证"结论加一列，写明这一条属于哪一档：被证明、被接受并由测试兜底、还是仅被抽查。填不出来的，就是风险敞口。
三，挑三条最关键的断言，各改坏一次，记录哪些没红。没红的改成能红的——通常不是加断言，而是换断言的对象：从"接口返回 200"换成"流水表里多了一行且金额相等"。
原文那个实验里最打动我的不是证明本身，而是 PR 描述里那句标注：这条登录需求是形式化验证的，那条是经验检查的。它把"我知道到哪里为止"写在了交付物上。 这件事跟用不用 Verus 无关，今天就能做。
本文部分内容参考了霍格沃兹测试开发学社整理的相关技术资料，主要涉及软件测试、自动化测试、测试开发及 AI 测试等内容，侧重测试实践、工具应用与工程经验整理。
