Microsoft tests formal proofs for AI-written Rust code

Microsoft Research and GitHub Next have demonstrated PDD Kit, a prototype that asks AI coding agents to produce mathematical proofs alongside their code. In a walkthrough published on 5 November, the researchers used it to verify the login logic of a Rust web application against an agreed set of rules.

The test involved PetStore, a storefront with about 5,000 lines of code. The researchers say the process uncovered existing bugs and let the developer merge the change without reviewing every generated line. The proof covered the login flow, not the whole application.

PDD stands for proof-driven development. The kit runs inside Chopin, GitHub Next's shared planning environment, where people and agents work on the same document. A developer reviews what the software should do; the agent turns the agreed requirements into a formal specification, writes code and supplies proofs for a separate tool to check.

A password rule that still allows a broken login

One of the PetStore requirements said a user should get an access token only with the right password. Taken literally, a login system that rejected everyone would satisfy it. No wrong password would ever receive a token, but no correct password would either.

PDD Kit asked the developer to settle that ambiguity before proceeding. The developer chose a stronger rule: valid credentials should produce a token, subject to the defined error cases. The plan also specified which accounts could receive administrator access and how to handle missing credentials, failed lookups and signing errors.

Microsoft Research comparison showing that a rule allowing tokens only with the right password can still permit refusing a valid login; the stronger rule requires a token for a valid password. — Microsoft Research’s simplified comparison of two login policies. The complete demonstration also specifies database, password-checking and token-signing errors. Source: Microsoft Research, 5 November 2026. Select the image to enlarge.

The difference matters to what the checker can establish. A proof that code follows a weak or mistaken rule can be valid even when the resulting program does not do what its developer intended. Microsoft identifies getting the specification right as a remaining human responsibility.

The proof is checked by Verus

PDD Kit uses Verus, an existing open-source tool that verifies Rust code against formal specifications. Verus relies on the Z3 solver to check the proof mechanically. An AI model does not decide whether that proof passes.

Ordinary tests run a selection of examples. A formal proof establishes the specified properties for every input covered by the model, under its stated assumptions. Verus itself supports a subset of Rust and remains under active development, according to its project documentation.

For PetStore, the contract had eight conditions describing the login result. They included tying a token to the same account whose password was checked, preserving the correct role and returning the specified error without issuing a token when login failed.

The workflow also challenged the specification. It introduced a deliberate bug for each condition in a scratch copy of the code and checked that Verus rejected it. A bug that survived would expose a gap in what the condition ruled out. Two AI reviewers checked the translation from requirements to specification, but those reviews were separate from the mechanical proof.

Once a change passes, PDD Kit can put the Verus check into the project's continuous-integration build alongside tests. Later edits must still satisfy the contract or fail that check.

What remains outside the proof

Microsoft's demonstration verified five functions, including the main login flow. It did not prove the database queries, the bcrypt password check, the clock or the signing of JSON Web Tokens, which carry the account's identity and role.

Microsoft Research diagram separating the verified login functions from tested assumptions such as database lookups, bcrypt, the clock and JWT signing, and from properties not promised by the proof. — The researchers’ diagram of the PetStore login proof. The green functions are verified under the stated assumptions; surrounding services and omitted requirements are not proved. Source: Microsoft Research, 5 November 2026. Select the image to enlarge.

Those components were treated as trusted dependencies, with contracts the developer accepted and tests against the actual libraries and database. The researchers name the password checker and account lookups as particularly important assumptions: the login guarantees depend on them behaving as specified.

The proof also made no promise about how quickly a login would finish, whether a stalled database query would return, the rate of login attempts or how other endpoints would use the role in a token. Requirements absent from the specification were not covered.

GitHub Next lists PDD Kit as a research prototype. It verifies Rust today; code in another language would need to be ported or call verified Rust through bindings. The project pages describe the workflow but do not provide a public PDD Kit download. Chopin has a separate public repository.

The published result is one login flow in one application. Microsoft has not presented a measured review-time reduction or a broader evaluation with this demonstration. GitHub Next's illustration of shorter review time is explicitly labelled illustrative, not measured.