AREX Feed Article
微软研究院发布 Proof-Driven Development Kit 技术拆解：把自然语言意图变成 Verus 规格，用数学证明校验智能体代码
11 月 5 日 16:00（UTC，北京时间 11 月 6 日零点），微软研究院在发布长文《Formally verifying agent-written full-stack web apps with PDD Kit》（用 PDD Kit 形式化验证智能体编写的全栈 Web 应用）；18:36 UTC，介绍 Proof-Driven Development Kit（PDD Kit）：一套把开发者的自然语言意图转成 Verus 形式化规格、再用数学证明校验 AI 智能体所写代码的研究原型工具，将传统上用于安全关键系统的形式化方法带进日常开发；证明覆盖不到之处会被明确标出，交由测试检验。帖文称，其结果是“更可靠的 agentic 代码”。
这套工具 10 月 21 日已由 和的官方账号介绍过，并预告在 10 月 28～29 日的 GitHub Universe 上演示。11 月 5 日的博客给出端到端的实测走查：在一个约 5,000 行 Rust 代码的全栈 Web 应用 Pet Store 中，开发者只用两句话提出登录要求，PDD Kit 把它落成 8 条 Verus 数学条款，带证明的登录代码随后完成合并，开发者审查的一直是意图文档，没有逐行读过智能体生成的代码。这些能力与效果均出自微软研究院与 GitHub Next 的自述，博客与帖文未附第三方评测。
计划是合同，但没人强制智能体照做
博客把背景写得很具体：编码智能体现在一次交付整个功能，代码量常达数万乃至数十万行，逐行读完整个 pull request（代码合并请求）已经不现实；多数团队把功夫转向计划与测试——向智能体描述要什么，来回改到计划和测试看起来没问题，再交给它实现。但这份计划只是应然的合同：智能体会悄悄偏离，实现成稍有出入的东西，再写出对自己的实现通过的测试；持续集成（CI）里堆积大量低质量测试，覆盖率看着健康，你要的和实际交付的之间的差距一直藏着，直到 bug 报告或刁钻的边界情况出现。
帖文把这个问题称作“信任问题”：AI 智能体生成代码的规模超出人类逐行审查能力，难以确保代码符合开发者意图，最终产出容易暴露于 bug 与安全风险。博客把智能体代码的典型失败归成两类，都是细心的审查者通常能抓到的：漏掉明显必需的东西，或者做了明显错误的事；测试补不上这个缺口，因为它们只踩到程序全部行为的一小片。微软研究院在 FAQ 里给现有方法排了座次：
| 方法 | 什么在检查代码 |
|---|---|
| Spec-Driven Development | 没有任何东西强制规格 |
| Test-Driven Development | 对抽样输入跑测试，测试往往照着已实现的东西写 |
| 让智能体自查代码 | 写代码的同一个模型 |
| Proof-Driven Development | Verus 机械验证代码满足你批准的规格 |
博客里有一句对照：审查问“这看起来对吗”，证明回答“这是不是对的”。数学证明说明代码对每一个输入都满足规格，包括测试套件漏掉的那些输入。
pdd-plan：写代码前先提问，一个短语钉成两种读法
微软把这套范式命名为 Proof-Driven Development（证明驱动开发），PDD Kit 是它的工具箱。博客解释了它为什么此刻才可行：证明过去太贵——需要专家、不熟悉的语言、比代码大许多倍的证明、以年计的开发周期；变化有两条，编码智能体已经能从定义清晰的规格出发帮助生成形式化证明，也能更好地帮人写规格。博客的定位是：PDD Kit 之于形式化方法，大约相当于 Spec Kit 之于规格驱动开发；它作为规划伙伴运行在 GitHub Next 的实时多人规划环境 Chopin 里，团队和智能体在同一份共享文档中规划。
工作流分两半。前一半 pdd-plan 管意图：它先读代码，在写任何东西之前把问题摆进 Decisions 选项卡；当问题依赖代码的工作方式，卡片会先解释那部分——目标、各块怎么拼、涉及哪个函数——让人不开源码就能回答。回答记进 intent artifact（意图文档），这份文档连接用户意图与形式化规格或测试：能形式化的部分转成形式化规格，必须靠信任的其余部分转成给测试用的非正式规格。博客强调，全程不需要形式化方法背景。
第一张决策卡就卡在一个短语上。开发者的原话是“只有密码正确才给你 token”，pdd-plan 追问：正确的密码是否必须总能拿到 token？按博客的解释，“只有密码正确才发 token”同样会被一个拒绝所有人的登录完美满足；要排除它，得补上“正确密码总是有效”这半句——前者是蕴涵（token ⇒ 密码正确），后者是它的逆命题，两个都证明才构成“当且仅当”。博客说，单干的智能体会自己挑一个而不告诉你；这次开发者选了“两个方向都证明”。
意图本身也有一张人能读的地图。pdd-plan 在计划顶部维护一块 rough work（草稿）区，含登录流程图、将被证明与将被信任的规格全景，以及一个“检票口”式的示意模型；intent map（意图地图）把每条需求连回开发者的原话，记录敲定过程，并链接到对应的 Verus 契约片段和测试。计划拿去签核前，两个审查智能体（reviewer agent）会从 intent artifact 出发挑刺，迭代到认定规格可靠为止；规格自身若有矛盾——比如两条需求互相冲突——则作为决策退回开发者。
pdd-prove：确定性证明加上防“vibe verification”的突变测试
签核之后，人的审查就结束了：博客写明，此后的实现与证明全部由机器检查。pdd-prove 把批准的计划转成任务图——Pet Store 登录对应七个任务——每个任务跑同一个循环：编码智能体写实现和证明，Verus 对照派生的规格检查；可信边界内的组件补齐计划要求的测试；一个充当校验器的大模型（LLM verifier）并排读计划、规格与结果，专找既没有证明、也没有通过的检查的缺口，缺口退回编码智能体直到清零。
博客点明，证明好不好取决于规格本身，所以 pdd-prove 连规格也查。模型自己写规格、或被调教去产出证明时，容易落在弱不变量上——博客管这叫“vibe verification”：条款能通过验证，却几乎不排除任何东西；它证明了点什么，只是很少是你关心的那件事。对策是突变检查（mutation check）：pdd-prove 在代码的临时副本里为每条 ensures 条款植入一个 bug——比如拒绝所有人、或者先查用户名再查邮箱——Verus 必须在对应条款上拒绝每个突变体；有突变体漏网，说明那条条款什么都没约束，作为缺口退回。
证明本身是带 Verus 注记的 Rust 代码，由 Verus 调 Z3 求解器机械检查。FAQ 写明：检查是确定性的、不含任何模型——模型写规格、代码和证明，但只有确定性的 Verus 运行决定通过与否；小模块通常几秒，大代码库可达数分钟。Verus 由微软研究院、卡内基梅隆大学、VMware Research、ETH Zurich 等 11 家机构共同开发，是一种面向 Rust 的证明语言。
每个结果都标注它靠哪种验证站得住。形式验证是数学证明，对每个可能输入成立；经验验证靠运行观察，覆盖证明够不到的地方——第三方加密库、用户界面等——用单元与端到端测试、终端自动化、浏览器智能体和 computer-use agents（直接操作电脑的智能体）。通过的测试只说明试过的输入没问题，所以 PDD Kit 把它标成证据而非证明。两类验证的分界线是可信计算基（Trusted Computing Base，TCB），即证明假定其行为如描述的那部分代码；PDD Kit 把这条线显式画出，请开发者逐项签核。
Pet Store 实测：登录逻辑如何被证明
实测对象 Pet Store 是为演示接入既有代码库而建的全栈 Rust 应用：后端用 Axum 和 SQLite，处理库存、促销、订单与结账；店面是编译成 WebAssembly 的 Leptos 应用。博客建议从最敏感的部分开始增量验证——一个登录 bug 能把客户账户或管理员权限交到攻击者手里——于是验证对象选了登录。开发者在 Chopin 里的全部请求是两句话：“验证 backend/src/handlers/auth.rs 的登录逻辑。我的要求：1. 只有密码正确才给你 token；2. 只有管理员账户拿 admin token。”请求故意写得粗糙——把意图捕捉出来、变成证明能查的东西，本来就是 PDD Kit 的活。
PDD Kit 默认只证明登录核心的决策——选表和密码门——把外围 handler 留在受信测试区。开发者选了更大范围：handler 正是查找被 await（等待返回）、token 被签名的胶水代码，重构时悄悄换错两行的就是这里，于是登录 handler 拿到自己的异步（async）规格，证明覆盖它。代价写在决策卡上：证明更多登录，就要信任更多小包装函数。改过的计划被重新送回签核——按博客的说法，“符合你的意图”本身不是证明，也不能顺带批准新的信任或更大的范围。
整份登录规格最终落在 login_flow 上，共 8 条 ensures 条款，其中 4 条保留今天的拒绝行为，店面与既有 API 测试照常工作。规格用无解释函数（uninterpreted function）谈论它并不运行的 SQLite、bcrypt 和 JWT——customer_on_file(email) 表示数据库中该邮箱对应的行，bcrypt_verdict(password, hash) 表示 bcrypt 的判定，token_claims(token, secret) 表示 token 里带什么——这些名字除受信契约承诺的内容外别无含义；连着它们的还有 ghost code，即验证器检查、但编译器会从程序里擦除的代码。
开发者逐一签核了六个受信组件：两个数据库查找（Customer::find_by_email 与 Admin::find_by_username）、bcrypt::verify 之上的薄包装 check_password、按配置密钥签发给定 claims 的 generate_token、读时钟并把过期时间定为 24 小时后的 expiry_from_now、把查找失败转成今日 500 的 database_error，以及原样把请求字段递给 login_flow 的 handler 外壳。
博客举了条款能抓住、测试套件很少想到去找的接线 bug：登录用一个账户校验密码、却给另一个账户签 token——Bob 用自己的正确密码登录，拿回的是 Alice 账户的 token。每一步单看都对，但规格要求密码检查和 token 指向同一个账户。
证明够不到的地方也在登录这里集中出现：bcrypt 哈希、sqlx 查询、jsonwebtoken 签名住在别的 crate（Rust 代码包）里，验证器看不见；SQLite 当前有什么、时钟几点，是程序的外部输入；规格说登录应答时你会得到什么，不承诺它完成或不挂起——挂起的查询不违反任何条款；也不承诺尝试频率、其他端点怎么读角色。
结果按博客口径：Verus 强化了代码并找出了既有的 bug，就规格而言证明了登录 bug 不存在。pdd-prove 开出的 PR 把真实登录 handler 接到 login_flow，保留既有 HTTP 状态码——验证逻辑加固的是生产登录路径而非它的副本；PR 描述逐条标注登录要求靠形式验证还是靠经验检验成立，充当收据。合并后，pdd-ship 把 Verus 检查放进 CI：此后任何对登录的改动，无论来自人还是智能体，都得继续通过同一规格的证明，证明坏了和测试失败一样挂掉构建；只重复已证明行为的测试（比如密码门的示例测试）被删掉，看守受信边界的测试保留，博客说 CI 因此更强也更精简。
证明的边界：哪些被证明，哪些被信任，哪些被假定
“Fully verified”容易被夸大，博客专列一节交代证明说了什么、没说什么：
- 已证明：login_flow、login_core、lookup_target、decide_login、issue_token 五个函数的主体对每个输入满足契约——登录选对表、把请求密码与所指账户的存储哈希比对、签发带该账户 id 及其表角色的 token，其余一律按今天的 400、401、500 拒绝且不发 token。
- 受信且有测试：那六个受信组件都在证明之外，各自背后是开发者接受的假定契约，由针对真实 bcrypt、真实 SQLite schema 和真实路由的测试覆盖。
- 假定：Verus、Rust 编译器、Z3 工具链与 Verus 标准库 vstd。
工具本身的边界也写在明面上：PDD Kit 是研究原型，目前只能验证 Rust——Verus 只做 Rust；其他语言可以移植到 Rust 后对照同一规格检查，非 Rust 项目也能通过绑定调用已验证的 Rust。证明仍然费工，博客说费力处主要在产出证明本身，清晰的规格能把成本压下来；建议从 bug 代价最高的地方开始——登录、支付、权限——一片一片验证代码库。
这套工具的亮相分两波。10 月 21 日，GitHub Next 的介绍帖截至 11 月 6 日查询获得 2,054 个点赞、约 39.7 万次浏览；同日的帖子标注 PDD Kit 为“研究预览（research preview）”，获得 603 个点赞。GitHub Next 的已经上线，收录同一套流程与示例；介绍帖还给出它的目标——“一个经过验证的软件工厂（verified software factory），工程师审查规格而不是代码”。11 月 5 日的拆解帖截至 11 月 6 日查询有 52 个点赞、11 次转发。博客致谢部分写明，这项工作是 Microsoft Research Catalyst Lab、GitHub Next 与 Research in Software Engineering（RiSE）小组的合作；帖文点名研究员 Matthai Philipose（）与 Alex Lavaee（）拆解了 Proof-Driven Development。
至于最弱环节，博客说得直白：这套保证的强度取决于六个受信组件，其中两个承担大部分重量——check_password 背着所有密码承诺，两个数据库查找背着所有“token 指向哪个账户”的承诺；测试支持它们，但没有任何东西证明它们。团队预计这条受信边界会随时间显著缩小，并想弄清这条路能扩展到多远。