你来审规格，机器来审代码

GitHub Next 和微软研究院在 10 月 21 日发布了 Proof-Driven Development Kit。它目前是研究预览版，只支持 Rust，而且它提出的论点，是很多跑编码 agent 的团队一直在回避的：如果你已经没法逐行读 diff 了，那就别再假装能读，换个东西来审。

那个「别的东西」是规格说明。在 PDD Kit 的工作流里，由人来批准 spec，然后由机器针对每一种可能的输入，检查实现是否满足它。

五个步骤，以及人坐在哪一环

整个循环是这样跑的。团队先在 Chopin 里规划功能——Chopin 是 GitHub Next 的多人在线 agent 规划工具。然后 PDD Kit 会讨论代码、推断意图，并提出一份用 Verus 写的形式化规格；Verus 是已有的、开源的 Rust 证明语言。人批准的是 spec，不是代码。接着 Verus 证明 agent 生成的代码对任意输入都满足这份 spec。在无法给出完整证明的地方，PDD Kit 退回到测试和 computer-use agent 做经验性检查，最终产出的是一个已验证的 pull request。

这个反转就是全部要点。你审需求，验证器审实现。在 Verus 里，spec 用前置条件和后置条件标注函数，验证器必须把这些条件清掉；而它的保证在某个具体意义上强过一套全绿的测试：测试是抽样输入，证明是对所有输入做量化。

GitHub 自己的说法是，Chopin 加上 PDD Kit，能让团队把 AI 生成的代码直接送上生产而不逐行审阅，且保证强度高于单纯的代码评审加测试。这是厂商在描述自家的研究预览版，不是一个经过审计的结论。别把它握得太紧。

{{INLINE1}}

成本只是挪了位置，并没有消失

很容易把它读成「评审负担解决了」。并没有。它被挪到了流水线的前端，而且变难了，难的程度很容易被低估。

写一份精确到可证明的 spec，和审一段 diff，是两种不同的技能。含糊的需求会产出无法证明的 spec，验证器会以失败的方式告诉你这一点，于是上线的头几周看起来就像「这工具不能用」。实际发生的是：你需求里的模糊之处被提前暴露了，而且是被一个不会用看似合理的函数糊弄过去的东西暴露的。

对那些一直在写没人看的设计文档的团队来说，这是实打实的变化。设计文档变成了承重结构，因为它是那个会被检查的产物。

证明止步的地方

有三条限制，比功能列表更重要。

只支持 Rust。Verus 检查的是 Rust，GitHub Next 说 PDD Kit 目前只在 Rust 上工作，不引入新语言，也不改变代码是怎么产出的。如果你的 agent 写的是 TypeScript 或 Python，现在没什么可装的。考虑到大量生产代码并不是 Rust，这是一句轻描淡写的话包着一条很大的限制。

只覆盖 spec 能表达的东西。形式化证明能覆盖你可以精确陈述的性质：输入输出契约、不变式、状态机迁移。它覆盖不了 UI 行为、绝大多数 I/O 密集的逻辑，以及任何「正确」是一种判断而不是一条性质的东西。这些全都落到测试加人工评审的兜底路径上——而那正是今天负担所在的地方。

研究预览版，而且有一段很具体的历史。Chopin 在 GitHub Next 的项目页上被列为研究原型，日期是 2026 年 9 月。GitHub Next 以前也发布过原型——Repo Mind、Project Copernicus、SpecLang 都在其中——它们从未走到正式可用。第一次针对真实代码的公开演示安排在 GitHub Universe，10 月 28–29 日。

兜底路径才是诚实所在

最能说明问题的设计决策，根本不在证明器上。而是它为无法证明的代码明确留了第二条路，通向测试和 computer-use agent 的经验性检查。

这是大多数验证工具都拒绝做出的承认。它在架构里明说：有些代码可证明，有些不可证明，假装不是这样，比交付两条流水线更糟。用这套东西的团队最后会给每个模块贴一个标签——已证明、已测试、已评审——这比任何覆盖率报告都更诚实地盘点了你的信心。

问题在于，兜底路径也正是 agent 给自己批作业的地方。一个 computer-use agent 点着 UI 检查改动有没有生效，它仍然是 agent，仍然在抽样，仍然可能得出「这个坏掉的流程看着没问题」的结论。证明路径给出的是证明，兜底路径给出的是「一个跑通了的 demo」。

底下那层研究，才是让人放心的部分

PDD Kit 不是从零造的验证器。Verus 是独立的、成熟的。微软研究院的 verus-proof-synthesis 仓库放着地基：两个 LLM 驱动的系统 AutoVerus 和 VeruSAGE，负责生成和修复 Verus 证明，分别在 150 个和 849 个验证任务上做过基准测试。

PDD Kit 看起来新增的是打包。这是这条证明合成研究线第一次被折进一个从规划到 PR 的产品工作流，而不是一次基准测试练习。这个说法比「AI 能证明自己的代码」要小，但也更可信。

另外注意，信源连名字都没统一。同一周的报道里，Proof-Driven Development Kit 和 Property-Driven Development Kit 都会出现，而且都归到同一个发布上。挑一个用就行；反正做品牌的是那个缩写。

今天就能做的事

能留下来的结论不是「等 GA」。而是：一个 agent 密集的代码库现在会分成可证明和不可证明两块地盘，而你的配置应该已经知道哪块是哪块。

解析器、状态机、数据结构不变式、带边界的算术、并发原语——这些是可证明的地盘，Verus 开源、现在就能用，有没有 PDD Kit 都行。前端的大部分工作、大部分胶水代码，以及任何正确性取决于「用户到底想干什么」的东西，都不在。

由此有两个实际动作。第一，在仓库里给可证明的模块打标签，并让 agent 专门针对这些模块用 Verus，早于任何厂商交付工作流。第二，别再让 agent 顺手写那些验证自己工作的测试；这种安排一直是利益冲突，也正是「全绿」比以前更不值钱的原因。

那个让人不舒服的问题

如果 spec 可以由人批准、证明可以由机器清掉，那评审者到底是干嘛的？不是读代码，大概也不是抓 agent 在第 412 行引入的 bug。

评审者的工作变成了它本来就该是的那件事：决定这个系统该做什么，并且拒绝接受一份没把这件事说清楚的规格。这比在 diff 上点通过要难。这也是整件工作里唯一一件验证器替你做不了的事。