Microsoft Research finds login bugs with mathematical checks of AI-written code

Microsoft Research says it uncovered existing login bugs by using PDD Kit to mathematically check part of a Rust storefront app. In a November 5 demonstration, the developer reviewed requirements rather than reading generated code line by line. The result came with a critical boundary: the proof established compliance with a specification, not freedom from every possible bug.

The researchers built Pet Store, a full-stack web app with roughly 5,000 lines of Rust, then focused the demonstration on its login logic. Their starting problem was a mismatch between instructions and implementation: a coding agent can build something different from the requested plan, then write tests that validate its own interpretation.

The developer began with two requirements: issue a login token only for the right password, and issue administrator tokens only to administrator accounts. PDD Kit’s first job was not to generate code. It read the existing code and asked questions to turn that rough request into something precise enough to verify.

One question exposed a meaningful ambiguity. A system that never lets anyone log in still satisfies the rule that nobody gets a token with a wrong password. To rule out that outcome, the developer also required the reverse: the correct password must produce a token. Both directions became part of the agreed behavior.

PDD Kit runs inside Chopin, GitHub Next’s shared planning environment, and uses Verus, a proof language for Rust. It records decisions in an intent document linking the developer’s requirements to formal specifications and tests. Microsoft describes the workflow as usable without a formal-methods background; the human reviews explanations and decisions rather than having to write the mathematical specification unaided.

The initial plan covered the central login decision: choosing the account table and checking the password. It left the surrounding handler—the code coordinating lookups and token signing—trusted and tested. The developer asked to include that coordination in the proof, too, because a refactor could quietly change the order of operations.

The revised design put that work in a new function, login_flow, with a contract covering the path from request fields to a token or an HTTP error. PDD Kit then sought fresh approval for the expanded plan. Agreeing that a plan captures intent does not automatically authorize a wider verification scope or new assumptions.

The login proof still depended on components Verus could not inspect, including database queries, password hashing and token signing. Clock access also sat outside the proof. PDD Kit made those dependencies explicit, asked the developer to accept their assumed behavior individually, and put tests for the assumptions into the plan.

There are limits beyond dependencies. The specification describes the result if login answers; a hung or slow database query does not violate it. Nor can the proof establish whether an error message is useful, or cover a requirement nobody wrote down. Those boundaries qualify Microsoft’s claim that the exercise proved the absence of login bugs relative to the specification.

Microsoft recommends starting with an application’s most sensitive parts and expanding verification incrementally. In Pet Store, login was the starting point because a mistake could expose customer accounts or administrator controls. The demonstration stops short of verifying the entire storefront, even though the researchers say the same process can be applied to its broader functional correctness.