微软研究院介绍 PDD Kit：用形式验证核查 AI 编码代理生成的全栈 Web 应用代码

01发布与试用场景

微软研究院发布博客介绍 PDD Kit。它把用户意图转成形式规范，再证明编码代理生成的代码对每个输入都满足该规范；证明覆盖不到的部分，用测试补充。该工具面向没有形式方法背景的工程师，并已在一个全栈 Web 应用上试用。¹²

试用对象是 Pet Store，一个用 Rust 编写的店面应用。研究团队在 GitHub Next 的 Chopin 环境中用 PDD Kit 形式验证它的登录逻辑；此次展示的范围并非整个应用。²

02工作流：先定意图，再证明或测试

据博客描述，PDD Kit 会像细心的审查者那样追问意图：把能形式化的部分转成形式规范，把必须依赖信任的部分转成非正式规范，交给测试。这里的“形式验证”指用数学证明代码对所有可能输入都满足规范，检查由 Verus 完成；Verus 是面向 Rust 的证明语言。测试则通过运行代码观察行为，覆盖第三方密码库、用户界面等证明难以到达的部分。¹⁵

PDD Kit 会标明每项结果基于形式验证还是经验验证，并列出证明所依赖、需假定行为正确的代码边界（TCB），要求用户逐项确认。博客强调，测试通过只说明代码在试过的输入上工作，因此被标为证据，而不是证明。¹⁵

03登录逻辑的验证结果

博客称，Verus 在 Pet Store 的登录逻辑上强化了代码，并发现已有缺陷，证明相对于所写规范不存在登录缺陷。开发者审阅的是意图，没有逐行阅读生成的代码。这个案例的证明只针对登录逻辑；博客称同一流程可用于验证整个应用的功能正确性，但此次展示的验证范围并不是整个应用。²³⁴