Here’s the uncomfortable question behind a lot of agent-written pull requests: if nobody reads every line, what exactly are you standing behind when you merge? Microsoft Research and GitHub Next took a swing at it on November 5 with PDD Kit, short for Proof-Driven Development Kit.
The Microsoft Research post, written by Alex Lavaee and Matthai Philipose, describes it as a research prototype. GitHub Next has a longer project write-up too. It’s not a product launch you can sign up for, so read this as “here’s an approach worth understanding,” not “go install this Monday.”
The idea: review the intent, prove the code
PDD Kit runs inside Chopin, GitHub Next’s project for planning work with agents. It reads your code, asks the questions a careful reviewer would ask, and records your answers in an “intent artifact.” The parts that can be formalized become a specification in Verus, a proof language for Rust. Then the coding agent writes a proof, and Verus checks that the code meets that spec for every input the formal model covers, under its stated assumptions. What can’t be proved gets turned into informal specs that are checked with tests.
The key move is that people stop reviewing the proof and the generated code line by line. They review the spec. GitHub Next’s write-up is blunt about why: an agent’s own tests “tend to pass for the code it wrote, not the code you meant,” and a model left to write its own spec tends to land on weak invariants that verify but rule out almost nothing. They call that “vibe verification.”
The Pet Store demo, in short
The team built Pet Store, a full-stack Rust web app (Axum and SQLite backend, Leptos storefront) of about 5,000 lines, and asked PDD Kit to verify just the login logic. The request was two sentences: you only get a token with the right password, and only admin accounts get admin tokens.
The first question PDD Kit came back with is the best part of the post. Does “only with the right password” also mean “the right password always works”? Those are different specs. A login that refuses everyone satisfies the first one perfectly. The team chose both, with a catch the contract spells out: the right password gets a token unless a lookup or signing failure returns a 500. And like every clause here, it describes the result you get if login answers, not a promise that it answers.
From there, the post says PDD Kit opens pull requests with a verified crate, routes the real login handler through the proven function, and adds the Verus check to CI next to the tests. Any later change to login, by a person or an agent, has to keep proving against the same spec. It also prunes example-based tests that only re-check what’s already proved.
Where the proof stops
This is where I give the authors credit, because “fully verified” is easy to oversell and they don’t. Per the post:
- Proved: five login functions (
login_flow,login_core,lookup_target,decide_login,issue_token) meet their contracts for every input. - Trusted and tested: the two database lookups, the bcrypt password check, the clock, token signing, the database error message and request unpacking. They sit outside the proof and are covered by tests.
- Assumed: the Verus, Rust compiler and Z3 toolchain, and Verus’s standard library, vstd.
- Not promised at all: the contracts describe the results login returns. They don’t guarantee that a login ever completes or how long it takes, anything about the timing or rate of attempts, that an out-of-range clock won’t panic, or how other endpoints read the role.
They also say the guarantees are only as strong as those trusted pieces, and that two carry most of the weight. So this is a proof about one bounded piece of one app’s login, not a claim that Pet Store, or login as a whole, is correct. It only verifies Rust today, and proofs still take real effort.
What I’d take from it now
You don’t need PDD Kit to steal the habit. Before an agent touches a sensitive path like login, payments or permissions, write the requirement both ways: what must never happen, and what must always happen. Then check whether your tests cover both halves. That “refuses everyone still passes” trap is real in plenty of hand-written test suites too.
And I like where the authors put the human: not reading every line, but owning what the software is supposed to do. As agents write more of the diff, that’s the part of review worth keeping.
Hero photo: Antelope Creek Masonry Arch Bridge, arch detail by SharonPapierdreams, via Wikimedia Commons, CC BY-SA 4.0; cropped and resized.
