Microsoft Tool Proves AI-Written Login Code

Microsoft Research said Nov. 5 that its PDD Kit prototype produced a machine-checked proof that AI-written login logic in a roughly 5,000-line Rust web app meets its specification for every input. The developer reviewed the intent and never read the generated code line by line, the researchers wrote.

Key takeaways

• PDD Kit turns a developer's plain-language intent into a formal specification and uses the Verus verifier to check agent-written Rust against it.
• In the Pet Store demo, a two-sentence request became eight proof clauses; five functions were proved and six pieces were left trusted and tested.
• Microsoft calls PDD Kit a research prototype. It verifies only Rust today, and the blog gives no bug count or proof cost for the demo.

How PDD Kit verifies AI-generated code

The toolkit runs inside Chopin, GitHub Next's multiplayer planning environment. Its planning step reads the code, asks questions before anything is written and records the answers in a document the team reviews. Coding agents then write the implementation and proof, and Verus checks the result using the Z3 solver.

"Review asks 'does this look right?' A proof answers 'is this right?'" the Microsoft Research post says. Models write the spec, code and proof, but the pass or fail decision comes from a deterministic Verus run.

The check typically takes seconds for a small module and up to minutes for a larger codebase, according to Microsoft. A later workflow adds it to continuous integration, so a broken proof fails the build.

What the Pet Store login proof covers

The developer's request was two requirements: a token only with the right password, and admin tokens only for admin accounts. PDD Kit then asked whether the right password must always work, because a login that refuses everyone would satisfy the first rule alone.

That exchange produced eight "ensures" clauses and a seven-task build plan. Five functions were proved for every input. To catch clauses that verify but rule out nothing, a step Microsoft calls guarding against "vibe verification," the tool plants one bug per clause in a scratch copy and requires Verus to reject each one.

Where the guarantee stops

Six pieces sit outside the proof: two database lookups, the bcrypt password check, token signing, the clock, the database error message and the handler's request unpacking. Each was accepted by the developer and covered by tests.

"The guarantees are only as strong as the six trusted pieces," the researchers wrote. The proof also does not promise that login finishes, or anything about timing or attempt rates. Microsoft says the run uncovered existing bugs but does not list them, and AI Newsway found no independent evaluation.

Why formal verification is back in focus

The work follows Anthropic's Oct. 22 report, covered by AI Newsway, that Claude proved 123 open-source libraries free of crashes under stated assumptions. AlphaSignal reported that GitHub Next and Microsoft Research introduced PDD Kit as a research preview on Oct. 21.

What's next

Microsoft recommends starting where bugs cost the most, such as login, payments or permissions. It expects the trusted boundary to shrink and says it wants to learn how far the method scales.

FAQ

Does a proof mean the code has no bugs? No. It shows the code meets its specification under stated assumptions. A wrong or incomplete specification is still possible.

Can teams using other languages use PDD Kit? Not directly. Code can be ported to Rust, or non-Rust projects can call verified Rust through bindings.

References

• Formally verifying agent-written full-stack web apps with PDD Kit — Microsoft Research (Nov. 5, 2026)
• GitHub - verus-lang/verus: Verified Rust for low-level systems code — Verus project
• Chopin — GitHub Next
• Microsoft's PDD Kit Makes Formal Math Proofs a Gate for AI Rust Code — AlphaSignal (Oct. 21, 2026)