Commit

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 Microsoft Research. PDD Kit brings assurance to AI-generated code. You describe what you want to build in plain English. PDD Kit then turns your intent into a precise formal spec, and proves the agent's code meets it for every possible input, including the ones your tests are likely to miss. Your code ships with its tests, a spec anyone can read, and a Verus proof that the code matches it. 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. 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.