Microsoft Research shows PDD Kit, a prototype for proving AI-written Rust meets its spec

Microsoft Research published a blog post on Thursday 5 November 2026 describing PDD Kit, a toolkit its authors say works with a developer to turn their intent into a formal specification and "proves the agent’s code meets that spec for every input, and falls back to tests where a proof can’t reach." The post, by Alex Lavaee and Matthai Philipose, describes the kit as "a research prototype".

What the kit does

The authors call the approach Proof-Driven Development (PDD) and compare PDD Kit's role to GitHub's Spec Kit for spec-driven development. They argue that an agent's tests "usually check what it built, rather than what you asked for", and that exhaustive line-by-line human review "can become difficult to scale" as agents generate more code.

• Intent first. A planning workflow, pdd-plan, reads the code and asks questions before writing anything. The answers go into an "intent artifact" in plain language. The parts that can be formalised become specifications in Verus, a proof language for Rust co-developed by Microsoft Research, Carnegie Mellon University and others; the rest become informal specifications for tests.
• Proof, then tests. A second workflow, pdd-prove, has a coding agent write the implementation and the proof, which Verus checks. Code the proof cannot see is covered by tests, and the kit labels a passing test as "evidence rather than proof".
• Explicit trust. The boundary between proved and trusted code (the trusted computing base) is made explicit, and the developer is asked to sign off on each trusted piece.
• Checks on the spec. Two reviewer agents check the derived spec, an LLM verifier looks for requirements with no proof and no passing check, and a mutation check plants one bug per specification clause to catch clauses that "verify but rule out almost nothing", which the authors call "vibe verification".
• CI. A pdd-ship workflow adds the Verus check to continuous integration. The authors write that "The check is deterministic, with no model involved", and that it takes "usually seconds for a small module, up to minutes for a larger codebase."

The post does not name which coding agent or model wrote the code and proofs.

The login demo

The team built Pet Store, a storefront written in Rust (Axum and SQLite on the back end, a Leptos front end compiled to WebAssembly), which the post puts at about 5,000 lines. Working inside GitHub Next's Chopin planning environment, the post covers the verification of the login logic only. The developer's request was two sentences: "You only get a token with the right password." and "Only admin accounts get admin tokens."

PDD Kit's first question was whether the right password must always get a token, because a login that refuses everyone would satisfy the first sentence on its own. The developer chose to prove both directions. The request ended up as eight clauses on a new login_flow function, and the developer also chose to bring the handler's glue code into the proof rather than trust it. Six pieces stayed trusted and tested, including the two database lookups, a wrapper around bcrypt, the clock and token signing.

The authors say Verus "hardened the code and uncovered existing bugs", without listing the bugs, and that the developer "never read the generated code line-by-line."

What you can use today

• PDD Kit itself: the post links no code repository, download or paper for the kit. Searching GitHub on 7 November, we found no PDD Kit repository under the Microsoft or GitHub Next organisations.
• Chopin: the post says PDD Kit runs as a partner inside Chopin. Chopin's code is public at githubnext/chopin under the MIT licence (per the GitHub API), but we found no PDD Kit or Verus files among its 3,127 paths. GitHub Next's own Chopin page, dated September 2026, says: "We don’t recommend you attempt to use it today. But within a month or so, we will have ironed out enough creases to seriously entertain some alpha users." The page still carried that wording when we checked it on 7 November.
• Verus: the verifier is public at verus-lang/verus under the MIT licence (per the GitHub API).
• Language: the authors write that "it only verifies Rust today". They suggest porting code or calling verified Rust through bindings.

The limits the authors state

• "Proofs still take real effort, mostly in producing the proof itself".
• "The guarantees are only as strong as the six trusted pieces", with the bcrypt wrapper and the two lookups carrying most of the weight: "Tests support them, but nothing proves them."
• The proof does not cover code in other crates (bcrypt, sqlx, jsonwebtoken), what the database or clock hold, whether or how fast login finishes, anything needing human judgement, or "Whatever nobody wrote down."
• On a wrong specification, the FAQ says: "A wrong spec is still possible".
• The toolchain (Verus, the Rust compiler and the Z3 solver) and Verus's standard library are assumed correct.
• The demo covers "one piece of one app", the login. The authors say the same process "can be used" for a whole app and that "we want to find out how far this scales."

Why it matters

The authors argue that teams should rely less on line-by-line review of agent code and more on reviewing what they meant, in plain language, with a proof holding the code to it. On our reading, the parts worth studying today are the "both ways" question and the published list of what was trusted rather than proved. UK teams have no obvious way to pick up PDD Kit yet: we found no public release, it targets Rust only, and the planning tool it runs in was described by its makers in September as not ready to use, with alpha users expected "within a month or so".