THE ESSENTIALS IN 30 SECONDS

  • PDD Kit converts requirements agreed with a developer into Verus specifications, and a coding agent must write Rust code and proofs that Verus accepts.
  • In a Pet Store demo of about 5,000 lines of Rust, five login functions were proved while six components, including bcrypt password checks, stay trusted.
  • The tool is a research prototype that only supports Rust; its authors say the trusted parts carry much of the remaining risk.

Microsoft Research and GitHub Next have published a new case study for PDD Kit, a research prototype built around what they call proof-driven development. Instead of trusting tests that sample a few inputs, the approach asks coding agents to produce Rust code together with mathematical proofs, checked by the Verus verifier, that the code meets a formal specification for every allowed input. The kit was first shown as a research preview in October; the latest work applies it to a full-stack web application.

From reviewed intent to proof

PDD Kit runs inside Chopin, GitHub Next's planning tool. It reads the codebase and puts reviewer-style questions to the developer on "decision cards", recording the answers as an intent document. The parts of that intent that can be formalized become Verus preconditions and postconditions. A coding agent then writes the implementation and its proof, and Verus checks the result. Anything that cannot be proved must be named, accepted by a person and covered by tests, which the project labels as evidence rather than proof. Two reviewer agents compare the formal specification with the intent, an LLM-based checker looks for requirements left without a proof or a passing test, and a mutation step plants one bug per clause to confirm each clause actually constrains the code. Pull requests then list what was proved and what was trusted.

The Pet Store experiment

The demo application is a pet store of about 5,000 lines of Rust, with an Axum and SQLite backend and a Leptos storefront. The team focused on login, where a bug could expose customer accounts or admin controls, starting from a two-sentence request about password checks and admin tokens. The resulting asynchronous login flow carries eight postconditions; five functions are proved, while six pieces remain trusted, including the bcrypt password check, two database lookups and token generation.

Limits acknowledged by the authors

The project page states that PDD Kit only works with Rust for now and that writing proofs still takes real effort. Its guarantees are only as strong as the trusted components, and the team says nothing yet proves the password check or the lookups. The proofs do not cover whether login terminates, its speed, rate limiting or requirements nobody wrote down. Earlier coverage also noted that a specification can be valid yet miss what the developer meant, so human review of architecture and security boundaries remains necessary. The authors expect the trusted boundary to shrink over time but have not shown how far the method scales.