微软研究院推出 PDD Kit，形式化验证智能体生成的应用

2026 年 11 月 6 日，Microsoft Research 发布 PDD Kit，用于对 AI 智能体生成的全栈 Web 应用做形式化验证。据 Microsoft Research 介绍，由于 AI 智能体能生成大量代码，人工逐行审查已经难以应对；PDD Kit 的做法是先把开发者意图转写成 Verus 形式化规约，再证明生成代码对任意输入都满足该规约。

对于无法实际证明的部分，PDD Kit 改用测试覆盖。Microsoft Research 称，这样一来开发者只需审查意图，而不必逐行阅读代码。

目前材料中只有这一篇 Microsoft Research 发布的报道，没有其他信源补充后续进展，该工具的后续动态和实际使用情况尚无法核实。