GitHub Next and Microsoft Research launch PDD Kit for verified AI-generated code

How do you _guarantee_ your agent's code is correct? You prove it. Introducing Proof Driven Development Kit (PDD Kit) from @MSFTResearch. PDD Kit helps turn your plan into a formal spec, then proves the agent's code meets that spec for every input. No vibe verification. PDD Kit is integrated with @GitHubNext's Chopin, so you can plan as a team. PDD Kit takes an app's login flow from intent to a verified pull request: It discusses your code, infers your intent as it goes, and proposes a formal spec in Verus, a proof language for Rust. Once you approve the spec, the Verus verifier automatically proves the code meets it. Where proof isn't possible, it falls back to empirical verification with tests and computer-use agents (CUAs). It works on Rust today. No new language, no change in how you produce the underlying code, making formal methods more accessible. The goal is a verified software factory, where engineers review specifications instead of code. Come see it in action at GitHub Universe, Oct 28–29. Swing by the Speakeasy and ask for GitHub Next!