PDD Kit Formally Verifies AI-Written Full-Stack Rust Apps
PDD Kit uses Verus proofs and targeted tests to verify AI-written Rust code, catching login bugs in GitHub Next’s 5,000-line full-stack Pet Store app.
Summary
Published November 5, 2026, PDD Kit brings Proof-Driven Development to agent-written everyday software inside GitHub Next’s Chopin planning environment. It turns team-approved plain-language intent into a Verus specification, asks clarifying questions, maps each requirement to contracts and tests, then has agents implement code and proofs. Verus mathematically checks specified properties for every input. Unit, end-to-end, terminal, browser and computer-use tests cover third-party libraries, interfaces and other unprovable behavior as evidence, not proof. Developers explicitly approve the Trusted Computing Base, while two reviewer agents refine the specification and an LLM verifier returns uncovered gaps to the coding agent.
In a Pet Store capstone, PDD Kit verified login logic in a roughly 5,000-line Rust full-stack storefront using Axum, SQLite, Leptos and WebAssembly. From a two-sentence request, it derived eight ensures clauses requiring tokens only for correct passwords, correct passwords to succeed barring lookup or signing failures, and admin tokens only for admin accounts. It introduced async login_flow, split work across five proved components and organized seven build tasks. Verus hardened the code, found existing bugs and proved the specified login properties without line-by-line human review. The proof trusts exact contracts for Customer::find_by_email, Admin::find_by_username, bcrypt checks, JWT signing, SQLite and sqlx failures, the clock and 24-hour expiry, and request unpacking. Each assumption receives developer approval and planned tests. It does not promise completion, safe out-of-range clock behavior, attempt timing, rate limits, downstream role handling, usability or unspecified requirements. PDD Kit recommends starting with sensitive code and expanding verification incrementally.
Positives
- Verus proved Pet Store’s specified login properties for every input and exposed existing bugs without line-by-line review of generated code.
- A two-sentence login request became eight precise contract clauses covering passwords, account identity, roles, tokens and existing HTTP errors.
- PDD Kit labels every result as mathematical proof or empirical evidence, making assurance levels and trusted assumptions explicit.
- Engineers can review plain-language intent artifacts and approve specifications without formal-methods expertise or reading agent-generated proofs.
- Verus was co-developed by Microsoft Research, Carnegie Mellon University, VMware Research, ETH Zurich and seven additional research institutions.
Risks & concerns
- Agent-generated features can span tens or hundreds of thousands of lines, making exhaustive pull-request review impractical.
- Agent-written tests may validate an implementation that drifted from the requested plan while inflating continuous integration workloads and apparent coverage.
- Verus cannot inspect bcrypt, sqlx or jsonwebtoken internals, so database, password and token guarantees depend on trusted contracts and tests.
- The login proof cannot guarantee completion, prevent clock-range panics, assess usability, constrain attempt timing or rate, or verify downstream role handling.
- A mathematically valid proof says nothing about requirements omitted from the approved specification.