Microsoft Research Introduces PDD Kit for Formally Verifying Agent Code

Addressing the scalability limits of line-by-line human review as AI coding agents generate large software codebases, Microsoft Research introduced Proof-Driven Development (PDD) supported by PDD Kit. Working inside GitHub Next's collaborative planning environment Chopin, the toolkit acts as a partner to capture user intent, formulate formal specifications in Verus—a Rust formal verification language developed across academic and industrial research groups—and generate mathematical proofs ensuring code satisfies specifications across all inputs. For components outside formal verification scope, such as third-party crates, database lookups, and system clocks, PDD Kit delineates a Trusted Computing Base (TCB) where developers explicitly approve assumptions and bind them to empirical testing suites.

Key takeaways

• PDD Kit translates human plain-language intent into formal specifications in Verus to verify agent-generated code across every input, using empirical tests where proofs cannot reach.
• The system operates inside GitHub Next's Chopin environment, prompting interactive decision cards to resolve natural-language requirement ambiguities before implementation.
• In a full-stack Rust demonstration, the toolkit formally verified login logic without requiring the developer to read agent code line-by-line, uncovering existing bugs.
• The tool explicitly tracks the Trusted Computing Base (TCB), requiring human sign-off on unproved external assumptions such as third-party hashing, database queries, and system time.