The Pulse
Microsoft Research Says It Used PDD Kit to Formally Verify Login Logic in a Rust Web App
Microsoft Research says it used PDD Kit to formally verify the login logic of Pet Store, a full-stack Rust web app. It says the kit turns plain-language requirements into formal specifications and tests, and marks which parts of the code re
AI.info Team · Written with AI · fact-checked ·
Microsoft Research described PDD Kit in a blog post published November 5, 2026, by Alex Lavaee and Matthai Philipose. The researchers say they used the toolkit inside GitHub Next’s Chopin to formally verify login logic in Pet Store, a Rust storefront. The full-stack app contains about 5,000 lines of Rust.
Login logic puts the kit to work
Pet Store’s backend uses Axum and SQLite and handles inventory, promotions, orders and checkout; its storefront is a Leptos app compiled to WebAssembly. The demonstration focuses on login, where the developer’s two-sentence request says users should get a token only with the right password and that only admin accounts should get admin tokens. The post says the developer reviewed the intent and never read the generated code line by line.
Microsoft Research describes the problem as a gap between a plan and an agent’s implementation: the agent can drift from the plan and write tests that pass for what it built, not what the developer requested. According to the post, PDD Kit runs as a partner inside Chopin, GitHub Next’s real-time, multiplayer planning environment, where teams and agents can plan in a shared document. It says the kit asks questions about the request and records the answers in an intent artifact linking the user’s intent to formal specifications or tests.
From plain-language intent to a Verus proof
According to the post, the kit converts the parts of the intent that can be formalized into formal specifications and turns the rest into informal specifications for tests. Before writing code, its planning workflow asks decision questions and explains relevant parts of the code. One question asks whether the right password must always produce a token: a rule that tokens require correct passwords would also permit a login that refuses everyone.
The developer chose to require both outcomes: a correct password gets a token, and an incorrect password does not. The post says PDD Kit then automatically generates proofs that the code meets the formal specifications, alongside tests for the informal specifications. Microsoft Research says a proof shows that code meets its specification for every input, while a passing test only shows the code worked on the inputs it tried.
PDD Kit draws a boundary around the proof
Microsoft Research says that, for PDD Kit today, the verifier is Verus, a proof language for Rust co-developed by Microsoft Research and researchers at several universities and research institutions. In the first draft of the plan, the login handler stayed trusted and tested, while the login decision logic was proved. The developer instead chose to give the handler its own async specification, so the proof would also cover the glue that awaits database lookups and signs the token.
That choice led to a new async function, login_flow, whose contract runs from the request’s fields to the token or the HTTP error. The post says the proof cannot see code in other crates, such as bcrypt hashing, sqlx queries or jsonwebtoken signing, and cannot establish outside facts such as what SQLite holds right now or what time the clock says. The post says PDD Kit spells out the trusted boundary, the part of the Trusted Computing Base, or TCB, that the proof leans on, and asks the developer to accept each trusted piece.
The developer signed off on six trusted pieces
For the login example, the developer signed off on six trusted pieces: the customer and admin account lookups, password checking, token generation, expiry calculation, database-error handling and the login handler shell. The lookup contracts say that each awaited, successful lookup returns exactly the row its own table holds for that email or username, or none; the password-checking contract says that Ok(true) means exactly the right password. The expiry wrapper’s contract is that the expiry is exactly 24 hours after the clock reading.
The post says PDD Kit writes a test for every assumed clause into the plan. It says PDD Kit recommends starting with the most sensitive parts of an application and verifying incrementally.