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

GitHub Next describes PDD Kit, a toolkit for Proof-Driven Development that turns a developer's intent into a formal specification in Verus, proves the agent's code meets that spec for every input, and falls back to tests where proofs cannot reach. The team applied it to Pet Store, a roughly 5,000-line Rust full-stack app, formally verifying its login logic while the developer reviewed the intent rather than reading generated code line by line. PDD Kit labels each result as either formal verification or empirical evidence and asks developers to sign off on each trusted component.