# Microsoft shows how PDD Kit formally verifies agent-written login code

> Original title: Formally verifying agent-written full-stack web apps with PDD Kit

- Source: Microsoft Research
- Published: 2026-11-05T16:00:00.000Z
- Bad Influence: https://badinfluence.news/items/teczye5mul2j0tkng8st0cssl
- Original: https://www.microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit/

## Summary

Microsoft Research describes PDD Kit, a toolkit that turns a developer's intent into a Verus formal specification, then proves that agent-written Rust code meets it for every input. The post demonstrates the method on the login logic of Pet Store, a full-stack Rust web app, where Verus uncovered existing bugs. Components that a proof cannot reach, such as the bcrypt password check and database lookups, are instead covered by tests and an explicitly accepted trust boundary.

## Why it matters

The post walks through a concrete login example, showing how an approved intent becomes a Verus spec and where the trusted boundary sits.