Microsoft PDD Kit: Proving Agent-Written Code with Verus Instead of Reading Every Line

Microsoft Research says it has a way to trust agent-written code without reading all of it. On November 5, 2026, it published PDD Kit, a research prototype that converts developer intent into a formal specification, has a coding agent prove the code meets it for every input, and falls back to tests where a proof cannot reach (Microsoft Research). The demo verifies the login logic of a small Rust web app. The developer "never read the generated code line-by-line."

Context matters. Agents now ship features of tens or hundreds of thousands of lines, and line-by-line review does not scale. We covered the same pressure in our posts on the AI verification tax and Anthropic's formal verification work. PDD Kit is Microsoft's answer: review the intent, let a proof hold the code to it.

TL;DR: the questions people ask first

The problem: the plan is a contract nothing enforces

Microsoft frames the gap simply. Teams invest in a plan, hand it to an agent, and the agent can drift. It builds something slightly different, then writes tests that pass for what it built rather than what you asked for. CI grows, coverage looks healthy, and the gap stays hidden until a bug report.

Tests only exercise a tiny slice of what a program can do. Agent code tends to fail in two ways a careful reviewer would catch: it omits something obviously necessary, or it does something obviously wrong. Microsoft's claim is that a proof closes that gap. "Review asks 'does this look right?' A proof answers 'is this right?'"

Proofs used to be too costly for everyday software. Microsoft says two things changed: agents can now help produce proofs from well-defined specs, and they can help write the specs. It calls the result Proof-Driven Development, and describes PDD Kit as to formal methods roughly what Spec Kit is to Spec-Driven Development.

How PDD Kit works

The workflow has two halves. First, the team reviews 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 intent that can be formalized become Verus specifications. The rest, which must be taken on trust, become informal specs for tests. Then the agent generates proofs for the formal part and tests for the informal part.

Two kinds of verification, always labeled:

• Formal verification: a mathematical proof, checked by Verus, that code meets its spec for every possible input. Verus is a proof language for Rust, and its open-source repo describes statically checking that Rust code satisfies specifications for all executions.
• Empirical verification: running the code, using unit and end-to-end tests, terminal automation, browser agents and computer-use agents. A passing test is labeled evidence, not proof.

The line between them is the Trusted Computing Base: code the proof assumes behaves as described. PDD Kit makes that line explicit and asks a human to sign off on each piece.

The demo: Pet Store login

Microsoft built Pet Store, a full-stack app written entirely in Rust: an Axum and SQLite backend for inventory, promotions, orders and checkout, and a Leptos storefront compiled to WebAssembly, around 5,000 lines in all. It focused on login because a login bug can hand an attacker a customer's account or an admin's controls.

The developer's whole request was two sentences: you only get a token with the right password, and only admin accounts get admin tokens.

Questions before code

The planner came back with a question that looks pedantic. "Only with the right password" is also satisfied by a login that refuses everyone. The other half, "the right password always works," rules that out. Formally that is the difference between an implication and an if-and-only-if. An unsupervised agent would pick one silently. Here the developer chose both directions.

What got proved

The developer asked for more than the default: a spec on the async login handler itself, so the glue where lookups are awaited and the token is signed is proved too. The result is a function, login_flow, with eight ensures clauses derived from the two-sentence request. Four of them keep today's refusals, so the storefront and existing API tests keep working. Examples:

• A token comes back only for the account the login names, with its right password, carrying that account's id and its table's role.
• The right password for the named account always gets a token, unless a lookup or signing failure produces a 500.
• A login naming no existing account gets a 401, unless the lookup fails.
• The admin role is issued only for an admins row found by username with no email sent.

Microsoft gives a bug this catches that tests rarely do: a login that checks the password against one account but signs a token for another. Because the same account appears on every line of the clause, that bug fails the build.

What was trusted

Proofs stop at the edge of code the verifier cannot see. For login, the developer signed off on six pieces: the two database lookups, the check_password wrapper over bcrypt, token generation, the clock-based expiry, the database error mapping, and the handler shell. Each sits behind an assumed contract, and each gets tests. Microsoft states what nobody promises: that the login future ever completes, that an out-of-range clock will not panic, anything about timing or rate of attempts, and how other endpoints read the role.

Microsoft is blunt about the weak links: the guarantees are only as strong as the six trusted pieces, and check_password and the two lookups carry most of the weight.

Guarding against "vibe verification"

A model that writes its own spec tends to land on weak clauses that verify but rule out almost nothing. Microsoft calls this vibe verification. PDD Kit counters it three ways, per the post:

1. It asks clarifying questions and flags ambiguity instead of guessing.
2. Two reviewer agents poke holes in the derived spec from the intent artifact.
3. A mutation check plants one bug per ensures clause in a scratch copy, such as refusing everyone, and Verus has to reject each mutant on the clause it targets. A mutant that survives means the clause constrains nothing.

The loop is also strict about goalposts. If a construct cannot be expressed in the pinned Verus version, the task stops and asks the team rather than weakening a contract.

From proof to pull request

After the developer signs off on the spec, machines do the rest. The approved plan becomes a task graph. For login that was seven tasks: build the spec under Verus, prove the decision, the token and the whole flow, then write tests for the trusted wrappers and the end-to-end login. An LLM verifier then looks for gaps between requirements, proofs and passing checks.

The pull request adds a verified crate and routes the real login handler through login_flow, keeping existing HTTP status codes. Its description marks each requirement as formally verified or empirically checked. A later pdd-ship step adds the Verus check to CI, so a broken proof fails the build like a failing test. Microsoft says it also prunes example-based tests that only re-check what is already proved, and keeps tests that guard the trusted boundary.

Limits Microsoft states

• Research prototype. It verifies Rust only today. Other languages can be ported or call verified Rust through bindings.
• A wrong spec is still possible. A proof shows code meets the spec, not that the spec captures what you meant.
• Proofs take effort. Microsoft says effort goes mostly into producing the proof, and a clear spec keeps it down.
• Scope. Only login was verified in the demo, although Microsoft says the same process can cover the whole app. It recommends starting with the most sensitive code, such as login, payments or permissions.
• No benchmark. The post is a single case study. It gives no data on cost, time or failure rates across projects.

What this means for what you build

If you use coding agents on Rust, this is a concrete pattern to watch: write the requirement as an intent, then make the agent prove it, then review the intent. If you do not use Rust, the transferable idea is the labeling. Mark every requirement as proved, tested or trusted, and make someone sign off on what is trusted. That works even with plain tests.

For related approaches, see our coverage of Claude and formal verification with Lean and TLA, the Theorem OSS free formal verification program, and the broader trust and intent problem in vibe coding. For the spec-first side, see DESIGN.md as an open spec for AI design systems.

How to try the idea today

You cannot assume PDD Kit access. Microsoft describes it as a prototype running inside Chopin and gives no release date. You can still apply the method:

Before writing code, list each requirement as an if-and-only-if where it makes sense.
Mark each as: provable, testable, or trusted.
For trusted items, name the exact function, the assumed contract, and one test that checks it.

Then ask the agent to write the tests for the trusted items first, and review those before the implementation.

Related reading

• The AI verification tax and how to cut it
• Anthropic's formal verification of 123 libraries
• Claude, Lean and TLA formal verification SDK
• Theorem OSS free formal verification
• How do we stop vibe coding?

Details are accurate as of November 5, 2026. PDD Kit is a research prototype and may change.