正式验证代理编写的全栈Web应用与PDD Kit

微软研究院近日发布PDD Kit工具包，试图解决AI编程代理日益凸显的“跑偏”问题。这个工具的核心思路是：让AI代理在写代码之前先产出一份形式化规格说明，然后用数学证明的方式验证生成的代码是否真正符合这份规格，证明覆盖不到的角落再用测试兜底。研究团队在GitHub Next的多人协作规划环境Chopin中做了实测，对象是一个名为Pet Store的Rust语言全栈网店应用，用PDD Kit对其登录逻辑进行形式化验证。结果显示，Verus证明器不仅证明了代码在规格层面不存在登录漏洞，还顺带挖出了代码中原本就存在的bug。整个过程中，开发者只审阅了意图和规格，没有逐行阅读AI生成的代码。 这件事的背景是，AI编程代理现在能一次性交付数万甚至数十万行的完整功能代码，传统的人工逐行审查已经完全不现实。大多数团队转向“重规划、重测试”的工作流：跟代理反复沟通需求，确认计划和测试方案后交给它实现。但问题在于，这份计划对代理并没有强制约束力——代理可能实现出略有偏差的东西，然后针对自己的实现写出一堆能通过的测试，覆盖率看起来很健康，但你要的和它交付的之间的差距，直到线上出bug才会暴露。测试只能覆盖程序行为中极小的一部分，而数学证明能回答“对所有输入是否都正确”，这正是审查所回答不了的。过去形式化证明成本极高，需要专家、专用语言，证明代码量往往是业务代码的许多倍，开发周期以年计。但微软研究院认为，随着编程代理能力提升，让代理辅助生成形式化证明和规格说明已经变得可行，他们把这种新范式称为“证明驱动开发”（Proof-Driven Development，PDD）。PDD Kit的定位类似于Spec Kit之于规格驱动开发，它作为Chopin环境内的协作伙伴运行，帮助工程师把意图转成Verus形式化规格，再证明代理代码满足规格。对于没有形式化方法背景的普通工程师来说，这意味着多了一道比测试更硬的验收关卡，尤其适合对登录、支付、权限等关键逻辑要求极高的场景。