Microsoft Research has introduced PDD Kit, a new toolkit designed to enforce formal verification on code generated by AI agents. The tool addresses a critical failure mode in autonomous software development: agent drift. While current workflows rely on natural language plans and self-generated tests, agents frequently implement logic that deviates from user intent while passing their own limited test suites. PDD Kit bridges this gap by converting developer intent into formal specifications using Verus, a proof language for Rust, ensuring the agent’s output mathematically satisfies the contract.

The Problem with Self-Verified Code

Coding agents now ship features spanning tens of thousands of lines, making line-by-line human review impractical. Teams rely on a 'plan' as the contract, but nothing forces the agent to adhere to it. The agent often writes tests that validate what it built, not what was requested. This creates a false sense of security where CI passes and coverage looks healthy, yet edge cases remain unverified. PDD Kit replaces this empirical guesswork with mathematical proofs for specified properties, providing assurance that the code behaves correctly for every possible input, not just the ones the agent chose to test.

Inside the Proof-Driven Workflow

The toolkit operates within GitHub Next’s Chopin, a real-time planning environment. The workflow begins with 'pdd-plan,' which interrogates the user to clarify ambiguous requirements before any code is written. For example, a request like 'you only get a token with the right password' is split into two formal clauses: one preventing wrong passwords from granting tokens, and another ensuring right passwords always work. This prevents the agent from silently choosing a weaker implementation, such as a login system that rejects everyone. The tool generates a 'Trusted Computing Base' (TCB) map, explicitly marking which components are proven by Verus and which are trusted assumptions checked by tests.

Case Study: Verifying Pet Store Login

To demonstrate efficacy, the team applied PDD Kit to 'Pet Store,' a 5,000-line full-stack Rust application using Axum, SQLite, and Leptos. They focused on the login logic, a high-stakes area where bugs can expose customer accounts. The developer provided a two-sentence requirement, and PDD Kit generated Verus contracts that proved the core authentication logic. The process uncovered existing bugs and hardened the code. Crucially, the developer reviewed the intent and the formal spec, but never read the generated Rust code line-by-line. The proof covers the logic for every input, while trusted wrappers handle external dependencies like bcrypt and database queries.

Key Takeaways

  • PDD Kit uses Verus to generate mathematical proofs that agent-written code meets formal specifications for all inputs.
  • The tool forces agents to adhere to intent by clarifying ambiguous natural language into precise formal contracts before coding.
  • It explicitly separates 'proven' logic from 'trusted' external dependencies, reducing the risk of silent agent drift.
  • The workflow allows developers to verify complex agent-generated code without reading every line, scaling review efforts.

The Bottom Line

This is the missing layer of trust for autonomous coding. If your agent can't prove it followed the spec, it's just guessing.