微软发布 PDD Kit：用形式化验证约束 AI 智能体编写的全栈应用

核心事实

微软研究院于 2026 年 11 月 5 日发布博客，介绍工具包 PDD Kit。据该文描述，PDD Kit 运行在 GitHub Next 的实时协作规划环境 Chopin 中，先把开发者用自然语言表达的意图整理成形式化规范，再证明智能体生成的代码对任意输入都满足该规范；对于证明覆盖不到的部分，则改用测试。团队在一个完全用 Rust 编写的全栈应用 Pet Store 上做了演示，重点验证登录逻辑，并称在规范范围内证明了不存在登录缺陷。开发者只审阅了意图，没有逐行阅读生成的代码。

背景与影响

文章指出，智能体一次可产出数万乃至数十万行代码，逐行人工审查难以扩展；而智能体自行编写的测试往往只验证它实际写出的实现，而非开发者原本的要求，导致需求与交付之间的偏差被掩盖。PDD Kit 把可形式化的意图交给 Verus（一种面向 Rust 的证明语言，由微软研究院与多所高校及研究机构共同开发）生成证明，其余部分转为非形式化规范并生成测试，结果会标注属于形式化验证还是经验性验证，并要求用户对信任计算基础逐项确认。文章称使用者无需具备形式化方法背景。

限制与来源

上述演示仅覆盖 Pet Store 的登录逻辑，文章未披露性能数据、适用范围或发布时间表。文中提到该流程可用于验证整个应用的功能正确性，但属规划性表述，尚未获独立验证。工具可用性、支持语言与地区以官网当前信息为准。来源：微软研究院博客。