微软研究院发布 PDD Kit：用形式化证明验证 AI 生成代码

Alex Lavaee @alexlavaee原推发布于 2026.10.22

在 X 上打开原推

I've never trusted code I didn't review until now. Agents write more code than any of us can review. We often end up skimming the PR/diff and pushing. Current review methods do not prove the code is correct or does what we asked. Recent research found the best AI code reviewer caught the bug on its first try only 42% of the time.* The evaluation bottleneck, regressions, and security incidents have forced us to find a better way. Introducing Proof-Driven Development Kit (PDD Kit) from @MSFTResearch. PDD Kit brings assurance to AI-generated code. You describe what you want to build in plain English. PDD Kit captures your objective, what we call your intent, and uses a verifier tool to prove the code meets it for every possible input. You never review a single line of the code or the proof. You review your plan and the defined objectives in natural language. A simple example is login. With testing, you check that only the correct password logs in a user but with a proof on top you can verify that there is no case a wrong password allows login. You can prove correctness and security across many complex scenarios. Not only does PDD Kit prove the correctness of your code, but also your intent so you can have confidence your code is correct and does what you asked. It provides a level of assurance that specs, code review, and tests never could. PDD Kit is in limited research preview. Video explainer below. If you want to learn more, I'll be sharing PDD Kit at GitHub Universe next week, Oct 28–29. Swing by the Speakeasy, ask for GitHub Next, and ask me about verified code. If you're in SF, let me know. *Yang et al., "(When) Should a Software Factory be Lights-off?", Microsoft Research and CMU, Oct 2026

这条是引用着另一条写的：x.com/githubnext/status/2112936525457740139