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 博客中详细拆解了这一方法。

正文 · 原文

How do you solve the trust problem with AI-generated code?

AI agents can generate code at a scale too great for humans to review line-by-line. That makes it difficult to ensure the code will do what the developer intended, and it leaves the final output vulnerable to bugs and security risks.

Proof-Driven Development Kit turns plain-language developer intent into a specification in Verus, applying formal methods traditionally used for safety-critical systems. PDD Kit uses mathematical proofs to test agent-generated code against the spec where possible, and clearly indicates where the proofs can’t reach. The result is more reliable agentic code.

Researchers @MatthaiP39719 and @alexlavaee break down Proof-Driven Development in the MSR blog: https://msft.it/6019af2V7

来源：Microsoft Research · x.com