From the source
Microsoft Research has released PDD Kit, a toolkit that helps turn a coder's intent into a formal spec and then proves the code an agent writes matches it for every input.
- The problem it answers is scale: agents now ship whole features spanning tens of thousands of lines, so reading every line of a pull request no longer works for most teams.
- Plan and tests are meant to hold the agent to that contract,
Microsoft says, but nothing constrains the agent to follow the plan, and the tests it writes usually check what it built rather than what was asked for.
- PDD Kit runs inside
GitHub Next's Chopin, asks the questions a careful reviewer would ask, and records the answers in an intent artifact bridging intent with the specification or tests.
- The parts of intent that can be formalized become formal specs and the rest become informal specs for tests, with proofs generated automatically by Verus, a Rust proof language co-developed by Microsoft Research and several universities.
- Microsoft says its own trial formally verified the login logic of Pet Store, a Rust storefront, and that Verus uncovered existing bugs; the developer reviewed the intent and never read the generated code line-by-line.
