Use Microsoft PDD Kit to Verify Agent Rust

A coding agent can drift from the plan you gave it and then write tests that praise the drift. Microsoft Research named that gap in its November 5, 2026 post on PDD Kit. The plan is meant to be the contract. Nothing forces the agent to keep it, and reading every line the agent wrote does not scale when one task can touch thousands of lines.

PDD Kit is the fix Microsoft Research built with GitHub Next. It turns intent into a formal specification, meaning a set of precise statements a machine can check. A tool called Verus then proves that the Rust code meets that spec for every input in the model. Where a proof cannot reach, the kit falls back to tests and says so in plain sight.

What You’ll Build or Learn

You will end with a clear method for verifying one piece of agent written Rust, and with Verus installed and proven on a sample file from its own guide. The method follows the worked example Microsoft published. That example is Pet Store, a full stack web app of about 5,000 lines of Rust, with an Axum and SQLite backend and a Leptos storefront compiled to WebAssembly.

The team in that example verified login. This tutorial uses the same target because login shows every hard part at once. It has a rule you can state in one sentence, a role rule that matters for safety, database lookups the verifier cannot see, and a password check that lives in an outside crate. If you can map login, you can map a payment check, a permission check, or a parser with strict rules.

You will also learn the limit that matters most. A proof covers its spec and nothing else. Work that sits outside the spec still needs tests, review, or an honest note that nobody promised it.

Before You Begin

Read the access limit first, because it shapes the whole tutorial. PDD Kit itself lives inside Chopin and stays in research preview. There is no cargo command that installs PDD Kit, and any guide that gives you one has invented it. Steps 4 to 8 describe the workflow as Microsoft and GitHub Next document it, for teams with that access. Steps 1 to 3 and the Verus work in Step 2 are useful on their own, and they are the prep a team needs before PDD Kit access arrives.

Back up the Rust code you plan to verify, and pick a branch for the work. The workflow adds a verified crate and new contracts. It should not land on your main branch until the proof and the tests for the trusted parts both pass. Use placeholder values in every example that touches a secret, a token, or a signing key. No step in this tutorial needs a real credential.

Our coverage of sandboxed agent sessions with Google Agent Substrate shows the other half of this problem, keeping an agent contained while it works. This tutorial covers the proof half: showing that the work the agent shipped matches what you asked for.

Step 1: Pick One Small Function Where a Bug Costs Real Money or Real Trust

Action: choose the first target the way Microsoft advises. Start with the most sensitive part of the app and verify the rest one piece at a time. Login, payments, and permissions are the examples Microsoft names. A good first target has clear inputs, clear outputs, and rules you can state without taste or judgement.

Expected result: you can write the target as one function and a short list of outcomes. In Pet Store, that function became login_flow. It takes the fields of a login request and returns a token or an HTTP error. Five smaller functions sit under it: login_core, lookup_target, decide_login, and issue_token among them. Each one has its own contract, so a change to one piece only needs that piece proved again.

A poor first target is a whole screen, a search ranking, or any behaviour where correct is a matter of opinion. Park those for tests and human review. Proof needs a rule, and a rule needs words that mean the same thing to everyone who reads them.

Step 2: Install Verus and Prove the Sample From Its Own Guide

Action: install Verus from its binary release. This is the verifier PDD Kit uses today, and it works on its own with no Chopin access at all. The Verus install file gives this order: download the latest release for your platform, unzip it, move into the folder it creates, and run the binary. On macOS, run the script in that folder that clears the Gatekeeper quarantine first.

bash macos_allow_gatekeeper.sh
./verus

Expected result: Verus either runs or tells you what to install. If rustup is missing, it prints the exact command to install it and the toolchain it needs. If rustup exists but the toolchain does not, it prints the rustup install command for that toolchain. Follow the printed command, then run the binary again. Do not guess a toolchain version. The binary names the one it was built for.

Next, create the sample file from the Verus guide. Name it getting_started.rs and paste in this content, which the guide uses as its first example:

use vstd::prelude::*;

verus! {

spec fn min(x: int, y: int) -> int {
    if x <= y {
        x
    } else {
        y
    }
}

fn main() {
    assert(min(10, 20) == 10);
    assert(min(-10, -20) == -20);
    assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j);
    assert(forall|i: int, j: int| min(i, j) == i || min(i, j) == j);
    assert(forall|i: int, j: int| min(i, j) == min(j, i));
}

} // verus!

The guide explains the shape in one line worth learning now. The file is Rust. The verus! macro extends it with spec language, such as forall, and tells Verus to verify the functions inside the block. A spec fn is ghost code. The verifier checks it, and the compiler erases it from the program you ship.

./verus getting_started.rs

Expected result: Verus prints a note that it is verifying the root module, then a results line that reads 1 verified, 0 errors, in the form the guide shows. That line is your first proof. Verus checked the claims about min for all inputs, not just the two pairs in the plain asserts. If you want a binary as well, the guide gives the same command with the compile flag added. Verification alone does not compile the file.

Step 3: Write Intent in Plain Language, Both Ways Where It Matters

Action: write the request for your target in plain sentences, as rough as you like. Pet Store started with two sentences for login. You only get a token with the right password. Only admin accounts get admin tokens. PDD Kit treats rough input as normal. Turning rough intent into checkable rules is its job.

Then read each sentence for the trap Microsoft found in the first one. A rule that says a token comes only with the right password is also kept by a login that refuses everyone. The missing half is that the right password always gets a token. Microsoft calls the first reading an implication and the pair of readings an if and only if. Together they rule out both the bad login and the lazy login.

Expected result: each key rule states what must happen and what must never happen. For login, the settled form covers both halves. A token is issued if and only if the request names a real account and the password matches the stored hash for that same account. That same account wording matters. It catches a wiring bug where the code checks one account and signs a token for another, a bug a test suite rarely thinks to look for.

Step 4: Run pdd-plan in Chopin and Answer the Decision Cards

Action: with Chopin access, open the plan for your repo and give PDD Kit the target and the intent from Step 3. Its planning workflow is called pdd-plan. It reads the code first. Then it comes back with questions on decision cards before it writes anything. When a question depends on how the code works, the card explains that part first, so you can answer without opening the source.

Answer each card as a team decision, not as a quick click. In the login example, the first card asked if the right password must always get a token. The team picked the both ways reading from Step 3. A later card asked how much of login to prove. The first draft proved the decision at the centre and kept the handler trusted and tested. The developer chose more: a spec for the handler itself, so the proof covers the glue where lookups get awaited and the token gets signed.

Expected result: PDD Kit keeps a rough work section at the top of the plan, with a flow chart of the target, a map of what will be proved and what will be trusted, and an intent map. Each intent entry links back to your own words and forward to the section of the formal spec that models it and the tests that cover it. If that map does not match what you meant, stop here. The rest of the workflow will faithfully prove the wrong thing.

Step 5: Approve the Spec and the Trusted Boundary, Not the Code

Action: review the intent artifact as a whole and sign off on it before any build starts. The formal spec is the plain language intent written as Verus contracts. Each function gets an ensures block. That block states what must hold about its result for every possible input. In login, two rough sentences became eight ensures clauses on login_flow, covering a token only for the named account, the right password always getting a token unless a lookup or signing step fails with a 500, a missing account getting a 401, a wrong password getting a 401, an unreadable hash getting a 500 and no token, and the admin role only for an admins row found by username with no email sent.

Then review the boundary with the same care. The Trusted Computing Base is the code the proof assumes behaves as described. PDD Kit makes that line explicit and asks you to accept each piece on its own. For login, the developer accepted six pieces:

In code, a trusted piece sits behind a small wrapper with an assumed contract. Verus reads the contract and not the body. The spec marks that with terms such as external_body for a wrapper, or an external spec for a function whose code stays where it is. Names for things the proof cannot model, such as what the database holds right now, appear as abstract functions with no body. The proof then says that whatever the database holds, login does the right thing with it, and the trusted contract says the lookup returns what the database holds.

Also read the list of what nobody promises. For login, that list names a future that never completes, a clock that is out of range and panics, timing and rate of attempts, and how other endpoints read the role. A proof says what its result will be if the function answers. It says nothing about how fast, or whether it answers at all.

Expected result: you have approved a spec you can read, a boundary you accepted piece by piece, and a list of gaps nobody claims to cover. Two reviewer agents in the workflow also probe the spec for gaps and for promises a proof could not show, and that review runs until the spec reads as sound. Your sign off is still the act that counts. Matching your intent is not proof, so a wider scope or a new trust choice comes back for a fresh sign off.

Step 6: Let the Agent Implement, Then Run pdd-prove

Action: hand the approved plan to the prove stage. In Microsoft terms, a build plan turns the plan into a small task graph. For login that graph had seven tasks: get the file building under Verus inside the backend crate, prove the decision, the token step, and the whole flow, then write the tests for the trusted wrappers and for login as a whole.

Each task runs the same loop. A coding agent writes the code and the proof. Verus checks them against the spec. Anything in the trusted boundary gets the tests the plan called for. A reviewer agent then reads the plan, the spec, and the results side by side and looks for gaps, meaning requirements with no proof and no passing check. Gaps go back to the coding agent. A gap in the spec itself goes back to you as a decision.

Watch for the failure mode Microsoft calls vibe verification. A weak clause can verify while ruling out almost nothing. The guard is a mutation check. The prove stage plants one bug per ensures clause in a scratch copy of the code, such as refusing everyone or checking the username before the email, and Verus has to reject each altered copy on the clause it targets. A mutant that passes means that clause constrains nothing, and it comes back as a gap.

Expected result: every clause is either proved or listed as a gap with a reason. The loop is strict about moving goalposts. If a construct cannot be stated in the Verus version in use, the task stops and asks the team. It does not swap in a simpler shape or soften a contract to get a green result.

Step 7: Test the Trusted Boundary Like It Is the Product

Action: run the tests the plan wrote for each trusted piece against the real parts, not against mocks of them. Microsoft describes the plan entries as planned until they run, after which they record the command result and the commit they ran against. In login, that means tests against the real bcrypt, the real SQLite schema, and the real router.

Use the same care you would use for secrets work. Our tutorial on stopping Claude Code from leaking secrets to GitHub makes the same point from the other side: a tool result is evidence about the inputs it tried, and nothing more. PDD Kit labels a passing test the same way. Evidence, not proof.

Expected result: each assumed clause in Step 5 has at least one named test that checks it, and the plan shows that test as run and passed on a named commit. If a trusted piece has no test, treat every promise that rests on it as a claim, not a result. In login, two pieces carry most of the weight: check_password for every password promise, and the two lookups for every promise about which account a token names.

Step 8: Ship It With pdd-ship and Keep the Proof in CI

Action: let the prove stage open its pull requests, review the pull request as a receipt, and merge. In the login example, the change added a verified crate with the flow, its pieces, their proofs, and the trusted wrappers with their tests. It also routed the real login handler through that flow and kept the HTTP status codes the app already used. The verified logic hardens the production path. It is not a copy kept to one side.

Then run the ship stage. The pdd-ship workflow adds the Verus check to CI next to the tests for the trusted parts. Every later change, by a person or by an agent, must keep proving against the same spec. A broken proof fails the build in the same way a failing test does. Microsoft also notes a tidy side effect: tests that only repeat what the proof now covers can be cut, while the tests that guard the trusted boundary stay. CI gets stronger and leaner at the same time.

Expected result: the pull request description marks every requirement as formally verified or checked by tests. Your review already happened on the intent artifact. You are not asked to read the generated code line by line, and you should be able to say, for any promise in the list, which of the two kinds of evidence backs it.

Running several agents at once while this work lands is a separate skill. Our guide to running Claude Code, Codex and OpenCode with Corgi covers the workspace side of that problem.

Verification

Work through this list before you call the target verified.

First, rerun Verus on the verified crate and read the results line. It should report the functions as verified with zero errors. Second, check the mutation record from the prove stage. Every ensures clause should show a mutant that Verus rejected. A clause with no mutant record has not been tested for strength. Third, open the plan and confirm each trusted piece from Step 5 shows a test that ran and passed, with a commit named beside it. Fourth, break the proof on purpose in a scratch copy, by changing one line of logic, and confirm Verus fails on the clause that covers it. Fifth, confirm CI runs the Verus check on the branch, so a future change that breaks the proof fails before merge.

If all five hold, you can state the result in the exact form Microsoft uses for login. Proved: the named functions meet their contracts for every input. Trusted and tested: the named wrappers sit outside the proof, each behind a contract a person accepted and a test that checks it. Assumed: the Verus, Rust, and solver toolchain itself, and the Verus standard library.

Troubleshooting

Next Steps

Pick the next sensitive function and repeat the loop: a payment check, a permission gate, or a parser with strict input rules. Keep each target small. The proof habit grows one function at a time, and the trusted boundary should shrink as more code moves inside it.

Keep the intent artifact with the code. It is the record of what your team meant, which promise rests on proof, and which promise rests on a test and a name. When the next agent arrives to change that function, that record is what stops it from quietly rewriting the contract while it rewrites the code.

Facts checked November 9, 2026, against the Microsoft Research account of PDD Kit, the GitHub Next project page for PDD Kit, the Verus guide, and the Verus install file. This tutorial follows the workflow those sources document for the Pet Store login example and the sample file in the Verus guide. It does not claim the full PDD Kit workflow was run inside Chopin for this article, because PDD Kit is a research prototype and access is limited.

Sources

• The PDD Kit workflow, the Pet Store app, the two sentence login request, the decision cards, the eight clauses, the six trusted pieces, the mutation check, and the ship stage: Formally verifying agent written full stack web apps with PDD Kit, Microsoft Research
• PDD Kit as a partner inside Chopin, the intent artifact, and the Verus spec route: PDD Kit, GitHub Next
• The getting_started.rs sample, the verus! macro, ghost code, and the expected results line: Verus Tutorial and Reference
• Binary release order, platform builds, the macOS quarantine script, and the toolchain prompts: Verus INSTALL.md
• Workflow diagram and proof boundary diagram: Microsoft Research, from the PDD Kit post above. Hero and other page art: Dirty Static.