Microsoft's PDD Kit formally verifies agent-written full-stack apps with Verus
Microsoft Research · rss · 2026-11-06
Microsoft Research introduces Proof-Driven Development (PDD) Kit, bringing formal methods to everyday AI coding. The problem: a plan is supposed to be the contract with a coding agent, but nothing enforces it — agents drift and write tests that validate their own implementation, hiding the gap between intent and shipped code. PDD Kit runs inside GitHub Next's Chopin: it interviews you in plain language to build an intent artifact, formalizes what it can into Verus specs with machine-checked proofs covering every input, falls back to clearly-labeled empirical tests where proofs can't reach, and makes the Trusted Computing Base explicit for sign-off. Demo: from a two-sentence request it verified the login logic of Pet Store, a 5,000-line Rust full-stack app, uncovering existing bugs and proving absence of login flaws — with the developer never reading the code line by line. Recommendation: start with the most sensitive modules and verify incrementally.
More from coding & agent
- Gemini /teamwork agents caught live: four parallel task logs all running that second — RyanSpunk · 2026-11-13
- Codex CLI 0.168.0 adds model provider picker, side-by-side TUI workspace and animated GIF generation — github-actions[bot] · 2026-11-13
- Free MCP server lets Claude read Altium, Allegro, KiCad and Gerber PCB files directly — woodisruff · 2026-11-13
- a16z Partner Clones Open-Source Game with Fable 5.2 Agent, Which Finds Its Own Horse Animation Asset — FinanceYF5 · 2026-11-13
- OpenAI team shares how it runs and governs fleets of persistent agents internally — romainhuet · 2026-11-13
- Perplexity's Decider scanned 1B tokens across 7,000 agent sessions, found 14 security fixes — denisyarats · 2026-11-13