Formally verifying agent-written full-stack web apps with PDD Kit

Microsoft Research has described PDD Kit, a research prototype that aims to replace line-by-line review of AI-generated code with review of intent. In a November 5, 2026 post, researchers Alex Lavaee and Matthai Philipose say the tool turns a developer's plain-language goals into a formal specification in Verus, a proof language for Rust, then has agents write code and proofs showing the specification holds for every input. Where proofs cannot reach, it falls back on tests and labels those results as evidence, not proof.

The team demonstrated it inside Chopin, GitHub Next's collaborative planning environment, on the login logic of Pet Store, a roughly 5,000-line Rust web app. A two-sentence developer request became eight guarantees on the login function, covering rules such as a token requiring the right password and admin tokens going only to admin accounts. According to the authors, the process uncovered existing bugs, and the developer merged without reading the generated code line by line. To catch specifications that prove little, a mutation check plants deliberate bugs that Verus must reject.

The authors are candid about limits. Six trusted components, including password checking through bcrypt and the database lookups, sit outside the proof and are only tested, and a wrong specification would yield wrongly verified code. PDD Kit handles only Rust directly, and proofs still take real effort. The work matters because agents now produce more code than people can realistically inspect, and it suggests formal methods could reach engineers without specialist training, though only one piece of one app has been shown so far.