Microsoft Research has introduced a new toolkit that uses mathematical proof, rather than ordinary testing, to check whether code produced by an AI coding agent actually does what the developer asked for. The toolkit, called PDD Kit, was described in a Microsoft Research blog post published on 5 November 2026.

The idea behind it is a new way of working that Microsoft calls Proof-Driven Development. Coding agents can now produce whole features in a single session, sometimes running to tens of thousands of lines, and reading every line of the result no longer scales. Teams usually rely on a written plan and a set of tests instead, but an agent can drift away from the plan and then write tests that pass for the code it built, rather than for the code that was requested. PDD Kit is designed to close that gap.

The workflow starts with intent, not code. Inside Chopin, GitHub Next's shared planning environment, the developer describes what a feature should do in plain language. PDD Kit asks the questions a careful reviewer would ask, explains the relevant parts of the code as it goes, and records the agreed answers in an intent document. Requirements that can be stated precisely are then turned into a formal specification written in Verus, a proof language for the Rust programming language. Everything else becomes a test instead.

Once the developer has reviewed and approved that specification, the coding agent writes the implementation, and the Verus verifier checks it. A mathematical proof shows that the code meets its specification for every input the model covers, including the edge cases a test suite would probably never try. Where a proof cannot reach, for example in a third-party cryptography library or a user interface, PDD Kit falls back to tests and labels the result as evidence rather than proof.

Microsoft demonstrated the approach on Pet Store, a full-stack web application written entirely in Rust, with about 5,000 lines of code. The back end uses Axum and SQLite and handles inventory, promotions, orders and checkout, while the storefront is a Leptos application compiled to WebAssembly. The team focused on the login flow, starting from two plain requirements from the developer: a token is issued only with the right password, and only admin accounts receive admin tokens.

That first requirement turned out to contain a subtle trap. A rule that says a token must follow a correct password is also satisfied by a login system that refuses everybody, since it never issues an invalid token. The missing half is the reverse promise: the right password must always produce a token. PDD Kit presented that choice to the developer as a decision card before any code was written, and the developer chose the two-way version. The two sentences eventually expanded into eight formal guarantees on the asynchronous login function.

According to Microsoft, the verification process hardened the code and uncovered existing bugs, proving the absence of login bugs with respect to the agreed specification. The developer reviewed the intent and never read the generated code line by line.

The toolkit also guards against weak specifications. A proof is only as good as the specification it checks, so the prove step deliberately mutates the implementation, for example by making login reject every attempt, and checks that Verus rejects each mutated version. A mutation that survives signals a specification too weak to catch the fault. Microsoft calls this failure mode vibe verification: the proof is mechanically valid, but the specification does not capture what the developer actually wanted. Two reviewer agents also inspect the specification for omissions before the developer approves it.

There are clear limits. PDD Kit is a research prototype, not a commercial product, and it works only with Rust, because its verifier is built for that language. Parts of the system sit outside the proof altogether, including password hashing with bcrypt, database queries and token signing, which are handled by trusted wrappers and tests. The developer must sign off on each of those trusted pieces, and a final step adds the verification to continuous integration, so a change that breaks a proof fails the build.

Even with those limits, the approach points to a different kind of pull request: one where each requirement arrives with a proof, a test, or an explicitly stated assumption, rather than a pile of tests that may only confirm what the agent happened to build.