Microsoft's PDD Kit Formally Proves AI-Written Rust Code Actually Works

Microsoft Research has introduced the PDD Kit, a research prototype for checking whether agent-generated code satisfies a developer’s requirements. The toolkit converts those requirements into machine-checkable specifications, then uses a formal verifier to prove that supported Rust code meets them across all modeled inputs and execution paths.

Agent-generated changes can span tens of thousands of lines, making exhaustive pull-request review impractical. Natural-language plans and tests help, but an agent can misread the plan and write tests that encode the same misunderstanding. Tests exercise selected cases; formal verification reasons about every case covered by the specification and model. Any omitted requirement, incorrect assumption, or unmodeled dependency remains outside the proof.

Formal methods have historically required specialist skills and have concentrated on systems such as kernels, cryptographic software, and aerospace controls. PDD Kit packages parts of that process inside GitHub Next’s Chopin planning environment, where developers and coding agents share requirements, implementation artifacts, proofs, tests, and trust assumptions. It uses Verus, a Rust verification tool co-developed by Microsoft Research and university researchers.

From developer intent to CI evidence

PDD Kit divides the workflow into explicit stages so that requirement decisions, proof obligations, and unverified dependencies remain visible during review.

Requirements that Verus can express become preconditions, postconditions, and related proof obligations. Requirements involving interfaces, external services, runtime state, or unsupported libraries remain informal specifications backed by tests and reviewed assumptions.

Three evidence labels

• Formal verification: Verus proves that supported code satisfies its specification for all inputs represented by the model.
• Empirical verification: Tests cover behavior outside the verifier’s model, including user interfaces, databases, system time, and third-party libraries.
• Trusted Computing Base: The pull request identifies wrappers, contracts, tools, and assumptions whose correctness the developer must review and approve.

A login request becomes eight guarantees

Microsoft evaluated the workflow with Pet Store, a roughly 5,000-line full-stack Rust application built with Axum, SQLite, and a Leptos WebAssembly frontend. The team focused its formal verification work on a login flow derived from two developer requirements: a token requires the correct password, and an administrator token requires an administrator account.

The password requirement contains a logical ambiguity. A rule stating that every issued token must follow a correct password allows an implementation that rejects every login, since such an implementation never issues an invalid token. Guaranteeing successful authentication also requires the reverse condition: valid credentials must produce a token. PDD Kit presents that choice in a decision card so the developer can select a one-way implication or an “if and only if” requirement before implementation begins.

The two initial sentences expand into eight ensures clauses on the asynchronous login_flow function. PDD Kit decomposes the proof across smaller functions, including lookup_target, login_core, decide_login, and issue_token.

Bcrypt operations, SQLite queries, JWT signing, and clock access sit outside Verus’s model. Thin wrappers expose those operations through assumed contracts and matching tests, using annotations such as #[verifier::external_body] and external_fn_specification. The proof remains valid only when those contracts accurately describe the wrapped behavior.

Mutation tests challenge weak specifications

Agent-authored specifications can contain weak invariants that verify successfully while excluding little unwanted behavior. Microsoft calls this failure mode “vibe verification”: the proof is mechanically valid, but the specification fails to capture the developer’s actual requirement.

The pdd-prove workflow probes each ensures clause by inserting a targeted defect into a temporary copy of the implementation. Example mutations include rejecting every login or changing account-lookup precedence. Verus should reject each mutant because it violates the clause under examination. A surviving mutation signals that the clause is weak, disconnected from the behavior, or missing a necessary condition.

Two additional reviewer agents inspect the derived specification for omissions and questionable assumptions before the developer approves it. Their critiques supplement the verifier because mathematical proof cannot determine whether the specification itself expresses the intended product behavior.

The proof ends at explicit boundaries

PDD Kit remains a Rust-only research prototype because its formal workflow depends on Verus. Components written in other languages require a Rust port or bindings, and behavior beyond the verified Rust model must enter through trusted contracts.

• External code: Bcrypt hashing, sqlx queries, JWT signing, and similar dependencies remain outside the proof unless modeled or verified separately.
• Runtime facts: The verifier cannot establish the current contents of a production database or the value returned by a real system clock.
• Termination: The postconditions describe results returned by an asynchronous future; they do not guarantee that the future will complete.
• Subjective requirements: Usability, wording quality, and visual design still require human evaluation.
• Specification omissions: Behavior absent from the formal and informal requirements can fail without violating any proof.

In the Pet Store example, password guarantees depend on the trusted check_password wrapper, while account-identity guarantees depend on two lookup wrappers. Tests cover those components, but the formal result assumes their contracts are accurate. Microsoft expects this trusted boundary to shrink as Verus supports more code and libraries.

A new contract for pull requests

PDD Kit changes the evidence available during review. A pull request can associate each requirement with a formal proof, an empirical test, or an explicit trust assumption, while pdd-ship reruns Verus in CI and blocks changes that invalidate established proofs.

Human review remains necessary for the intent artifact, formal clauses, trusted boundaries, tests, security architecture, and maintainability. The verifier handles a narrower question with stronger guarantees: whether the modeled implementation satisfies the approved formal specification.

The current tooling applies only to Rust, but its workflow can inform agent-assisted development in other ecosystems. Requirements can be resolved before implementation, evidence can be attached at the requirement level, and unverified dependencies can be exposed for review. Authentication, authorization, payments, and other rule-heavy services offer practical targets because their core guarantees can often be written as precise conditions.