Microsoft Research proves agent-written login code against a spec reviewed in plain language

PDD Kit, which the authors call a research prototype, turns a developer's intent into a formal specification in Verus, has a coding agent write the implementation and proof, and falls back to tests where a proof cannot reach. The worked example is the login logic of Pet Store, a roughly 5,000-line Rust storefront. The developer's request was two sentences; the tool asked clarifying questions, and the result was eight ensures clauses on one function, login_flow. The developer signed off on six trusted pieces the proof assumes, including the bcrypt password check and the two database lookups, which the authors say carry most of the weight. The authors report that Verus uncovered existing bugs and that the developer never read the generated code line by line.

One mechanism applies beyond Rust. To catch what they call "vibe verification", proofs that hold but rule out almost nothing, the tool plants one bug per ensures clause and requires Verus to reject each. It verifies Rust only, and the post is the authors' own account of a single example.

Why it matters: The idea worth taking is the mutation check on the spec: an agent that writes its own spec and proof can satisfy both without constraining anything, and planted bugs are a cheap way to test that. The claim that review can shift from code to intent rests on one login function so far.