微软研究院11月5日介绍了PDD Kit：它与开发者一起把开发意图转成Verus形式化规格，再证明AI编程智能体生成的代码对所有输入都符合该规格；证明无法覆盖的部分则使用测试。
这项工具针对的是“计划与实现不一致”的问题。微软研究院指出，智能体可能实现了与要求略有不同的功能，再编写能通过自身实现的测试。当生成代码越来越多时，逐行人工审查难以扩展，测试通过也不等于代码实现了开发者原本的意图。
文章展示的案例是在GitHub Next的Chopin中，使用PDD Kit对Rust网店Pet Store的登录逻辑进行形式化验证。微软研究院称，Verus帮助加固了代码，并发现已有缺陷；开发者审查的是开发意图，没有逐行阅读生成的代码。
这里的证明范围需要说清：案例证明的是登录逻辑相对于所写规格不存在登录缺陷，不是宣布整个全栈应用没有任何错误。PDD Kit的做法也不是以证明完全替代测试，而是将规格约束、形式化证明与测试结合，用于核验智能体实现是否符合要求。
原始来源：Formally verifying agent-written full-stack web apps with PDD Kit