Microsoft's PDD Kit Makes Agent-Written Code Prove Itself With Math, Starting With Login

The verdict first: code review is shifting from "read the code" to "read the intent"

On November 5, 2026, Microsoft Research published a toolkit called PDD Kit, short for Proof-Driven Development Kit. It attacks a problem everyone who has had an agent write code knows well: an agent can hand you tens of thousands of lines in one sitting, the features look complete, the tests look green — but whether you dare to merge no longer depends on how many lines you read. It depends on the fact that you cannot read them all. Line-by-line review has run out of road against the speed at which agents produce code.

Microsoft Research's answer is not "let the agent check its own work," and it is not "write more tests" either. Their argument is blunt: tests can only prove the code is right on the inputs you tried, and reading code can only prove the lines you actually read are right. The only way to cover "every input" is a mathematical proof — code that arrives with a machine-checkable proof that it satisfies the specification you wrote down. PDD Kit takes a craft that used to belong to safety-critical systems and formal-methods specialists and moves it into everyday full-stack web apps, without requiring you to know any formal methods at all.

The conclusion up front: this is still a research prototype, it only supports Rust today, and it is not yet something everyone can pick up and use. But the problem it points at is real, and the approach is new — it does not ask you to read the proof. It asks you to review the intent. The agent writes the code and the proof, a machine checks both, and a person reviews just one thing: what you actually wanted. That is worth a serious look for any team that ships agent-written code.

What it actually is: intent becomes a spec, the spec becomes a proof

Proof-Driven Development is the name Microsoft Research gives this new paradigm, and PDD Kit is the toolkit that implements it. It runs inside Chopin, GitHub Next's real-time, multiplayer planning environment, where a team and its agents plan in one shared document. The workflow has three stages: pdd-plan turns intent into a specification, pdd-prove proves the code meets that specification and fills in the tests, and pdd-ship puts the proof check into CI.

Here is how it works. You start by stating what you want in plain language, and PDD Kit responds like a demanding reviewer, asking questions until every ambiguity is pinned down and recorded in an "intent artifact" — a document a person can read that states clearly what was agreed. The parts of your intent that can be formalized become a Verus specification — Verus is a proof language for Rust co-developed by Microsoft Research, Carnegie Mellon University, VMware Research, ETH Zurich, and several other institutions. The parts that cannot be formalized become informal specifications covered by tests. Then the agent writes the code and the proof, Verus checks them clause by clause, and if any clause fails, the build fails, exactly as if a test had failed.

The key design decision is that "what is proved and what is not" is drawn explicitly. PDD Kit labels every verification result with what it rests on: formal verification is a mathematical proof that the code satisfies its specification for every possible input; empirical verification is evidence from running the code, which only shows it worked on the inputs it tried. The line between the two is the Trusted Computing Base (TCB) — the code the proof simply assumes behaves as described. PDD Kit puts that line on the table and asks you to sign off on each piece, instead of burying it somewhere you will never read.

The worked example: proving the login logic of a 5,000-line Rust store

To show the kit working on a real codebase, the Microsoft Research team built Pet Store, a full-stack web app written entirely in Rust, about 5,000 lines: an Axum and SQLite backend handling inventory, promotions, orders, and checkout, and a Leptos storefront compiled to WebAssembly. They chose to verify just one piece of it, the most sensitive one: the login logic. The reasoning is practical — a login bug hands an attacker a customer's account or an admin's controls, so that is where proof effort pays off first.

The developer's original request was two sentences: "You only get a token with the right password" and "Only admin accounts get admin tokens." PDD Kit's job is to start from that rough wording and drag the ambiguities into the open. The best moment is the first decision card: read literally, "you only get a token with the right password" is perfectly satisfied by a login that refuses everyone — it never gives a token to anyone with the wrong password. The real meaning has to include the other direction too: "the right password always gets a token." Formally, the first is an implication (a token implies the right password) and the second is its converse; together they make an "if and only if." An agent working alone would quietly pick one direction without telling you. PDD Kit turns it into a question and makes a person choose.

Those two sentences end up as eight ensures clauses on the login_flow function: no email and no username means a 400; a token goes only to the account the login names, only with that account's right password, and the token must carry that account's id and its table's role; the right password always gets a token unless a lookup or signing failure produces a 500; an unknown account or a wrong password gets a 401; a hash bcrypt cannot read gets a 500 and no token; the admin role can only come from an admins-table row found by username with no email sent; and a token from an email login always carries the customer role. Five pieces of core logic — login_flow, login_core, lookup_target, decide_login, and issue_token — are all proved by Verus against their own contracts, for every input.

The proof is not all-encompassing, and the blog is explicit about that. Six things sit inside the "trusted, not proved" ring: the two database lookups, the password check wrapping bcrypt, the JWT token signing, the clock read that computes an expiry exactly 24 hours ahead (86,400 seconds), the conversion of database errors, and the unpacking of the request by the handler shell. Each one carries an assumed contract the developer accepted, and each one gets tests against the real bcrypt, the real SQLite schema, and the real router. The blog states the honest limit: the guarantees are only as strong as these six trusted pieces, and two carry most of the weight — check_password for every password promise, and the two lookups for every promise about which account a token names. Tests support them, but nothing proves them.

The phrase worth remembering: "vibe verification"

My favorite idea in this post is what the authors call "vibe verification": when a model writes its own specification and its own proof, it tends to land on weak invariants — clauses that verify but rule out almost nothing. The proof passes, yet the guarantee is nearly empty. It is the same disease as vibe coding, one level up: everything looks right, and nobody was rigorous.

PDD Kit fights this on two levels. The first is procedural: the specification is derived from the intent artifact, and two reviewer agents poke holes in it, checking that the spec matches what was asked and does not promise more than a proof could show, iterating until the reviewers agree the spec is sound. The second is technical, and it is called the mutation check: pdd-prove plants one bug per ensures clause in a scratch copy of the code — refusing everyone, say, or checking the username before the email — and Verus has to reject each mutant on the clause it targets. A mutant that slips through means that clause constrains nothing, and it comes back as a gap. The loop is also strict about not moving the goalposts: if an async construct cannot be expressed in the pinned version of Verus, the task stops and asks the team, instead of quietly switching to a synchronous helper or weakening a contract.

The FAQ includes a comparison table that states the differences cleanly: in Spec-Driven Development, nothing enforces the spec; in Test-Driven Development, tests cover a sample of inputs and are often written to match what was already built; when an agent checks its own work, the checker is the same model that wrote the code; in Proof-Driven Development, Verus automatically verifies the proof that the code satisfies the spec you approved. PDD keeps the planning loop from spec-driven development and keeps the tests — but tests move back to where they belong, covering what a proof cannot reach.

Merging stops being "I finally finished reading the code" and becomes "the intent was reviewed and the proof passed." Verified changes arrive as pull requests with a receipt: every login requirement marked as either formally verified or empirically checked. Then pdd-ship adds the Verus check to CI, so every later change to login, by a person or an agent, has to keep proving against the same spec, and a broken proof fails the build like a failing test. A side benefit is that CI gets leaner: tests that merely re-check what is already proved, like example-based tests of the password gate, can be pruned, keeping only the ones that guard the trusted boundary.

Do not confuse it with October's formal-verification story: this is a different thing

VibeFix covered a related story on October 22: Anthropic and Theorem had Claude write mathematical proofs for 123 open-source libraries, down to RISC-V assembly level, totaling 180 million lines of Rocq. That story was about a scale record — how big verification can get, how many libraries, how much code. PDD Kit is not about scale. It is about daily workflow: it does not try to verify the whole world at once, but starts where a bug costs the most — login, payments, permissions — and expands one piece at a time. And it does not celebrate how large a proof is, but moves human review effort from "read every line of code" to "review the intent and sign off on the trust boundary." One is about the ceiling of verification capability; the other is about verification moving into ordinary development. They complement each other; they do not overlap.

It is equally important to be clear about what PDD Kit is not. It is not a testing tool and not a code review tool. It cannot tell you whether your requirements are right — if the specification itself is wrong, the proof only guarantees that you are wrong thoroughly. The FAQ faces this directly: a proof shows the code meets the spec, not that the spec is what you meant. That is why the toolkit spends so much effort on getting intent right first: decision cards, intent maps, reviewer agents, mutation checks — all of it exists so the spec does not get written wrong.

Staying sober: you cannot just go use it yet

The limits, in order. First, Rust only, for now. If your codebase is already Rust, there is nothing to migrate; code in other languages can be ported to Rust and checked against the same spec, or non-Rust projects can call verified Rust through bindings. But for the large majority of vibe coding projects in TypeScript or Python, PDD Kit cannot reach the main codebase today. Second, proofs still take real effort, mostly in producing the proof itself, and a clear spec is what keeps that effort down — which is why so much of the toolkit is about getting intent right first. Third, the strength of the guarantee is bounded by the trusted boundary: bcrypt, database lookups, the clock, and JWT signing — the most consequential pieces — remain "trusted plus tested," not proved. Fourth, the proof promises nothing about whether the login ever completes, how fast it is, or how it behaves under repeated attempts; rate limiting, timeouts, and whether an error message is helpful are all outside its reach.

Microsoft Research is appropriately restrained about this: it is a research prototype, and the goal is to find out how far this scales. They expect the trusted boundary to shrink significantly over time, and they recommend starting where a bug costs the most — login, payments, or permissions — and verifying the rest of a codebase one piece at a time. For most developers, the more immediately useful lesson is methodological, and it costs nothing to steal. First, write one-way statements both ways: when you catch yourself writing "only ... when ...", ask whether the reverse holds too. Second, move review effort from "what does the code look like" to "what was actually asked for," and write down explicitly which things you are merely trusting to be correct. Many production incidents do not start with code written wrong; they start with requirements that were never pinned down.

One more piece of context is worth noting: this is a collaboration between the Microsoft Research Catalyst Lab, GitHub Next, and the Research in Software Engineering (RiSE) group, running inside GitHub Next's Chopin environment. Microsoft Research is betting on two directions at once for the problem of verifying agent-written code — getting agents to write proofs themselves (PDD Kit), and getting proof checks into CI (pdd-ship). If this path works, the standard answer to reviewing agent-written code may stop being "did you read it all?" and become "did you review the spec, and did the proof pass?"

One line for vibe coders

You probably cannot use PDD Kit today — unless you write Rust. But it names a reality that will arrive sooner or later: agents now write code faster than humans can review it line by line, so review has to level up. Tests can tell you "everything we tried was right." Only a proof can tell you "the things we never tried are right too." And a proof starts with stating clearly what you actually want. The next time you ask an agent to write login, payments, or permissions, borrow the PDD Kit habit first: write the requirement both ways, list the things you are merely trusting, and pin down the fuzzy edges before the work starts. That step is free — and it is the precondition for every kind of verification.