Microsoft's PDD Kit Makes an AI Agent Prove What a Login Requirement Means

“Only the right password gets a token” sounds strict. It still allows a broken login that refuses every password. Microsoft’s new Proof-Driven Development workflow uses this logical gap to show where reviewing AI-generated code should begin: with the meaning of the requirement.

The requirement is not the specification

Microsoft Research describes PDD Kit as a workflow inside Chopin, GitHub Next’s shared planning environment. A developer states a requirement in ordinary language. The kit asks questions, records decisions in an intent artifact, derives a formal specification for properties that can be proved, and creates tests for the rest. After people approve the plan, agents generate implementation and proof work for Verus, a verifier for Rust. ^{[1] [2]}

The login example starts with two rules: the user gets a token only with the right password, and only administrators get administrator tokens. The first rule is one-way: if a token exists, the password must have been correct. It does not say that a correct password will succeed. A service that rejects everyone satisfies the rule literally. PDD Kit asks the developer to choose whether both directions are intended before proof work begins. ^[1]

Requirements often hide an unstated converse. “Only admins can delete this record” does not guarantee an authorized admin can delete it. “Never send without consent” does not say what affirmative consent looks like. A model can implement a grammatical interpretation while missing the behavior people assumed.

What did the proof cover?

The example is a roughly 5,000-line Rust application with an Axum backend, SQLite database and Leptos/WebAssembly frontend. Microsoft’s post focuses on login logic. Verus checks selected functions against contracts for account lookup, password decision and token claims. The authors describe the proof as applying to every input in the formal model, which is stronger than passing selected test cases. ^[1]

But “formally verified” is not a synonym for “the whole application is secure.” The post identifies a trusted computing base: components whose behavior the proof assumes. Database lookups, bcrypt password checking, the clock, token signing and parts of the request handler sit outside parts of the proof and receive tests or trusted contracts. The verifier, compiler, solver and Verus libraries matter too. If an assumed wrapper contract is wrong, a proof can be internally valid without establishing the real-world claim the team cares about. ^{[1] [3]}

A test can show that one known wrong password does not receive a token. A formal contract can constrain all modeled inputs. Neither establishes that an unverified database query reached the right user’s record. Teams need both, with a clear map of which promise rests on which evidence.

Review the contract before the code

PDD Kit changes the order of review. It presents decision cards that explain relevant code and expose ambiguous choices before an agent writes. It then asks the developer to approve the intent map and derived formal plan. If a later choice widens scope or adds an assumption, the plan returns for approval rather than treating that as an invisible implementation detail. ^[1]

That makes intent review more important. Reviewers should ask: What does success mean, including the positive case? Which identities can cross each authorization boundary? What happens when an account is missing, a hash is unreadable or a dependency fails? Which values come from outside the program? What must remain true for unusual inputs?

Formal notation can expose gaps by forcing an abstract statement to become explicit. It cannot decide whether a product should allow a role transition, whether recovery should invalidate old sessions, or whether the prompt omitted a requirement. Those remain policy and design choices.

Our database transaction explainer covers a related boundary: a proof of one function does not by itself settle the behavior of its storage and callers.

Where this approach fits

PDD Kit currently centers on Rust and Verus. Verus is a research and engineering project for proving properties of Rust programs; its repository notes that it supports a subset of Rust and is expanding that coverage. It is not a drop-in checkbox for every language or dependency. ^{[2] [3]}

A sensible first target is a compact, high-consequence decision with a tractable boundary: authorization, state transitions, payment invariants or safety checks. Write both positive and negative behavior. Define which inputs the model covers and which real components remain trusted. Then test those components against the contracts they are supposed to satisfy.

For another example of making machine-produced claims traceable, see our guide to source-aware verification for agent citations.

Do not discard ordinary code review or integration tests. Use proof to reduce uncertainty about a specific invariant, tests to exercise dependencies and interfaces, and human review to decide whether the specification is the right one. That is more useful than asking one reviewer to inspect thousands of generated lines and infer every hidden assumption.

A receipt, not a certificate for everything

Microsoft describes a pull request that records what was formally proved, what was empirically tested and what remained trusted. This evidence ledger is more useful than a badge saying “verified.” It gives maintainers somewhere to focus: the approved contract, the assumptions behind it and the edges the proof does not reach. ^[1]

For teams using coding agents, ask the agent to make the requirement precise before implementation, and insist that the proof report its boundary. The most important review question remains human: “Does this specification describe the behavior we meant to ship?”