Microsoft Research's PDD Kit proves agent-written code against formal specs

Microsoft Research has published a post introducing PDD Kit, a toolkit for what it calls Proof-Driven Development (PDD). The problem it targets: coding agents now ship whole features in one sitting, often spanning tens of thousands or hundreds of thousands of lines of code, so reading every line of a pull request does not scale. Most teams instead invest in a plan and tests, but the authors say nothing forces the agent to follow the plan. It can drift, implement something slightly different, and write tests that pass for its own implementation rather than for what the developer asked. CI grows with many low-quality tests, coverage looks healthy, and the gap stays hidden until a bug report or an edge case exposes it.

The authors' answer is proof. A review asks whether code looks right; a proof answers whether it is right, for every input, including ones a test suite can miss. Proofs used to be too expensive for everyday software, needing specialists, unfamiliar languages and proofs many times larger than the code. The authors say two things have changed: coding agents can now help generate formal proofs from well-defined specs, and they can better help write the specs too.

PDD Kit is described as being to formal methods roughly what Spec Kit is to Spec-Driven Development. It runs inside Chopin, GitHub Next's real-time, multiplayer planning environment. Team members first review intent in plain language. PDD Kit asks the questions a careful reviewer would ask, explains the relevant code, and records the answers in an intent artifact. Parts of the intent that can be formalised become formal specifications in Verus, the proof language for Rust. The rest, which must be taken on trust, become informal specifications checked by tests. PDD Kit then generates proofs that the code satisfies the formal specs, plus tests for the informal ones. The authors say no formal methods background is needed. Every result is labelled by what it rests on: formal verification (a proof checked by Verus) or empirical verification (unit and end-to-end tests, terminal automation, browser agents and computer-use agents), which is labelled evidence rather than proof because a passing test only shows the code worked on the inputs tried. The boundary between the two is the Trusted Computing Base (TCB), the code the proof assumes behaves as described, and PDD Kit asks the developer to sign off on each piece.

The demonstration is Pet Store, a full-stack web app written entirely in Rust: an Axum and SQLite backend handling inventory, promotions, orders and checkout, and a Leptos storefront compiled to WebAssembly, together about 5,000 lines of Rust. For brevity the post verifies only the login logic, in backend/src/handlers/auth.rs, though the authors say the same process can cover the whole app and recommend starting with the most sensitive parts. The developer's whole request in Chopin was two sentences with two requirements: you only get a token with the right password, and only admin accounts get admin tokens.

Step 1: before writing anything, the planning workflow pdd-plan reads the code and returns questions in a Decisions tab. One shows why they matter. 'Only get a token with the right password' rules out a wrong password getting a token, but a login that refuses everyone satisfies it. The converse, that the right password always works, closes that hole; together they make an if-and-only-if. An agent left alone would pick one silently; here the developer chose both.

Step 2: PDD Kit keeps a readable work section at the top of the plan, with a flowchart of the login, a spec landscape of what will be proved versus trusted, and a mental model where it helps (for login, a ticket desk). An intent map ties each requirement to the developer's own words, to the matching section of the formal spec, and to the tests covering it.

Step 3: PDD Kit's first draft proved the central decision of login (choosing the table and gating on the password) and left the handler around it trusted and tested. That was its recommended default, but the developer wanted more. Because the handler is where lookups are awaited and the token is signed, and a refactor could quietly swap two lines there, the developer chose at intent review to give the handler its own async spec. A new async function, login_flow, carries the contract from the request's fields to the token or the HTTP error. PDD Kit brought the revised plan back for a fresh sign-off, since it does not treat matching intent as approval of new trust or a wider scope.

Step 4: the post lists what a proof cannot cover. Code the verifier cannot see (bcrypt hashing, sqlx queries and jsonwebtoken signing live in other crates); facts about the outside world, such as what SQLite holds or what the clock says; whether and how fast something finishes, so a hung or slow query breaks nothing in the spec; anything a person has to judge, such as whether an error message helps; and whatever nobody wrote down. Those parts are wrapped in small functions with assumed contracts, using Verus's external_body or external_fn_specification, each accepted separately by the developer, with a test written for every assumed clause. For login the developer signed off on six pieces: the two lookups (Customer::find_by_email and Admin::find_by_username), check_password (a thin wrapper around bcrypt::verify), generate_token, expiry_from_now (reads the clock and writes an expiry exactly 24 hours later), database_error (turns a failed lookup into a 500 carrying sqlx's message), and the login handler shell.

The post's summary of the outcome: Verus hardened the code and uncovered existing bugs, proving the absence of login bugs with respect to the specification, while the developer reviewed the intent and never read the generated code line by line.

Key facts

• PDD Kit is Microsoft Research's toolkit for Proof-Driven Development: it turns a developer's intent into a formal spec in Verus, proves the agent's Rust code against it, and falls back to tests where proofs cannot reach.
• It runs inside GitHub Next's Chopin planning environment, and the authors say no formal methods background is needed.
• The demo is Pet Store, a roughly 5,000-line Rust web app (Axum, SQLite, Leptos); only the login logic was verified, from a two-sentence request with two requirements.
• The developer chose to give the login handler its own async spec (login_flow), going beyond PDD Kit's recommended default, and signed off on six trusted pieces.
• Per the authors, Verus hardened the code, uncovered existing bugs and proved the absence of login bugs with respect to the spec; a proof covers only what the spec says.

Why it matters

Agents now produce changes of tens of thousands or hundreds of thousands of lines, and the authors argue line-by-line review cannot keep pace. Agent-written tests tend to check what the agent built rather than what was asked, so a healthy-looking coverage number can hide drift from the plan. PDD Kit's pitch is to move human attention from reading code to reviewing intent, and to let a verifier check the code against that intent for every input. The authors also frame it as taking formal methods beyond specialist work to everyday applications such as a full-stack web app.

Who it affects

Engineers who direct coding agents and cannot read every generated line, especially on security-sensitive code such as login, where a bug can hand an attacker a customer's account or an admin's controls. The post says it is aimed at engineers without a formal methods background. It currently targets Rust through Verus and runs as a partner inside GitHub Next's Chopin, so teams outside that stack are not the demonstrated audience.

How to use it

The workflow in the post: describe what you want in Chopin, answer the questions PDD Kit raises in its Decisions tab, review the intent map linking each requirement to a formal spec section and to tests, then sign off on the plan and on each trusted piece. PDD Kit generates the proofs and the tests. The authors recommend starting with the most sensitive parts of an application and verifying incrementally. The visible text gives no release, availability or licensing information for PDD Kit.

How solid is it

This is a vendor's own demonstration on one small app, and only on its login logic. The claim that Verus uncovered existing bugs and proved the absence of login bugs is stated by the authors; the text available to us does not state the number or nature of those bugs, and gives no proof size, verification time or effort figures. The article text we had ends partway through the list of trusted pieces, so the closing results and conclusions are not covered here. No comparison with other tools is given. Verus itself is an established proof language for Rust, co-developed by Microsoft Research and several universities.

Risks and caveats

A proof covers its spec and says nothing about requirements outside it, so a missed or wrongly stated requirement stays unproved. Proofs also assume the trusted pieces behave as described: bcrypt, sqlx and jsonwebtoken sit outside the verifier, and database contents and the clock are inputs. Termination and speed are out of scope, so a hung or slow query breaks nothing in the spec. Anything needing human judgement, such as whether an error message helps, is left to tests, which the authors label evidence rather than proof. The developer still has to decide the intent and sign off on each assumption; in the demo the spec itself needed careful choices, such as requiring both that the right password gets a token and that a wrong one does not.

“You only get a token with the right password.”

— First of the two requirements in the developer's Chopin request, from the Microsoft Research post