跳到正文
Microsoft Research 博客·· 3 小时前精选AI 评分86

Microsoft Research 发布 PDD Kit，用 Verus 形式化验证智能体编写的全栈 Web 应用

AI 导读

Microsoft Research 发布 PDD Kit 工具包，引入证明驱动开发（PDD）新范式，结合 GitHub Next 的 Chopin 环境与 Verus 形式化验证工具，将用户的自然语言意图转化为数学规范。该工具包通过自动生成代码证明和受信任的测试边界，在全栈 Rust 应用的登录逻辑验证中实现对每个输入的穷举式证明，从而减少对代码逐行审查的依赖。

推荐理由

微软发布 PDD Kit 将形式化验证引入智能体生成的代码，读者可以通过 Verus 和意图映射了解其如何摆脱对逐行代码审查的依赖。

正文 · AI 翻译
PDDKit decision flowchart on green gradient background

一目了然

  • 将形式化方法应用于日常软件。PDD Kit 帮你将意图转化为形式化规范，然后证明你的智能体为各种输入所编写的代码，并在无法进行证明的地方使用测试。它将形式化方法从利基的专家工作，推向没有形式化方法背景的工程师以及全栈 Web 应用等日常场景，正如这里所示的范例。
  • 随着 AI 智能体生成越来越多的代码，穷尽式的逐行人工审查将变得难以扩展。计划本应是你与编程智能体之间的契约，但实际上没有任何机制强迫智能体去遵守它。它所编写的测试通常检查的是它构建了什么，而不是你要求它做什么。 
  • PDD Kit 让智能体遵守计划。它与你协作，将你的意图转化为 Verus（在新标签页中打开） 中的形式化规范，证明智能体的代码对每种输入都符合该规范，并在无法进行证明的地方退回到测试。
  • 我们在一个全栈 Web 应用上进行了尝试。在 GitHub Next 的 Chopin（在新标签页中打开） 中，我们使用 PDD Kit 对 Rust（在新标签页中打开） 店面 Pet Store 的登录逻辑进行了形式化验证。Verus 强化了代码并发现了现有 Bug，证明了在规范方面不存在登录 Bug。开发者审查了意图，而无需逐行阅读生成的代码。 

计划本应是智能体应遵循的契约，但没有任何东西约束智能体去遵循它。

编程智能体现在经常一次性交付整个功能，往往跨越数万甚至数十万行代码。因此，阅读拉取请求（PR）的每一行代码已无法适应这种新的工作方式。现在，大多数团队转而投资于计划和相关的测试：向智能体描述他们想要什么，来回沟通直到计划和建议的测试看起来没问题，然后将它们交给智能体去实现。 

这个计划或自然语言规范本应是智能体所持有的契约。然而在实践中，智能体可能会偏离它。它实现了一些略有不同的东西，然后针对其实现而不是你期望它编写的代码编写能够通过的测试。持续集成（CI）由于大量低质量且高数量的测试而不断膨胀，覆盖率看起来很健康，而你要求的和实际交付的之间的差距一直被隐藏，直到 Bug 报告或棘手的边界情况出现。

那么，当智能体生成越来越多的代码时，如何可靠地扩展审查？智能体代码通常会以细心的审查者通常能捕获的两种方式失效：它遗漏了明显必要的东西，或者它做了明显错误的事情。单靠测试无法弥补这一差距，因为它们只测试了程序可能执行的一小部分。要弥补这一差距，需要一种不同类型的机制，这就是证明的用武之地。

焦点：活动系列

Research Forum | abstract background with colorful hexagons

微软研究论坛

加入我们，就通用 AI 时代的研究所进行持续的思想交流。随时点播观看最新剧集。

代码审查会问“这样对吗？”而形式化证明则能回答“这真的对吗？”数学证明可以证明代码对于所有输入都符合其规范，包括测试套件可能遗漏的那些输入。与单纯的测试相比，它能为指定的属性提供更强的保证，特别是在逐行审查不切实际的时候。

过去，对于日常软件而言，形式化证明的成本过高。你需要专门的人才、不熟悉的语言、比代码大好几倍的证明，而且开发这些证明往往需要数年时间。但自那以后，有两件事发生了变化。首先，近期编码代理（coding agents）的进展使得它们越来越切实可行地协助从定义明确的规范生成形式化证明。其次，代理现在能更好地帮助你编写形式化规范。我们将这种全新的软件开发范式称作证明驱动开发（Proof-Driven Development, PDD）。PDD Kit 就是我们为此打造的工具包。

PDD Kit 的工作原理

PDD Kit 之于形式化方法，大致相当于 Spec Kit（在新标签页打开）之于规范驱动开发（Spec-Driven Development）。它作为合作伙伴运行在 Chopin（在新标签页打开）中——这是 GitHub Next 的实时多人规划环境，团队和代理可以在一个共享文档中进行规划。

工作流分为两半（图 1）。首先，团队成员以通俗易懂的语言审查意图。PDD Kit 会提出仔细的审查者会问的问题，边走边解释相关的代码，并将答案记录在意图工件（intent artifact）中——这是一个连接用户意图与形式化规范或测试的文档。用户意图中可以形式化的部分被转化为形式化规范，其余必须信任的部分则被转化为用于测试的非形式化规范。PDD Kit 会自动生成代码满足所派生形式化规范的证明，以及针对非形式化规范的高质量测试。这一切都不需要你具备形式化方法的背景。 

Flow diagram showing the PDD Kit workflow for formally verifying agent-written code. Team members review intent by expressing requirements in plain language, which are formalized in a pdd-plan containing decision cards, intent artifacts, trusted boundaries, and reviewer approvals. The plan generates a formal specification with Verus ensures clauses. Machines then check the code through pdd-prove, which includes Verus proofs, tests for trusted components, and LLM gap review. Verified code and receipts are submitted as a pull request. Dashed feedback loops return specification contradictions and verification gaps to earlier planning and coding stages.
图 1：使用 PDD Kit 进行证明驱动开发。团队成员确定意图，Verus 和测试套件以此约束代码。

因此，PDD Kit 中的每一个结果都会指明它依赖的验证类型： 

  • 形式化验证（Formal verification）是对代码在所有可能输入下都满足其规范的数学证明，由称为验证器的工具进行检查。对于如今的 PDD Kit 而言，该验证器是 Verus（在新标签页打开），这是一种由微软研究院、卡耐基梅隆大学、VMware 研究院、苏黎世联邦理工学院、MPI-SWS、新南威尔士大学悉尼分校、德克萨斯大学奥斯汀分校、密歇根大学、英属哥伦比亚大学、威斯康星大学麦迪逊分校和魏茨曼科学研究所共同开发的 Rust 证明语言。
  • 经验验证（Empirical verification）通过运行代码并观察其行为来检查代码。它涵盖了证明触及不到的领域，例如第三方密码学库或用户界面。它使用单元测试和端到端测试、终端自动化、浏览器代理，以及针对浏览器无法驱动的任何内容的计算机操作代理。通过的测试只能表明代码在尝试过的输入上能够工作，因此 PDD Kit 将其标记为证据而非证明。

这两者之间的分界线就是可信计算基（Trusted Computing Base, TCB）：即证明假设其行为如描述的代码。PDD Kit 让这条界限变得明确，并要求你对每个部分进行签字确认。 

核心成果：一个全栈 Web 应用

为了展示 PDD Kit 如何与现有代码库集成，我们构建了 Pet Store，这是一个完全用 Rust（在新标签页中打开） 编写的全栈 Web 应用。后端使用 Axum（在新标签页中打开） 和 SQLite（在新标签页中打开），并处理库存、促销、订单和结账。前端是一个编译为 WebAssembly（在新标签页中打开） 的 Leptos（在新标签页中打开） 应用。两者加起来大约有 5,000 行 Rust 代码。

为了保持这篇博客的简炼，我们重点关注形式化验证应用的登录逻辑，但同样的过程可用于验证整个应用的功能正确性。PDD Kit 建议从应用中最敏感的部分开始，并逐步验证应用。一个登录漏洞可能会将客户的账户或管理员的控制权限交到攻击者手中，因此这正是证明工作最先带来回报的地方。开发人员在 Chopin 中的整个请求只有两句话：

Verify the login logic in backend/src/handlers/auth.rs. Here are my requirements:

  1. You only get a token with the right password.
  2. Only admin accounts get admin tokens.

我们故意让请求保持粗略。捕捉用户的意图并将用户请求转化为证明可以检查的内容，正是 PDD Kit 的工作。

第 1 步：代码编写前的提问

PDD Kit 的规划工作流 pdd-plan 会在编写任何代码之前读取代码，并在“决策”标签页中返回问题。当问题取决于代码的工作原理时，卡片会首先解释该部分：目标、各个部分如何组合以及涉及的具体函数，因此你无需打开源码即可回答。

Screenshot of a verification tool evaluating a login authentication requirement. The prompt asks, “Must the right password always get a token?” A flow diagram shows a login request leading to a password check, where matching passwords receive a token and non-matching passwords are refused. Option A, highlighted as recommended, proves both outcomes: the correct password receives a token and an incorrect password is refused. Option B proves only that incorrect passwords are refused, leaving the result for the correct password unspecified.
图 2. 第一张决策卡片。“只有使用正确的密码”本身也符合拒绝所有人的登录方式。双向证明排除了这种情况。

这个问题看起来有点迂腐，但它很重要。“你只有在密码正确时才能获得令牌”排除了错误情况（密码错误却获得了令牌），而拒绝所有人的登录则完美地兑现了这一承诺。“正确的密码总是有效”是排除前者的另一半。在形式上，第一个是蕴涵（令牌 ⇒ 正确密码），第二个是其逆命题。它们共同构成了“当且仅当”。无人看管的代理会在不告诉你 A 的情况下选择其中一个，但在这里，开发人员双向都进行了选择。

第 2 步：人类可读的意图映射

随着对话的进行，PDD Kit 会在计划顶部的“粗略工作”部分保持更新，以便用户能够跟踪重要的概念，而不必在漫长的聊天记录中往回滚动来查找达成一致的内容。它包括正在指定的登录流程图、将要证明的内容与将要信任的内容的规范全景图，以及在图片有帮助时的心理模型。对于登录，PDD Kit 绘制了一个售票台（图 3）。

Three-panel illustration comparing login outcomes. In the first panel, a customer logs in with the correct email and password and receives a “customer” ticket. In the second panel, the same email is paired with an incorrect password and access is refused. In the third panel, an administrator logs in with the correct username and password and receives an “admin” ticket. The diagram uses a ticket-counter analogy to explain authentication and role-based access.
图 3. PDD Kit 的登录心理模型。你发送的字段选择窗口，窗口选择表格及其角色，并且在密码匹配之前不会打印任何内容。

在其下方，“意图映射”将每个需求追溯到开发人员自己的话，并记录它是如何解决的（图 4）。每个条目都链接到对其实施建模的形式化规范部分以及涵盖它的测试，并且规范部分显示了 Verus 契约的代码片段，并带有注释，以便开发人员了解形式化规范如何对其意图进行建模。

Intent map showing the login authentication flow for issuing a token. If an account exists and bcrypt verifies the correct password, the user receives claims for that account. If the account does not exist or the password is incorrect, the result is “401 Unauthorized.” If the password hash cannot be read, the result is “500 unreadable hash.”
图 4. 决策后的意图映射条目：只有使用该账户的正确密码才能获得登录令牌，并且总是能获得。流程图显示了密码检查可能结束的每种方式。

图 2 中的决策卡片揭示了一种智能体通常会默默自行解决的歧义。图 5 展示了这种差异在纸面上看起来有多小：这两种解读在一个单元格上存在分歧，即一个未获得令牌的正确密码。

Side-by-side comparison of two authentication policies. The left panel, “Only when,” shows that a token implies the correct password but does not guarantee a token for a correct password. The right panel, “Exactly when,” shows a two-way relationship in which a token is issued if and only if the correct password is provided. The highlighted difference is that denying a token to a user with the correct password is allowed under the first policy but forbidden under the second.
图 5. 同一个句子的两种解读。它们在一个单元格上不同，而该单元格改变了证明必须确立的内容。

第三步：证明登录函数

在构建任何东西之前，PDD Kit 会要求团队对整个计划进行签字确认。它的初稿证明了登录核心处的决策（挑选表格并对密码进行门控），并将周围的处理程序保持在受信任且经过测试的状态。这是一个合理的默认设置，也是 PDD Kit 推荐的做法，但开发人员想要更多。处理程序是进行查找等待和对令牌进行签名的地方，而这种胶水代码恰恰是重构时可能悄悄调换两行代码的地方。因此，在意图审查时，开发人员选择为登录处理程序赋予其自己的异步规范，以便证明也涵盖该胶水代码，而不是去信任它（图 6）。

Comparison of two approaches to verifying a login handler. Option A, recommended, keeps the login handler trusted and verifies only the login decision logic, while database lookups and token signing remain tested but trusted components. Option B gives the login handler its own formal specification, proving the orchestration logic but requiring additional trusted wrappers and assumed contracts around database lookups, clocks, and JWT signing.
图 6. 证明更多的登录代码意味着信任更多的小型包装器。在开发人员做出选择之前，卡片就已经指出了这一点。 

这一选择将几乎所有东西都移入了证明中，只留下登录处理程序负责解包请求。一个新的异步函数 login_flow 承载了从请求字段一直到令牌或 HTTP 错误的契约。随后，PDD Kit 将修改后的计划带回来重新进行签字确认，因为符合你的意图并不等于证明，它也并不批准新的信任或更广泛的范围。 

第四步：证明停止的地方

关于程序，有很多东西是无法证明的，而登录过程会遇到其中的大部分：

  • 验证器无法看到的代码。bcrypt 的哈希、sqlx 的查询以及 jsonwebtoken 的签名存在于其他 crate 中，处于证明范围之外。 
  • 关于外部世界的客观事实。SQLite 此刻保存的内容以及时钟显示的时间是程序的输入，而不是其代码所能确定的。 
  • 某事是否会完成以及完成的速度有多快。该规范规定了如果登录有响应，你将得到什么。挂起的查询或缓慢的查询不会破坏其中的任何内容。 
  • 任何需要人工判断的事情，比如错误消息是否有帮助或屏幕显示是否合理。 
  • 任何没有人写下来的东西。证明只覆盖其规范，对规范之外的需求闭口不谈。 

这就是经验验证（empirical verification）发挥作用的地方。PDD Kit 明确了受信任的边界，即该证明所依赖的 TCB 部分。它将每个受信任的部分包装在一个具有假设契约的小型函数中，使用 Verus 的 #[verifier::external_body] 或 external_fn_specification，要求开发人员分别接受每一个部分，并将每个假设条款的测试写入计划中。对于登录功能，开发人员对六个部分进行了签字确认：

  • 两次查找：Customer::find_by_email 和 Admin::find_by_username。每次等待且成功的查找，都会准确返回其自身表格中为该电子邮箱或用户名所保存的行，或者不返回任何行。 
  • check_password 是围绕 bcrypt::verify 的薄包装器。它仅在 bcrypt 无法读取存储的哈希时报错，并且 Ok(true) 准确表示密码正确。 
  • generate_token 在配置的密钥下对给定的声明进行精确签名，并将签名失败报告为 500 错误。 
  • expiry_from_now 读取时钟并在整整 24 小时后写入过期时间。 
  • database_error 将失败的查找转换为带有 sqlx 消息的当前 500 错误。 
  • 登录处理程序外壳，它解包请求并将字段无修改地传递给 login_flow。 

在规范中，查找保持其代码原样，并从外部获取带有 external_fn_specification 的合约： 

/// Looks up a customer by exact email. 
/// Trusted, not proved: the SQL query runs in sqlx, which Verus cannot check. 
/// Every customer promise of `login_flow` rests on it. 
#[verifier::external_fn_specification] 
pub async fn ex_customer_find_by_email(pool: &sqlx::SqlitePool, email: &str) 
    -> (r: Result, sqlx::Error>) 
    ensures 
        // When the query succeeds, it returns the customers row on 
        // file for exactly this email, or None when there is none. 
        r matches Ok(found) ==> found == customer_on_file(email@), 
{ 
    Customer::find_by_email(pool, email).await 
} 

时钟是一个标记为 #[verifier::external_body] 的小型封装器。Verus 使用其 ensures 子句，从不读取函数体： 

/// Reads the clock and computes a token's expiry 24 hours ahead. 
/// Trusted, not proved: chrono's clock is outside the proof. 
/// It panics if the time is out of range, as today's login does; 
/// that panic is not promised against. 
#[verifier::external_body] 
pub fn expiry_from_now() -> (r: Expiry) 
    ensures 
        // The expiry is exactly 24 hours (86,400 seconds) after the clock reading. 
        r.exp as int == r.now as int + 86_400, 
{ 
    ... 
} 

图 7 将三层结合在了一起：Verus 证明的内容、人们接受且测试检查的内容，以及无人承诺的内容。 

Diagram showing the proof boundary for a formally verified login system. Functionality outside the proof is either not promised or trusted and validated through human review and testing, including SQLite lookups, bcrypt, the system clock, JWT signing, database error handling, and request parsing. At the center, the formally verified portion consists of the login_flow and its components login_core, lookup_target, decide_login, and issue_token, which are proven by Verus for every input.
图 7. 登录证明终止的位置。Verus 为每个输入证明了核心。人们接受受信任的环，测试对其进行检查。计划列出了无人承诺的内容。 

图 8 映射了被证明的内容和被信任的内容。每个信任决策都有其自己的卡片。它展示了 Verus 将盲目信任的子句、开发者所接受的内容，以及如果该假设错误将崩溃的承诺（图 9）。然后，每个假设的子句都会在计划的“经验验证”（Empirical verification）部分获得经验检查，在任何测试存在之前编写为 Given/When/Then 场景（图 10）。条目在运行之前显示为 planned（已计划），运行后则记录命令的结果与其运行针对的提交（commit）。

Proof map showing how a verified login system is divided between formally proved code and trusted, tested components. Five core functions, including login_flow, login_core, lookup_target, decide_login, and issue_token, are formally verified with Verus. Supporting functions for database queries, password verification, token signing, clock access, and error handling are treated as trusted contracts that are reviewed and tested.
图 8. 登录中被证明与被信任的内容。绿色函数由 Verus 针对每个输入进行证明。琥珀色部分是受信任的、由开发者接受的，并由计划第 4.1 节中的计划测试进行检查。
Proof map showing how a verified login system is divided between formally proved code and trusted, tested components. Five core functions, including login_flow, login_core, lookup_target, decide_login, and issue_token, are formally verified with Verus. Supporting functions for database queries, password verification, token signing, clock access, and error handling are treated as trusted contracts that are reviewed and tested.
图 9. 针对 check_password 的信任卡片。Verus 盲目信任这两个子句，因此人们接受它们，并且有两个测试对其进行检查。 
Screenshot of a test plan for verifying password validation behavior. The section, “check_password_answers_with_bcrypts_verdict,” describes unit tests confirming that password checks return true for the correct password and false for incorrect or empty passwords. Example test cases use bcrypt hashes for customer and administrator accounts.
图 10. 针对受信任的 check_password 的计划测试，在测试存在之前编写。计划将通过的测试标记为证据而非证明。 

该计划对于无人承诺的内容同样明确：登录未来是否会完成、超出范围的时钟是否不会 panic、关于尝试的时间或速率的任何内容，以及其他端点如何读取角色。 

第 5 步：读取规范

意图工件是团队审查的对象。它是 PDD Kit 编写为 Verus 合约的形式化规范的通俗语言版本。你可能在想，现在是否有人必须阅读证明而不是代码。没有人需要，因为编码代理会编写证明，而 Verus 会检查其中的每一步。如果 Verus 接受了证明，无论是否有人阅读，它都成立。规范是证明所依据的标准，所以这是人们审查的内容，而这个规范足够简短，只需几分钟就能学会阅读。每个函数都有一个 ensures 块：关于其结果 r 的语句，这些语句必须对每个可能的输入都成立。你在构建时 Verus 会检查它们，如果有任何子句甚至对一个输入失败，构建就会失败，并且 Verus 会指出该子句。每个子句读起来都像是一个 if-then，图 11 剖析了开发者第一个需求的子句。

Annotated code snippet explaining a formal verification clause for login tokens. The clause states that if a login returns a token, then the request names a valid account, the password matches the stored hash, the token contains valid claims, and the token’s subject and role match the authenticated account. Numbered callouts explain each part of the expression.
图 11. login_flow 上关于“你只能凭正确的密码获得令牌”的 ensures 子句。相同的账户 a 出现在每一行上，这把密码检查与令牌绑定在了一起。

请注意，每一行中都出现了相同的 a，它将密码检查与令牌绑定在一起。例如，设想这样一个漏洞：登录时用一个账户验证密码，却为另一个账户签发令牌。Bob 使用自己正确的密码登录，却返回了 Alice 账户的令牌。每一步单独看都没问题，但这个条款捕捉到了它，因为密码检查和令牌必须指向同一个账户。这就是测试套件极少会去寻找的那种连线漏洞。该规范还必须讨论 SQLite、bcrypt 和 JWT，而无需运行它们中的任何一个。它通过未解释函数来实现这一点，即没有方法体的名称：customer_on_file(email) 和 admin_on_file(username) 表示数据库保存的行，bcrypt_verdict(password, hash) 表示 bcrypt 的输出，token_claims(token, secret) 表示令牌携带的内容。Verus 对它们一无所知，除了第 4 步中受信任契约所承诺的内容。证明写着“无论数据库保存了什么，登录都能对其进行正确的处理”，而受信任契约则写着“查询返回数据库所保存的内容”。 

/// The customers row the database holds for 
/// exactly this email, if any, when login looks. 
/// Left abstract: only `Customer::find_by_email`'s 
/// trusted contract says what it is. 
pub uninterp spec fn customer_on_file(email: Seq) -> Option; 
... 
/// What bcrypt says about `password` against a 
/// stored `hash`: Some(true) when it is the password 
/// the hash was made from, Some(false) when it is 
/// not, None when bcrypt cannot read the hash. 
/// Left abstract: its meaning is bcrypt's, taken on trust through `check_password`. 
pub uninterp spec fn bcrypt_verdict(password: Seq, hash: Seq) 
    -> Option; 

 /// The password is the right one for the stored hash, by bcrypt's verdict. 
pub open spec fn password_matches(password: Seq

, hash: Seq) -> bool { 
    bcrypt_verdict(password, hash) == Some(true) 
} 

除此之外，named_account(email, username) 指明了登录指定的账户：如果发送了电子邮件，则是 customers 行中的电子邮件；否则是 admins 行中的用户名；否则为空。它的写法类似于 Rust，但它是一个数学定义，从不运行，仅出现在契约中。像这样的代码被称为幽灵代码（ghost code），因为验证器会检查它，而编译器会将其从程序中擦除。有了它，开发者的两句话需求最终变成了 login_flow 上的八个 ensures 子句（图 12）。 

/// The account a login names: the customers row for 
/// the email when one is sent (role "customer"), 
/// otherwise the admins row for the username (role "admin"), otherwise none. 
pub open spec fn named_account(email: Option, username: Option) 
    -> Option { 
    match email { 
        Some(e) => match customer_on_file(e@) { 
            Some(c) => Some(NamedAccount { 
                id: c.id@, password_hash: c.password_hash@, role: customer_role() }), 
            None => None, 
        }, 
        None => match username { 
            Some(u) => match admin_on_file(u@) { 
                Some(a) => Some(NamedAccount { 
                    id: a.id@, password_hash: a.password_hash@, role: admin_role() }), 
                None => None, 
            }, 
            None => None, 
        }, 
    } 
} 

Traceability diagram showing how formal verification promises are derived from requirements. Statements made by developers and decisions recorded in design cards are mapped to eight specific guarantees in the login_flow specification, covering token issuance, account roles, invalid credentials, missing accounts, malformed requests, and error handling.
图 12. 两句话的需求和“双向”决策最终变成了 login_flow 上的八个 ensures 子句。其中四个保留了现有的拒绝方式，因此店面和现有的 API 测试可以继续工作。 

以下是完整的契约，修剪掉了文档注释。每个子句上方都有意图工件向团队展示的通俗英语注释： 

/// The whole login, awaited end to end: from the 
/// request's fields to the token or the HTTP error. 
/// ... 
pub async fn login_flow(pool: &sqlx::SqlitePool, config: &Config, 
    email: Option, username: Option, password: &str) 
    -> (r: Result) 
    ensures 
        // Neither an email nor a username: 400 with today's message. 
        email is None && username is None 
            ==> (r matches Err(AppError::BadRequest(m)) 
                && m@ == missing_identity_text()), 
        // A token only for the account the login names, with its right 
        // password; it carries that account's id and its table's role. 
        r matches Ok(t) ==> (named_account(email, username) matches Some(a) 
            && password_matches(password@, a.password_hash) 
            && token_claims(t@, config.jwt_secret@) matches Some(c) 
            && c.sub@ == a.id && c.role@ == a.role), 
        // The right password for the named account always gets a 
        // token, unless a lookup or signing failure gives 500. 
        (named_account(email, username) matches Some(a) 
            && password_matches(password@, a.password_hash)) 
            ==> (r is Ok || r matches Err(AppError::Internal(_))), 
        // A login naming an account nobody holds gets 
        // 401, unless the lookup fails with 500. 
        ((email is Some || username is Some) && named_account(email, username) is None) 
            ==> (r matches Err(AppError::Unauthorized) 
                || r matches Err(AppError::Internal(_))), 
        // A wrong password for an account whose hash bcrypt 
        // can read gets 401, unless the lookup fails with 500. 
        (named_account(email, username) matches Some(a) 
            && bcrypt_verdict(password@, a.password_hash) == Some(false)) 
            ==> (r matches Err(AppError::Unauthorized) 
                || r matches Err(AppError::Internal(_))), 
        // An account whose stored hash bcrypt cannot read gets 500 and no token. 
        (named_account(email, username) matches Some(a) 
            && bcrypt_verdict(password@, a.password_hash) is None) 
            ==> r matches Err(AppError::Internal(_)), 
        // The admin role only for an admins row 
        // found by username, with no email sent. 
        (r matches Ok(t) && token_claims(t@, config.jwt_secret@) matches Some(c) 
            && c.role@ == admin_role()) 
            ==> (email is None && username matches Some(u) 
                && admin_on_file(u@) is Some), 
        // An email login's token always carries the customer role. 
        (r matches Ok(t) && email is Some) 
            ==> (token_claims(t@, config.jwt_secret@) matches Some(c) 
                && c.role@ == customer_role()), 
{ 
    unimplemented!() 
} 

受信任的边界也体现在代码中。check_password 是 Verus 不检查方法体的函数之一。它的契约将其与 bcrypt_verdict 绑定，后者是一个没有公理的 bcrypt 未解释模型：

/// Asks bcrypt whether `password` matches the stored `hash`. 
/// Trusted, not proved: Verus cannot check bcrypt's hashing, 
/// so this wrapper's contract is assumed. 
/// Every password promise of `login_flow` rests on it. 
#[verifier::external_body] 
pub fn check_password(password: &str, hash: &str) -> (r: Result) 
    ensures 
        // bcrypt answers (Ok) exactly when it can read the stored hash. 
        r is Ok <==> bcrypt_verdict(password@, hash@) is Some, 
        // Its answer is its verdict: true for the 
        // right password, false for any other. 
        r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b), 
{ 
    bcrypt::verify(password, hash).map_err(|e| e.to_string()) 
} 

它上方的文档注释说明了其基础所在：login_flow 的每一个密码承诺。每次登录最终都会落在少数几个地方之一，并且其中只有一处包含令牌（图 13）。该证明同时涵盖了所有这些情况。 

Flowchart showing the end-to-end login process. A login request selects an account table based on an email or username, looks up the account, verifies the password, and issues a signed token when authentication succeeds. Error paths return appropriate HTTP responses: 400 for missing credentials, 401 for invalid credentials or missing accounts, and 500 for lookup or password-hash failures.
图 13. 登录可能结束的所有方式，来自计划。 

login_flow 是异步的：它等待数据库查询。Verus 可以对异步函数施加契约，但有一条规则值得了解（图 14）。requires 在调用创建 future 时进行检查。ensures 描述了你 await 它时得到的值。没有任何东西承诺 future 一定会完成，因此挂起的查询不会破坏任何子句。 

login_flow 上的文档注释用同样的话说明了这一点： 

/// ... No promise the future completes. 
pub async fn login_flow(...) -> (r: Result) 

Diagram comparing how formal verification applies to synchronous and asynchronous functions. For both types, preconditions are checked when the function is called and postconditions are guaranteed when a result is returned. In an asynchronous login flow, the function may pause while awaiting a database lookup, and the specification makes no guarantee about whether or how quickly the operation completes.
图 14. 检查契约时，针对 sync fn 和 async fn。 

login_flow 保持简短，因为它是由经过验证的较小部件构建而成的。lookup_target 选择表。login_core 等待查询并调用密码关卡 decide_login。issue_token 签号令牌，或将拒绝映射到今天的 HTTP 错误。每个部件都有自己的契约，Verus 仅使用这些契约来证明 login_flow，而无需重新读取其方法体。更改 decide_login 的方法体，最终只需要重新证明 decide_login。 

以下是最小的完整部件，以及密码关卡的开始和结束： 

pub fn lookup_target(email: Option, username: Option) 
    -> (r: Result) 
    ensures 
        // An email, when sent, wins: customers are searched for exactly that email. 
        email matches Some(e) 
            ==> r == Ok::(LookupTarget::CustomerByEmail(e)), 
        // With no email, a username sends the search 
        // to admins for exactly that username. 
        email is None && username matches Some(u) 
            ==> r == Ok::(LookupTarget::AdminByUsername(u)), 
        // With neither, the login is refused for missing an identity. 
        email is None && username is None 
            ==> r == Err::(LoginError::MissingIdentity), 

pub fn decide_login(target: &LookupTarget, found: Option, password: &str) 
    -> (r: Result) 
    ensures 
        // No row found: refused as Unauthorized, 
        // the same answer as a wrong password. 
        found is None 
            ==> r == Err::(LoginError::Unauthorized), 
        // Claims come back only for a found row 
        // whose stored hash matches the password. 
        r is Ok ==> found is Some 
            && password_matches(password@, found->Some_0.password_hash@), 
        // The right password for a found row always gets claims. 
        found matches Some(a) && password_matches(password@, a.password_hash@) 
            ==> r is Ok, 
        ... 
        // An admins-table search gives the role text "admin". 
        r matches Ok(c) && target is AdminByUsername ==> c.role@ == admin_role(), 
        // A customers-table search gives the role text "customer". 
        r matches Ok(c) && target is CustomerByEmail ==> c.role@ == customer_role(), 

login.rs 概述 

图 15 绘制了整个规范文件的地图，verified/src/login.rs。它从上到下分为四个层级：标头、Verus 需要了解的导入和类型、对外部世界的抽象视图、将该视图连接到真实代码的可信契约，以及证明必须满足的五个契约。  

Annotated map of the verified/src/login.rs file showing the structure of a formally verified login implementation. The diagram categorizes sections as specification-only definitions, trusted external contracts, data types, and five functions formally proved with Verus: login_flow, login_core, issue_token, lookup_target, and decide_login.
图 15. login.rs 的组成部分，按文件顺序排列。灰色是标头和类型，紫色是仅出现在契约中的数学，琥珀色是可信的，绿色是已证明的。

以下是其中两个不太显眼的部分（经删节）。external_type_specification 引入了一个 Verus 未定义的类型。pool 保持不透明，而 customers 行保持其字段可见： 

/// The connection pool, opaque to the proof: only 
/// the lookups' contracts say what it returns. 
#[verifier::external_type_specification] 
#[verifier::external_body] 
#[verifier::reject_recursive_types(DB)] 
pub struct ExPool(sqlx::Pool); 
... 
/// A customers row, with its fields visible to the proof. 
#[verifier::external_type_specification] 
pub struct ExCustomer(Customer); 

并且 LoginError 将决策与 HTTP 响应分开，这使得 issue_token 能够将每次拒绝锚定到当天的状态码： 

/// Why a login gets no token. 
pub enum LoginError { 
    /// Neither an email nor a username was sent: 400 Bad Request. 
    MissingIdentity, 
    /// No such account, or the password does not match: 401 Unauthorized. 
    Unauthorized, 
    /// bcrypt could not read the stored hash, with its message: 500 Internal. 
    UnreadableHash(String), 
    /// The lookup query failed: 500 Internal, with sqlx's message. 
    Database(sqlx::Error), 
} 

在计划返回给你之前，两个审阅者 Agent 会从意图产物中找出衍生形式化规范的漏洞，以确保高质量的翻译，从而使规范符合你的要求，且不会作出超出证明能力范围的承诺。规范优化在后台运行并接受实时用户反馈，不断迭代，直到审阅者一致认为规范是健全的。 

步骤 6：证明、检查、填补空白 

开发者对规范的审阅到签署通过为止。此后的所有内容（实现和证明）都由机器检查，这就是为什么本文重点关注规范而非证明的原因。一旦开发者签署通过，构建计划阶段（图 16）就会将批准的计划交由 pdd-prove 处理，将其转换为小型任务图（图 16）。对于登录功能，一共有七个任务：让 login.rs 在后端 crate 内的 Verus 下构建，证明决策、令牌和整个流程，然后为可信包装器和端到端登录编写测试。 

Screenshot of a PDD Kit build plan for a login-token issuance specification. The build workflow contains seven tasks, with the first task focused on making verified/src/login.rs successfully build under Verus while preserving contract meanings. Subsequent tasks cover proving login-related functions, testing trusted wrappers, running end-to-end login tests, and validating token-signing behavior.
图 16. 构建计划将批准的规范转化为开发机器上的七项任务。第一项任务让 login.rs 在 Verus 下构建，而不改变任何契约所承诺的内容，并在需要时暂停询问，而不是削弱契约。 

每个任务都运行相同的循环： 

  • 编码 Agent 编写实现和证明，Verus 根据派生的形式化规范对其进行检查。 
  • 可信边界内的任何内容都会获得计划要求的测试。 
  • LLM 验证器并排读取计划、规范和结果，寻找漏洞：没有证明且没有通过检查的需求。漏洞会被送回给编码 Agent，直到不复存在。如果规范本身存在漏洞（例如两个相互矛盾的需求），它将作为决策返回给开发者。 

证明的好坏取决于其规范，因此 pdd-prove 也会检查规范。当模型编写自己的规范，或者经过微调以生成证明时，它往往会陷入弱不变量：即能够验证但几乎排除不了任何情况的子句。它们确实证明了某些东西，但很少证明你在乎的东西。我们称之为“氛围验证（vibe verification）”。这就是为什么确保你的意图与 Agent 保持一致如此重要，这也是 PDD Kit 的强项所在。 

该循环严格禁止更改目标。如果无法在固定的 Verus 中表达异步结构，任务将停止并询问团队，而不是切换到非异步助手或削弱契约。 

PDD Kit 是如何消除各类 Bug 的？变异检查（mutation check）是 PDD Kit 防范“氛围验证（vibe verification）”的机制。`pdd-prove` 会在代码的临时副本中，为每个 ensures 子句植入一个 Bug（例如拒绝所有用户，或在验证邮箱之前验证用户名），而 Verus 必须在目标子句上拒绝每一个变异体。能够通过的变异体意味着该子句没有任何约束力，它会被作为漏洞反馈回来。 

第 7 步：结合已验证的代码审查意图

当任务通过时，pdd-prove 会开启拉取请求。它们会添加一个带有 login_flow、其组成部分、其证明以及带有测试的受信任包装器的 verified/ crate，并通过 login_flow 路由真实的登录处理器，同时保留现有的 HTTP 状态码。你验证过的逻辑会集成并加固你的生产登录路径，而不是其副本。 

开发人员无需依赖对生成代码的逐行详尽审查即可进行合并。审查其实一直在意图工件（intent artifact）上进行，团队对此拥有最终决定权。我们将更多的审查重点从代码审查转移到了意图审查。拉取请求就像一张回执，其描述将每一项登录需求标记为形式化验证（formally verified）或经验性检查（empirically checked）。 

合并是证明融入团队常规工作流的环节。PDD Kit 的 `pdd-ship` 工作流将 Verus 检查与经验性测试一起加入到了 CI 中，因此以后无论是人还是代理对登录进行的任何更改，都必须继续针对同一规范进行证明，而损坏的证明会导致构建失败，就像测试失败一样。而且，由于证明覆盖了所有输入，PDD Kit 会剔除那些只重新检查已被证明的内容的测试（例如基于示例的密码关卡测试），并保留那些守护受信任边界的测试，从而使 CI 同时变得更强大、更精简。 

证明说了什么，没说什么 

“完全验证”很容易被夸大，因此以下是我们确切的声明。

  • 已证明。login_flow、login_core、lookup_target、decide_login 和 issue_token 的函数体针对所有输入都满足其契约。Login 会选择正确的表，将请求中的密码与所命名账户的存储哈希进行比较，签发带有该账户 ID 及其表所赋予角色的令牌，并对其他所有情况拒绝请求，返回现有的 400、401 或 500 且不带令牌。 
  • 受信任且经过测试。两次数据库查询、check_password （基于 bcrypt）、时钟、令牌签名、数据库错误消息以及处理器的请求解包都在证明之外，各自位于开发人员接受的假设契约之后。针对真实 bcrypt、真实 SQLite 模式和真实路由器的测试覆盖了这些部分。 
  • 已假设。Verus、Rust 编译器和 Z3（在新标签页中打开） 工具链，以及 Verus 的标准库 vstd（在新标签页中打开）。 

为什么选择 Rust 

PDD Kit 目前只验证 Rust，因为这是 Verus 支持的语言。如果你的代码库已经是 Rust，则无需迁移。其他语言的代码可以移植到 Rust 并针对相同的规范进行检查，非 Rust 项目可以通过绑定调用经过验证的 Rust 代码。 

还有一个不太明显的好处。一旦减少了对逐行详尽审查的依赖，可读性就不再是选择语言的主要原因。你可以为了速度和安全性选择某种语言，并尽情地进行优化，因为任何破坏规范的更改都会导致证明失败。 

对 PDD Kit 的期望

PDD Kit 是一个研究原型，目前它只验证 Rust，因为这是 Verus 支持的语言。其他语言的代码可以移植到 Rust 并针对相同的规范进行检查，非 Rust 项目可以通过绑定调用经过验证的 Rust。证明仍然需要付出切实的努力，主要在于证明本身的产出，而清晰的规范是减少这种努力的关键，这就是为什么 PDD Kit 的很大一部分工作在于首先搞对意图。我们将从漏洞代价最高的领域（如登录、支付或权限）开始，然后逐个部分地验证代码库的其余部分。

Pet Store 的登录是单个应用中的一部分：任何人都可以阅读的规范、证明代码与之匹配的 Verus 证明，以及针对证明所依赖的一切内容的测试。我们希望坦诚面对最薄弱的环节。这些保证的强度取决于六个受信任的部分，其中两个承担了大部分分量：针对每个密码承诺的 check_password，以及针对每个关于令牌指代哪个账户的承诺的两次查找。测试支持它们，但没有任何机制能证明它们。我们期望这个受信任的边界随着时间推移显著缩小，从而使越来越多的代码能够被形式化验证，我们希望探索这能扩展到多大程度。

我们真正改变的是人们审查的内容。团队不再主要依靠对智能体生成的代码进行逐行审查，而是用通俗的语言审查其意图，并通过证明来约束代码。这项计划本就应该成为契约，而现在智能体真的必须遵守它。

致谢

这项工作是 Microsoft Research Catalyst Lab、GitHub Next 与软件工程研究 (RiSE) 小组合作的成果。我们要感谢 GitHub Next 的 Maggie Appleton 和 Krzysztof Cieślak 在 Chopin 上的合作，感谢 Nikhil Swamy、Lef Ioannidis、Janardhan Kulkarni 和 Shuvendu Lahiri 对形式化验证和意图形式化提出的反馈与讨论。我们还要感谢 F*/Pulse 和 Verus 团队提供的支持。最后，感谢 GitHub Next 的 Idan Gazit 对此次合作的支持。

常见问题解答

  • 是的，确实如此。证明表明代码符合规范，而不是说规范就是你的本意。这就是为什么 PDD Kit 建立在现有的意图形式化研究基础之上。pdd-plan 工作流会读取你的代码，在编写任何内容之前提出问题，并将你的回答转化为 Verus 规范加上你批准的通俗语言计划，它会标记出模棱两可之处而不是盲目猜测。两个评审智能体会检查该规范，而 pdd-prove 工作流则会为每个条款植入一个漏洞，以捕捉那些通过了验证却什么也没有排除的条款。错误的规范仍然是有可能的，这就是为什么 PDD Kit 强调明确需求、识别模糊不清之处，并让开发人员在验证开始前参与审查和批准规范。 

  • 区别在于是什么在约束代码遵循计划。

    方法什么来检查代码
    规范驱动开发没有任何机制强制执行规范
    测试驱动开发针对输入样本的测试，通常编写为与构建内容相匹配 
    智能体检查自己的工作编写代码的同一个模型
    证明驱动开发Verus 自动验证证明，确保你的代码满足你所批准的规范

    PDD 保留了 SDD 的规划循环，并且在证明无法触及的地方仍然使用测试。测试检查某些输入，而证明则在既定假设下，确立代码对形式模型所涵盖的所有输入都满足指定的属性。 

  • 该证明是使用 Verus 结构注释的 Rust 代码，由 Verus 借助 Z3 求解器进行机械化检查。它可以在你的 Rust 构建所在的任何地方运行：pdd-prove 工作流在证明时运行它，而 pdd-ship 工作流则将其加入到你的构建和 CI 中，以便失效的证明会导致构建失败。该检查是确定性的，不涉及任何模型。模型编写规范、代码和证明，但只有确定性的 Verus 运行才能决定它是否通过。检查所需的时间取决于代码的大小和证明的难度：小型模块通常需要几秒钟，较大的代码库则最多需要几分钟。

  • PDD Kit 将更多审查流程转移到验证代码应该做什么上，同时利用形式化验证来提供额外的保证，确保实现满足这些要求。开发人员审查自然语言计划、形式化规范以及超出证明范围的受信任组件。由此产生的拉取请求（pull request）记录了经过形式化验证的内容、经过测试的内容以及可能需要进行额外审查的地方。在 Pet Store 全栈 Web 应用程序中，这种方法减少了对生成的代码进行详尽的逐行审查的依赖。

  • 我们选择 Verus 是因为它允许我们直接验证 Rust 代码，这与 PDD Kit 专注于将形式化验证集成到现有 Rust 开发工作流中的理念不谋而合。 其他证明语言（例如 Lean、F*、Rocq）采用不同的形式化验证方法，每种方法都有其自身的权衡。PDD Kit 背后的技术也可以帮助将它们投入使用。

来源：Microsoft Research 博客 · microsoft.com

Microsoft / Copilot开源生态产品更新#产品更新#开源生态#Microsoft