微软给 AI 写的 Rust 代码加了道证明关，开发者审意图不审代码
Agent 一口气交上来一个 PR，几万行，你滑到底要多久？
说实话，大多数人早就不逐行看了，点个 Approve，心里默念测试别骗人。
11 月 5 日，微软研究院在官方博客发了一篇长文，讲他们和 GitHub Next 合作的 PDD Kit。微软研究院的 PDD Kit 把 AI 写完代码之后的把关环节，从逐行读代码挪到了审规格加数学证明，不过它目前还是研究原型，只支持 Rust。我们 AI主线 觉得这个方向是对的，但离“拿来就用”还差一段路。
测试是 Agent 自己写的，它能替你把关吗
先说官方点出的痛点。计划本该是你和 Agent 之间的合同，可没有任何东西逼它照着做。它悄悄做出一个略有出入的版本，再写一堆测试证明“我做的没问题”，CI 越跑越绿，你要的和它交的之间那条缝，要等线上出 bug 才露出来。
PDD Kit 的解法是把测试这道关换成证明。背后的验证器是 Verus，一个给 Rust 用的证明语言，由微软研究院、卡内基梅隆大学、苏黎世联邦理工等十多家机构一起做的。打个比方，测试像抽检几件样品，证明像把图纸里所有可能的情形都推一遍。
它怎么装进日常流程？跑在 GitHub Next 的 Chopin 里，那是个让团队和 Agent 在同一份文档里实时规划的多人环境。博客自己的说法是，PDD Kit 之于形式化方法，大致相当于 GitHub 开源的 Spec Kit 之于规格驱动开发。GitHub Next 在 10 月 21 日已经先对外介绍过这个工具包，11 月 5 日这篇是带完整案例的详细版。
两句话的需求，怎么变成八条证明条款
演示项目叫 Pet Store，一个全 Rust 写的网店，后端用 Axum 加 SQLite，前端是编译成 WebAssembly 的 Leptos，合起来约 5000 行。开发者在 Chopin 里提的需求只有两句：拿对密码才发 token，只有管理员账号才拿管理员 token。
接下来这段我觉得最有意思。PDD Kit 没急着动手，先甩回来一堆问题。比如“只有对的密码才发 token”这句话，一个把所有人都拒之门外的登录也完全满足。所以得再确认反过来的那半句：对的密码必须能登进去。按官方的说法，Agent 放着不管会悄悄选一边，不会告诉你。
这两句话最后被展开成八条 ensures 条款，写进 Verus 的合同里，团队审的是配套的白话版意图文档。其中一条专防很隐蔽的接线错误：校验的是 Bob 的密码，签出去的却是 Alice 账号的 token。官方举这个例子是想说明，每一步单看都对，测试很少会想到去查，证明会直接卡住。
证明够不着的地方，它画了条线
形式验证最容易被吹过头，这点 PDD Kit 的博客倒是挺老实。登录里有六块东西被划到证明之外：数据库查询、bcrypt 验密码、读时钟、签 token 这些都在里面，别人写的库 Verus 看不见。每一块都套上一份“假定成立”的合同，开发者逐条签字认下，再配上测试。测试通过只标成“证据”，不标“证明”。
官方自己承认最薄的两处，一是密码校验的那个包装函数，二是两个数据库查询。所有关于密码、关于“token 属于哪个账号”的承诺都压在它们身上，现在靠测试撑着，没有证明。
还有个细节我挺在意：怎么防“证明了个寂寞”。模型自己写规格，容易写出一堆能通过、却几乎排除不了任何错误的条款，官方管这叫 vibe verification。他们的办法是变异检查，给每条条款单独植入一个 bug，比如让登录拒绝所有人，Verus 必须在对应条款上把它拦下来。拦不住，就说明这条条款形同虚设。这招有点像给证明本身做测试。
现在值得上手吗
先泼点冷水。Pet Store 是他们自己搭的演示项目，登录只是其中一个模块。官方说 Verus 还翻出了原有的 bug，这件事眼下只有微软自家的演示在背书。证明依然要花真功夫，规格要是写歪了，验证过的也是错代码（官方 FAQ 自己也认了这点）。
那它对谁有用？写 Rust 的人，尤其是登录、支付、权限这种出一次事就要命的地方，官方也是建议从这些地方开始，一块一块往外验。不写 Rust 的，博客说可以先移植到 Rust 再对同一份规格检查，或者让其他语言的项目通过绑定去调用验证过的 Rust，听着就不轻松。做选型的朋友，我更想让你看的是它的思路：评审的对象从代码变成了意图。
我们 AI主线 的判断是，PDD Kit 眼下是个方向标，还不是能直接塞进团队流水线的工具。接下来盯三件事：受信边界到底能缩多少，Verus 之外的验证器会不会接进来（博客提到 Lean、F*、Rocq 各有取舍，这套技术也可能用得上），以及它能不能在比 5000 行大得多的真实仓库里跑通。
Agent 越写越多，人越看越少，这个矛盾迟早得有人拿出办法，PDD Kit 至少把一个办法摆上了台面。