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 of the pull request doesn’t scale to this new way of work. Now, most teams invest in the plan and relevant testing instead: describe to an agent what they want, go back and forth until the plan and proposed tests look right, and hand them off to the agent for implementation.  This plan or natural language spec is meant to be the contract that an agent holds. However, in practice, the agent can drift from it. It implements something slightly different, then writes tests that pass for its implementation rather than the code you intended it to write. Continuous integration (CI) grows due to a profusion of low quality and high quantity of tests, coverage looks healthy, and the gap between what you asked for and what shipped stays hidden until a bug report or a nasty edge case shows up. So, how do you reliably scale review as agents generate increasingly large amounts of code? Agent code fails in two ways a careful reviewer would usually catch: it leaves out something obviously necessary, or it does something obviously wrong. Tests alone don’t close that gap, because they only exercise a tiny slice of what a program can do. Closing it needs a different kind of machinery, which is where proofs come in. Review asks “does this look right?” A proof answers “is this right?” A mathematical proof shows that code meets its specification for every input, including the ones your test suite can miss. That provides stronger assurance for specified properties than testing alone, especially when line-by-line review isn’t practical. Proofs used to be too expensive for everyday software. You needed specialists, unfamiliar languages, proofs many times larger than the code, and proofs took years to develop, but two things have changed since. First, recent advances in coding agents have made it increasingly practical for them to help generate formal proofs from well-defined specs. Secondly, agents can now better help you write formal specs. We call this new software development paradigm Proof-Driven Development (PDD). PDD Kit is our toolkit for it. How PDD Kit works PDD Kit is to formal methods roughly what Spec Kit (opens in new tab) is to Spec-Driven Development. It runs as a partner inside Chopin (opens in new tab) , GitHub Next’s real-time, multiplayer planning environment, where a team and agents can plan in one shared document. The workflow has two halves (Figure 1). First, team members review intent in plain language. PDD Kit asks the questions a careful reviewer would ask, explains the relevant code as it goes, and records the answers in an intent artifact , a document that bridges the user’s intent with the formal specification or tests. The parts of the user’s intent that can be formalized are converted into formal specifications and the rest, which must be taken on trust, are converted to informal specifications for tests. PDD Kit automatically generates proofs that the code satisfies the derived formal specs and high-quality tests for the informal specs. You don’t need a formal methods background for any of it.  Consequently, every result in PDD Kit says which kind of verification it rests on:  Formal verification is a mathematical proof that code satisfies its specification for every possible input, checked by a tool called a verifier. For PDD Kit today, that verifier is Verus (opens in new tab) , a proof language for Rust co-developed by Microsoft Research, Carnegie Mellon University, VMware Research, ETH Zurich, MPI-SWS, UNSW Sydney, the University of Texas at Austin, the University of Michigan, the University of British Columbia, the University of Wisconsin–Madison and the Weizmann Institute of Science. Empirical verification checks code by running it and observing what it does. It covers what a proof can’t reach, such as a third-party cryptography library or a user interface. It uses unit and end-to-end tests, terminal automation, browser agents, and computer-use agents for anything a browser can’t drive. A passing test only shows the code worked on the inputs it tried, so PDD Kit labels it as evidence rather than proof. The line between the two is the Trusted Computing Base (TCB) : the code that the proof assumes behaves as described. PDD Kit makes that line explicit and asks you to sign off on each piece.  The capstone: a full-stack web app To show PDD Kit integrating with existing codebases, we built Pet Store, a full-stack web app written entirely in Rust (opens in new tab) . The backend uses Axum (opens in new tab) and SQLite (opens in new tab) and handles inventory, promotions, orders and checkout. The storefront is a Leptos (opens in new tab) app compiled to WebAssembly (opens in new tab) . Together they come to about 5,000 lines of Rust. For brevity in this blog, we focus on formally verifying the login logic of the app, but the same process can be used to verify functional correctness of the entire app. PDD Kit recommends starting with the most sensitive parts of your application and incrementally verifying your application. A login bug can hand an attacker a customer’s account or an admin’s controls, so that’s where proof effort pays off first. The developer’s whole request in Chopin was two sentences:  Verify the login logic in backend/src/handlers/auth.rs. Here are my requirements: You only get a token with the right password. Only admin accounts get admin tokens. We kept the request rough on purpose. Capturing the intent of the user and turning the user request into something a proof can check is PDD Kit’s job. Step 1: Questions before code PDD Kit’s planning workflow, pdd-plan, reads the code and comes back, before writing anything, with questions in a Decisions tab. When a question depends on how the code works, the card explains that part first: the goal, how the pieces fit, and the exact function involved, so you can answer without opening the source.  The question looks pedantic, but it matters. “You only get a token with the right password” rules out the bad case, a wrong password getting a token, and a login that refuses everyone keeps that promise perfectly. “The right password always works” is the half that rules it out. Formally, the first is an implication (token ⇒ right password) and the second