Microsoft Research 推出 Proof-Driven Development Kit，用形式化证明校验 AI 生成代码

Microsoft Research· @MSFTResearch · X·2026-11-06 02:36· 33 分钟前AI 评分55

AI 导读

Microsoft Research 介绍 Proof-Driven Development Kit，用于解决 AI 智能体生成代码难以逐行审查的信任问题。该工具把开发者的自然语言意图转成 Verus 规范，沿用安全关键系统中的形式化方法，用数学证明尽可能验证智能体生成的代码是否符合规范，并明确标出证明无法覆盖的部分。研究人员在 MSR 博客中详细拆解了这一方法。

正文 · 原文

如何解决 AI 生成代码的信任问题？

AI 智能体生成代码的规模远超人类逐行审查的能力。这使得难以确保代码符合开发者的意图，也让最终输出容易受到缺陷和安全风险的影响。

Proof-Driven Development Kit 将开发者的自然语言意图转换为 Verus 规范，沿用传统上用于安全关键系统的形式化方法。PDD Kit 在可能的情况下使用数学证明来检验智能体生成的代码是否符合规范，并清楚标明证明无法覆盖的部分。由此得到更可靠的智能体代码。

研究人员 @MatthaiP39719 和 @alexlavaee 在 MSR 博客中详细拆解了 Proof-Driven Development：https://msft.it/6019af2V7

来源：Microsoft Research · x.com