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

At a glance 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. Verus hardened the code and uncovered existing bugs, proving the absence of login bugs with respect to the specification. The developer reviewed the intent and never read the generated code line-by-line. The plan is the contract the agent should follow, but nothing constrains the agent to follow it. Coding agents now ship whole features in one sitting often spanning tens of thousands or hundreds of thousands of lines of code. As a result, reading every line o

PDD Kit improves code reliability and reduces errors, but may also increase dependence on AI-generated code.

SOURCE     Microsoft Research (tier 1)
   ↓
DOCUMENT   92dd6400-26bd-489e-947a-51a2c4998714
           https://microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit
   ↓
EVIDENCE   2 extracted excerpts
   ↓
MODEL RUN  1 run, methodology 1.0.1
   ↓
SCORE      +50  (Favourable)
   ↓
CONFIDENCE 80%