Microsoft Research introduces PDD Kit to verify agent-written web apps

A contract between developers and coding agents

Microsoft Research says coding agents can now produce complete features spanning tens of thousands or hundreds of thousands of lines of code, making exhaustive line-by-line review difficult to scale. Developers often rely on a natural-language plan and tests, but an agent can drift from the plan and write tests that validate its own implementation rather than the behavior the developer requested.

PDD Kit is intended to address that gap through what Microsoft Research calls Proof-Driven Development, or PDD. The toolkit works with developers to clarify their intent, turn the parts that can be formalized into specifications in Verus, and generate proofs that the code satisfies those specifications. Requirements that cannot be formalized are converted into informal specifications and covered with tests.

“Review asks ‘does this look right?’ A proof answers ‘is this right?’” Microsoft Research writes in its announcement. Unlike a test, which checks behavior on the inputs it tries, a mathematical proof can establish that code meets its specification for every input covered by the specification.

How PDD Kit combines proofs and tests

PDD Kit runs as a partner inside Chopin, GitHub Next’s real-time, multiplayer planning environment. Its workflow begins with team members reviewing intent in plain language. The toolkit asks questions a careful reviewer might ask, explains relevant code, and records the answers in an intent artifact that connects the user’s request to formal specifications and tests.

For formal verification, PDD Kit currently uses Verus, a proof language for Rust co-developed by Microsoft Research and academic and research institutions. Empirical verification covers areas that proofs cannot reach, such as a third-party cryptography library or a user interface. It can use unit and end-to-end tests, terminal automation, browser agents, and computer-use agents.

Microsoft Research distinguishes evidence from proof in the toolkit. A passing test shows that code worked for the inputs tested, while formal verification is a mathematical proof checked by a verifier. PDD Kit also makes the Trusted Computing Base explicit. This is the code that a proof assumes behaves as described, and users are asked to sign off on each part.

Pet Store demonstration focuses on login security

Microsoft Research tested PDD Kit on Pet Store, a full-stack storefront written entirely in Rust. The application uses Axum and SQLite on the backend to handle inventory, promotions, orders, and checkout. Its storefront is a Leptos application compiled to WebAssembly, and the complete app contains about 5,000 lines of Rust.

The demonstration focused on formally verifying the login logic in backend/src/handlers/auth.rs. The developer supplied two requirements: a user should receive a token only with the right password, and only admin accounts should receive admin tokens. PDD Kit first asked questions about the request before changing code, including whether the password requirement should work in both directions. That distinction rules out both an incorrect password receiving a token and a login that refuses every user.

According to Microsoft Research, Verus hardened the login code and uncovered existing bugs, proving the absence of login bugs with respect to the specification. The developer reviewed the intent without reading the generated code line by line. The research team recommends beginning with an application’s most sensitive areas, such as login, where a bug could expose a customer account or administrative controls, and then verifying the application incrementally.