Microsoft Research 推出 Proof-Driven Development Kit 验证 AI 生成代码
Microsoft Research 出了个工具，能把你的代码意图转成数学证明，自动检查 AI 写的代码有没有偏离规范，写代码的可以试试。
Microsoft Research 推出 Proof-Driven Development Kit，用于解决 AI 生成代码的信任问题。该工具把开发者的自然语言意图转换成 Verus 规范，并应用原本用于安全关键系统的形式化方法。PDD Kit 通过数学证明来检验智能体生成的代码是否符合规范，无法验证的部分会明确标示出来。
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: msft.it/6019af2V7 Your browser does not support the video tag. 🔗 View on Twitter 💬 2 🔄 1 ❤️ 7 👀 1444 📊 4 ⚡
