Skip to content
Microsoft Research· Alex Lavaee, Matthai Philipose·· 4h agoSelected

Microsoft Research Releases PDD Kit to Formally Verify Agent-Written Full-Stack Web Apps

Original source: Microsoft ResearchRead original
AI brief

Microsoft Research introduces PDD Kit, a toolkit that turns developer intent into formal specifications in Verus and mechanically proves AI-generated code satisfies them for every input, falling back to tests where proofs cannot reach. The team verified the login logic of Pet Store, a roughly 5,000-line Rust full-stack web app, inside GitHub Next's Chopin environment, uncovering existing bugs without line-by-line code review.

Why it matters

PDD Kit tackles the review scalability problem of agent-generated code by combining Verus formal verification with empirical testing, offering a practical path toward trustworthy AI coding, though it remains a research prototype limited to Rust.

Explained
What
Formally verifying agent-written full-stack web apps with PDD Kit

Source: Microsoft Research · microsoft.com

AI Models & ApplicationsAI AgentsDeep Dives

Article discussion

Reader opinions are hosted on GitHub Discussions; posting requires a GitHub account. Comments are not verified facts.

Open GitHub Discussions