微软研究院发布PDD Kit：用形式化证明核验编程智能体生成的代码

微软研究院11月5日介绍PDD Kit（Proof-Driven Development Kit），尝试把开发者的自然语言需求转成可审阅的规格，再用形式化验证检查编程智能体写出的代码是否满足这些规格。它与仅对代码运行测试的方式不同：对可形式化的性质，PDD Kit使用Verus生成并检查证明；无法证明的部分则通过测试，并明确标出哪些组件仍被信任。

研究团队在一个约5000行Rust的全栈示例应用Pet Store中演示了登录逻辑验证。开发者先确认需求和规格，工具再验证密码校验、账号类型与令牌签发等指定行为。微软称，Verus证明覆盖了所列核心函数的规格；数据库查询、bcrypt、时钟和令牌签名等边界仍在证明范围之外，由开发者接受其假设并配合测试。

PDD Kit目前是研究原型，当前只验证Rust代码。它的证明结论也只适用于写明并审阅过的规格及其信任假设，不能替代需求本身的审查。这个方向试图把代码审查的一部分前移到“需求是否表达准确”，再用机器检查明确约束智能体生成的实现。

来源：Microsoft Research官方博客（2026年11月5日）
https://www.microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit/