微软研究院展示 PDD Kit 如何形式化验证智能体编写的 Web 应用

发生了什么

微软研究院介绍了 PDD Kit，这是一款研究原型，可将经过审阅的意图转化为 Verus 规范，并据此检查智能体编写的 Rust 代码，同时通过测试检查证明范围之外的行为。在一个约 5,000 行的 Pet Store 应用中，团队对登录逻辑进行了形式化验证，并测试了数据库查询和密码校验等可信组件。PDD Kit 目前仅验证 Rust，文章也说明了其可信假设和局限。

接下来读什么

• 今日还有哪些重要变化OpenAI 发布 Images 2.6，支持导出 SVG、生成 GIF，速度更快

这件事到目前为止

Microsoft Research introduced PDD Kit, a research prototype that checks agent-written Rust code against formal specifications; it currently verifies Rust because it uses Verus. The team used the kit on a roughly 5,000-line Pet Store app. It formally verified the login logic and used tests to check behavior outside the proof, including trusted components such as database lookups and password checking.