Microsoft Releases PDD Kit to Formally Verify Agent-Generated Code

Summary:Microsoft Research has introduced PDD Kit, a research prototype that brings Proof-Driven Development to agentic software development. Developers approve a plain-language intent artifact, after which the system derives Verus specifications, proofs, and tests for trusted boundaries. Verus uses Z3 to deterministically check whether the implementation satisfies the approved contract for every input covered by the model. The toolkit's Pet Store case study applies the workflow to Rust login logic, ca

---

Microsoft Research has introduced PDD Kit, a research prototype designed to address a scaling problem in agentic software development: coding agents can now produce tens of thousands or hundreds of thousands of lines, making exhaustive human review impractical. Tests generated by the same agent may also validate the implementation it happened to write rather than the behavior the developer requested.

PDD Kit does not primarily generate more tests. It turns a development plan into a machine-checkable contract. Developers first approve the intended behavior, after which the system derives Verus specifications and proofs. Parts that formal verification cannot reach, such as third-party libraries, database state, user interfaces, and the system clock, remain inside an explicitly documented trust boundary and are checked through empirical tests.

From Natural-Language Intent to a Formal Contract

The workflow has three main stages: planning, proving, and continuous delivery.

pdd-plan reads the existing codebase, asks decision questions before generating an implementation, and produces a human-readable intent artifact. This artifact links the developer's original request to formal specifications, tests, trust assumptions, and approval decisions.

Requirements that can be modeled formally are translated into Verus specifications. Requirements that cannot be expressed as proofs are retained as informal specifications backed by tests. Contradictions and ambiguities stop the workflow and return to the developer.

This distinction is essential: a proof establishes that code satisfies a specification, not that the specification captures human intent. The login requirement “you only get a token with the right password” appears precise but actually means token ⇒ correct password. A login implementation that rejects every user satisfies that statement. PDD Kit asks for the converse, correct password ⇒ token, turning the requirement into a genuine equivalence.

How Verus Verifies the Login Flow

The demonstration uses Pet Store, a roughly 5,000-line Rust full-stack application with an Axum and SQLite backend and a Leptos frontend compiled to WebAssembly. The formal verification effort focuses on authentication rather than attempting to prove the entire application.

The login flow is decomposed into five principal functions:

• lookup_target selects the customer or administrator table from the supplied identity fields;
• decide_login handles account existence and password matching;
• issue_token signs a token or maps a refusal to an HTTP error;
• login_core composes lookup, password validation, and token issuance;
• login_flow specifies the complete asynchronous path from request fields to a token or error.

Each function carries requires and ensures contracts. A typical postcondition binds the account used for password validation to the token subject and role. If an implementation validates Bob's password but signs a token for Alice, the shared account variable in the contract prevents Verus from accepting the code.

SQLite contents, bcrypt decisions, and token claims are represented as uninterpreted functions. The verifier does not need to understand the internal algorithms of those systems; it reasons from their external contracts. Their specification definitions are ghost code, checked by the verifier but erased from the compiled program.

For an async fn, requires is checked when the call creates the future, while ensures applies when the future yields a result. The contract does not guarantee eventual completion. A permanently blocked database query can therefore satisfy functional-correctness clauses while violating latency, liveness, or availability expectations that must be verified separately.

The Trusted Computing Base Defines the Guarantee

PDD Kit explicitly separates verified logic from assumptions. In the login example, Verus proves five core functions, while six component categories remain trusted:

1. Customer and administrator database lookups;
2. check_password, which wraps bcrypt;
3. JWT token signing;
4. The system clock and expiry calculation;
5. Database error-message mapping;
6. HTTP request unpacking and field forwarding.

External functions receive assumed contracts through external_fn_specification, while external_body lets Verus check a contract without inspecting the implementation. PDD Kit creates a Given/When/Then test for each assumption and requires the developer to accept the assumption and its failure consequences individually.

This is more precise than claiming that the application is “fully verified.” The security claim depends on whether the trusted contracts accurately describe real behavior. In particular, check_password and the database lookups carry most of the password and account-identity guarantees. Their tests are empirical evidence, not formal proof.

Mutation Checking Against “Vibe Verification”

A language model can readily produce a specification that verifies but imposes almost no useful constraint. PDD Kit calls this vibe verification.

To detect it, pdd-prove injects one targeted mutation per ensures clause into a scratch copy of the code. Examples include rejecting all logins or reversing the email and username lookup order. If a mutation survives, the corresponding clause does not constrain the intended behavior, and the system reports a verification gap.

During this phase, models write code, specifications, and proofs, but the final verdict comes from the deterministic Verus and Z3 toolchain rather than a model approving its own work. An LLM gap review compares requirements, specifications, and verification results to detect uncovered obligations. If the pinned Verus version cannot express an async construct, the task stops rather than silently weakening the contract.

Engineering Value and Cost

The immediate benefit is a redistribution of review work. Humans review intent, formal specifications, and trusted boundaries, while deterministic tools check whether the implementation meets the approved contract. Proof failures can block CI in the same way as failing tests. Once example-based behavior is formally covered, redundant tests can be removed, leaving the suite focused on trusted components and end-to-end behavior.

The workflow is not a fully automatic route to whole-program correctness. The primary cost lies in specification design and proof authoring, not in the final Verus execution. Small modules may take seconds to verify, while larger codebases can take minutes. Agents can lower the cost of writing proofs, but they do not remove SMT-solver complexity, asynchronous modeling constraints, or external dependencies.

The prototype currently supports Rust only because Verus verifies Rust directly. Other-language systems can port critical logic to Rust and expose it through bindings, but that introduces interface-consistency and operational overhead. Verus, Z3, vstd, and the underlying compiler toolchain are themselves assumed trustworthy.

Formal verification also does not automatically establish liveness, throughput, availability, security-response time, or user experience. Whether the login future completes, whether queries time out, whether brute-force rate limiting works, and whether downstream endpoints honor the role remain outside this proof's guarantees.

Practical Adoption Guidance

1. Start with high-risk boundaries. Prioritize authentication, payments, authorization, and data-access policy instead of attempting to prove the entire repository at once.
2. Resolve ambiguity first. Confirm equivalence, error semantics, and role mappings so the system does not precisely prove the wrong requirement.
3. Document the TCB explicitly. For every external function, record its assumption, failure consequence, and corresponding empirical test.
4. Run Verus in CI. A proof must remain a continuous gate; otherwise later edits quickly invalidate the contract.
5. Retain empirical verification. Third-party cryptography, database semantics, clocks, UI behavior, termination, and performance still require dedicated tests and independent audits.
6. Treat pull requests as verification receipts. Mark every requirement as formally proved, empirically checked, or explicitly unpromised.

PDD Kit's central contribution is not the elimination of code review. It is a more precise allocation of review responsibility: people own intent and trust assumptions, while deterministic tools enforce the properties that can be mechanically decided.

---

Source: Microsoft Research AI (2026-11-05)

— END —

Tags: #PDD Kit Follow #Formal Verification Follow #Verus Follow #Rust Follow #Coding Agents Follow