PDD Kit uses Verus to formally verify agent-written Rust web apps

• PDD Kit (Proof-Driven Development Kit) transforms natural language intent into formal Verus specifications to prove agent-written code meets requirements for every input, addressing the impracticality of line-by-line human review for AI-generated code.
• In a Pet Store case study (approx. 5,000 lines of Rust), the tool formally verified login logic derived from a two-sentence user request, distinguishing between formal proofs (mathematical certainty) and empirical tests (evidence for specific inputs).
• The verification process identifies a Trusted Computing Base (TCB) of six components, including check_password and database lookups, which are tested but not proved; the system uses mutation checking to flag weak invariants that verify but rule out little.
• Currently a research prototype supporting only Rust via Verus, PDD Kit integrates with GitHub Next's Chopin environment and adds Verus checks to CI, ensuring that any code change breaking the proof fails the build.

Verification Mechanics

• Formal verification uses Verus (a Rust verifier) to check ensures clauses and ghost code, while empirical verification runs unit and end-to-end tests labeled as evidence.
• The login_flow contract contains 8 ensures clauses, including 4 preserving existing refusal behaviors (400/401/500) and constraints ensuring tokens are issued only for the named account with the correct password.
• Modular proof strategy allows login_flow to be composed of smaller proved pieces (lookup_target, login_core, issue_token), where changing one function requires re-proving only that specific piece.

Scope and Limitations

• Proofs cover the bodies of login_flow and related functions for all inputs, but do not cover external facts like current SQLite state, system clock time, or termination/performance guarantees.
• The tool relies on the Verus, Rust compiler, and Z3 toolchain as assumed correct; other languages can be ported to Rust or call verified Rust via bindings.
• Recommended starting points for adoption are high-cost bug areas such as login, payments, and permissions, where clear specifications significantly reduce the effort required for proof generation.