# Microsoft Research — Formally verifying agent-written full-stack web apps with PDD Kit

- Company: Microsoft Research (microsoft.com)
- Announced: 2026-11-05T16:00:00+00:00
- Category: developer-tool-release
- Coverage: not counted
- Announcement: yes
- Group: announcements
- Source: https://www.microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit/
- Record: https://forck.live/items/32207-formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit
- Subject: Research / Phi

Microsoft Research has released PDD Kit, a toolkit that helps turn a coder's intent into a formal spec and then proves the code an agent writes matches it for every input. The problem it answers is scale: agents now ship whole features spanning tens of thousands of lines, so reading every line of a pull request no longer works for most teams. Plan and tests are meant to hold the agent to that contract, Microsoft says, but nothing constrains the agent to follow the plan, and the tests it writes usually check what it built rather than what was asked for. PDD Kit runs inside GitHub Next's Chopin, asks the questions a careful reviewer would ask, and records the answers in an intent artifact bridging intent with the specification or tests. The parts of intent that can be formalized become formal specs and the rest become informal specs for tests, with proofs generated automatically by Verus, a Rust proof language co-developed by Microsoft Research and several universities. Microsoft says its own trial formally verified the login logic of Pet Store, a Rust storefront, and that Verus uncovered existing bugs; the developer reviewed the intent and never read the generated code line-by-line.

## Evidence

Verbatim from https://www.microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit/:

> Formal methods for everyday software. PDD Kit helps you turn your intent into a formal spec, then proves the code your agent writes for every input and uses tests where a proof can’t reach. It takes formal methods beyond niche, specialist work to engineers without a formal methods background and to everyday applications, like the full-stack web app shown here.
> 
> Exhaustive line-by-line human review can become difficult to scale as AI agents generate increasingly large amounts of code. The plan is supposed to be the contract between you and a coding agent, but nothing actually forces the agent to follow it. The tests it writes usually check what it built, rather than what you asked for.
> 
> PDD Kit makes the agent keep the plan. It works with you to turn your intent into a formal specification in Verus (opens in new tab) , proves the agent’s code meets that spec for every input, and falls back to tests where a proof can’t reach.
> 
> We tried it on a full-stack web app. Inside GitHub Next’s Chopin (opens in new tab) , we used PDD Kit to formally verify the login logic of Pet Store, a Rust (opens in new tab) storefront.

---

Record: https://forck.live/items/32207-formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit
Catalogue: https://forck.live/llms.txt
Current issue: https://forck.live/feed.md