微软研究院推出 PDD Kit，用形式化验证校验 AI 生成代码

AI 导读

微软研究院推出 Proof-Driven Development（PDD）Kit，将开发者意图转成形式化规格，再用形式化验证证明生成的代码符合规格，以应对 AI 智能体写代码增多后的正确性问题。

正文 · AI 翻译

Microsoft Research· @MSFTResearch · X·2026-10-22 03:19· 46 分钟前AI 评分47

AI 导读

微软研究院的 Proof-Driven Development（PDD）Kit 将开发者意图转成形式化规格，再用形式化验证证明生成的代码符合规格，以应对 AI 智能体写代码增多后的正确性问题。

正文 · 原文

AI 智能体正在编写越来越多的代码。开发者如何确保这些代码是正确的？

微软研究院的 Proof-Driven Development（PDD）Kit 探索了一种更严谨的方法：它将开发者的意图转化为形式化规格，然后使用形式化验证来证明生成的代码符合该规格。

PDD Kit 可与 Rust 的 Verus 配合使用，并与 @GitHubNext 的 Chopin 集成，将形式化方法引入面向团队的 AI 辅助开发工作流。

欢迎在 2026 年 10 月 28–29 日的 @github Universe 上观看该工作的实际演示。

来源：RadarAI · aihot.news