PDD Kit: Formally Verifying What Your Coding Agent Wrote

Reading every line of an agent’s pull request stops scaling when agents ship tens or hundreds of thousands of lines at a time. Microsoft Research’s PDD Kit proposes Proof-Driven Development (PDD): review the intent, and let a verifier check the code. The blog positions it as roughly what Spec Kit is to Spec-Driven Development, but for formal methods. It runs inside GitHub Next’s Chopin planning environment. Everything below is from the blog, not from running the tool myself.

The problem it targets

A plan is meant to be the contract between you and the coding agent, but nothing forces the agent to follow it. It drifts, then writes tests that pass for what it built rather than what you asked for. CI grows, coverage looks healthy, and the gap shows up later as a bug. Tests only exercise a slice of what a program can do. A proof covers every input.

The workflow

Every result is labelled by what it rests on. Formal verification is a proof, checked by Verus, a proof language for Rust. Empirical verification is running the code (unit and end-to-end tests, browser and computer-use agents) and is labelled evidence, not proof. The boundary between them is the Trusted Computing Base (TCB): code the proof assumes behaves as described. PDD Kit makes the line explicit and asks you to approve each piece.

The login example

The case study is Pet Store, about 5,000 lines of Rust (Axum, SQLite, a Leptos WebAssembly front end). The developer asked, in two sentences, to verify backend/src/handlers/auth.rs with two requirements: you only get a token with the right password, and only admin accounts get admin tokens.

• Decision cards before code. “Only with the right password” is also satisfied by a login that refuses everyone. The first card forces the converse: the right password always works. Formally, implication plus converse gives an if-and-only-if. An agent left alone would silently pick one.
• Intent map. Each requirement is tied back to the developer’s own words, to the spec section modelling it and to the tests covering it.
• Proof scope is a choice. The first draft proved the core decision and trusted the handler. The developer chose to give the handler its own async spec (login_flow) so the glue code, where a refactor could swap two lines, is proved too. The plan was re-approved because matching intent is not approval for new trust.
• Where proof stops. bcrypt, sqlx and jsonwebtoken live in other crates; database contents and the clock are inputs; termination and timing are not specified. The external dependencies are wrapped in small functions with assumed contracts (#[verifier::external_body] or external_fn_specification), accepted individually, and each assumed clause gets a Given/When/Then test. Termination, timing and out-of-range clock panics are not promised at all; the plan lists them as outside the spec.

A trusted wrapper from the blog:

#[verifier::external_body]
pub fn expiry_from_now() -> (r: Expiry)
    ensures r.exp as int == r.now as int + 86_400,
{ ... }

Verus uses the ensures clause and never reads the body. That is the mechanism that keeps the trusted surface small and visible.

The blog reports that Verus hardened the code and uncovered existing bugs, and that the developer reviewed intent without reading the generated code line by line. One class it highlights: a bug that checks the password against one account but signs the token for another. Each step looks fine alone, but the spec clause ties the same account a across every line, so the build fails.

What I take from it

• Review moves up a level. You read a short plain-language spec and the trust list, not the diff. That only works if the spec is right, so the decision cards are the real product.
• Honest labelling is the feature. “Proved”, “trusted” and “planned” per claim beats a coverage percentage.
• Limits are real. Today the verifier is Verus, so this is Rust. The blog’s own example verifies login, not the whole app, and it advises starting with the most sensitive code and growing. A proof covers its spec and says nothing about requirements nobody wrote down.

Source: Microsoft Research blog.