先了解这件事
2026年11月4日,GitHub Next介绍了与Microsoft Research共同开发的Proof-Driven Development Kit(PDD Kit)。该工具通过对话把需求整理成可机器验证的规格,再用数学证明确认AI智能体生成的代码满足规格,目前是面向Rust代码的研究原型,仅提供有限研究预览,并运行在GitHub Next开发的Web应用Chopin中。原文以Pet Store的登录处理为例,说明规格最终包含8个条件,由Verus检查证明,证明范围之外的库处理则用测试确认。后续微软研究院联合GitHub Next和RiSE团队发布的材料称,团队在Chopin环境中用PDD Kit验证了Rust全栈应用Pet Store的登录逻辑,约5000行Rust代码中开发者只审阅意图文档和规格,未逐行阅读生成代码;PDD Kit目前仅支持Rust,登录逻辑中有6处被列为受信任边界,由测试而非证明覆盖。
AI 根据公开报道生成
最新进展 · 正式报道
微软研究院用 PDD Kit 形式化验证智能体编写的全栈 Web 应用事件进展
1 个已确认进展
- 来源：Microsoft Research
报道与讨论时间线
按时间查看正式报道与传播讨论；两类内容的证据等级保持独立。
11月6日
Microsoft Research一手
微软研究院用 PDD Kit 形式化验证智能体编写的全栈 Web 应用
微软研究院联合 GitHub Next 和 RiSE 团队提出 Proof-Driven Development（PDD）范式，并发布研究原型 PDD Kit，把用户意图转成 Verus 形式化规格，再证明智能体生成的代码对每个输入都满足该规格，证明覆盖不到的部分回退到测试。团队在 GitHub Next 的 Chopin 环境中用 PDD Kit 验证了 Rust 全栈应用 Pet Store 的登录逻辑，约 5000 行 Rust 代码中，开发者只审阅意图文档和规格，未逐行阅读生成代码。PDD Kit 目前仅支持 Rust，登录逻辑中有 6 处被列为受信任边界，由测试而非证明覆盖。
11月5日
gihyo.jp
GitHub Next 介绍 PDD Kit：用数学证明验证 AI 生成代码符合规格
GitHub Next 于 2026 年 11 月 4 日介绍了与 Microsoft Research 共同开发的 Proof-Driven Development Kit（PDD Kit），它通过对话把需求整理成可机器验证的规格，再用数学证明确认 AI 智能体生成的代码满足该规格。该工具目前是面向 Rust 代码的研究原型，仅提供有限的研究预览，并运行在 GitHub Next 开发的 Web 应用 Chopin 中。原文以 Pet Store 的登录处理为例，说明规格最终包含 8 个条件，由 Verus 检查证明，证明范围之外的库处理则用测试确认。