Microsoft Research proved an AI-written login correct for every input. What it could not prove is the lesson
PDD Kit turns a developer's request into a formal specification, has agents write code and proofs, and labels what remains tested but unproved. A research prototype with a useful habit.
Listen to this article · 4 min
AI-generated narration of the full article.
A developer asks for something simple: users log in with a password and get a token that expires after a day. Two sentences. In Microsoft Research’s new experiment, those two sentences became eight formal conditions that the login code must satisfy for every possible input, and an AI agent wrote both the code and the mathematical proof that it does.
The project is called PDD Kit, from Microsoft Research’s Catalyst Lab, GitHub Next and the RiSE group. It is a research prototype, and the authors say so. It is still the clearest picture so far of what checking AI-written code could look like when tests are not enough.
How it works
PDD Kit uses Verus, a verification tool for Rust. The team demonstrated it on Pet Store, a full-stack Rust storefront of about 5,000 lines inside GitHub Next’s Chopin project, and focused on the login logic.
- Plan
- Specify
- Stress the spec
- Prove
- Ship
Two design choices stand out.
The mutation check addresses a problem the authors call vibe verification: a specification so weak that almost any code satisfies it. By planting one bug for each condition and confirming that the proof then fails, PDD Kit tests the specification itself.
The trusted boundary is explicit. Some pieces cannot be proved and are marked as trusted, and the developer signs off on each one. For the login flow there were six. Passing tests are labeled evidence, not proof.
The honest part
The authors list what PDD Kit cannot prove, and the list is the most useful thing in the post for anyone running AI-generated code in production:
- third-party libraries, such as the bcrypt, sqlx and jsonwebtoken crates;
- facts about the outside world, such as what is in the SQLite database or what the clock says;
- whether an operation finishes, or how long it takes; an asynchronous query that hangs breaks no condition;
- requirements nobody wrote down.
They also say that the password check and two lookups, the pieces carrying most of the security weight, are tested but not proved. And proofs still take real effort, mostly in producing the proof itself. Today it works only for Rust.
What to take from a prototype
Few enterprises will run Verus on their order management system next year. But the habit PDD Kit enforces is transferable now, and it addresses the problem we described in verification capacity becoming the bottleneck: agents make code cheap, and checking it is not.
Write the intent down before the code. The two-sentence request turned into eight conditions because an agent asked questions. Most AI coding sessions skip that step, and the reviewer later has to guess what the code was supposed to do.
Test the tests. Mutation testing is decades old and rarely used. If agents write both code and tests, a check that the tests can actually fail is the cheapest protection against tests that prove nothing.
Keep a trusted list. For every AI-written component, record what was proved, what was tested and what is simply trusted, with a person’s name next to each trusted item. That is what proof from outside the model looks like in a code review: not certainty, but a clear account of where certainty ends.