Microsoft Research· @MSFTResearch · X·· 5 天前AI 评分61
AI 导读
微软研究院推出 Proof-Driven Development (PDD) Kit，将开发者意图转化为形式化规约，并利用形式化验证来证明 AI 生成的代码符合该规约。PDD Kit 适用于 Rust 的 Verus，并与 GitHubNext 的 Chopin 集成，将形式化方法引入团队的 AI 辅助开发工作流中。
正文 · 原文
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.
来源：Microsoft Research · x.com