AI agents are writing more code. How can developers ensure that code is correct?

Microsoft Research’s Proof-Driven Development (PDD) Kit explores a more rigorous approach: it translates a developer’s intent into a formal specification, then uses formal verification to prove that generated code meets it.

PDD Kit works with Verus for Rust and is integrated with @GitHubNext’s Chopin, bringing formal methods into an AI-assisted development workflow for teams.

See the work in action at @github Universe, Oct. 28–29, 2026.