跳到正文
Microsoft Research· Alex Lavaee, Matthai Philipose·· 5 小时前AI 评分56

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

Formally verifying agent-written full-stack web apps with PDD Kit

AI 导读

Microsoft Research 发布 Proof-Driven Development（PDD）工具包 PDD Kit，将开发者的意图转为 Verus 形式化规约，自动证明 Agent 编写的 Rust 代码对所有输入满足规约，证明无法覆盖处回退到测试。

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

一览

  • 面向日常软件的形式化方法。PDD Kit 帮助你把意图转化为形式化规约，然后针对所有输入证明你的智能体所写代码的正确性，在证明无法覆盖之处再用测试。它让形式化方法从小众的专业工作走向没有形式化方法背景的工程师，走向日常应用，例如此处展示的全栈 Web 应用。
  • 随着 AI 智能体生成越来越大量的代码，逐行穷尽式的人工审查会变得难以扩展。计划本应是你与编码智能体之间的契约，但实际上没有任何东西强制智能体遵守它。智能体编写的测试通常检查的是它构建的东西，而不是你要求的东西。 
  • PDD Kit 让智能体遵守计划。它与你协作，把你的意图转化为 Verus（在新标签页中打开） 中的形式化规约，证明智能体的代码在所有输入下都满足该规约，并在证明无法覆盖之处退回到测试。
  • 我们在一个全栈 Web 应用上进行了尝试。在 GitHub Next 的 Chopin（在新标签页中打开） 中，我们使用 PDD Kit 对 Pet Store（一个 Rust（在新标签页中打开） 店面应用）的登录逻辑进行了形式化验证。Verus 加固了代码并发现了已有缺陷，证明了登录逻辑相对于该规约不存在缺陷。开发者只需审查意图，从未逐行阅读生成的代码。 

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

如今，编码智能体一次性交付完整功能，往往横跨数万甚至数十万行代码。因此，逐行阅读拉取请求的方式已无法适应这种新的工作方式。现在，大多数团队转而投入于计划和相关测试：向智能体描述他们想要什么，反复沟通直到计划和拟定的测试看起来无误，然后交由智能体实现。 

这份计划或自然语言规约本应是智能体遵守的契约。然而在实践中，智能体可能会偏离它。它实现的东西略有不同，然后编写针对其实现而非你本意所需代码的测试。持续集成（CI）因大量低质量测试而膨胀，覆盖率看起来很健康，而你要求的与实际交付之间的差距一直被隐藏，直到缺陷报告或棘手的边缘情况出现。

那么，随着智能体生成越来越大量的代码，如何可靠地扩展审查？智能体代码有两种细心的审查者通常能发现的问题：遗漏了明显必要的内容，或做了明显错误的事情。单靠测试无法弥合这一差距，因为测试只能覆盖程序能力中极小的一部分。弥合它需要另一种机制，这正是证明的用武之地。

播客系列

Illustration of Doug Burger

未来之形

与 Microsoft 的 Doug Burger 及各位嘉宾一起，深入探讨关于 AI 的基本真相，以及它将如何重塑未来。

评审问的是“这看起来对吗？”而证明回答的是“这是对的吗？”数学证明表明代码对于每一个输入都符合其规范，包括你的测试套件可能遗漏的那些输入。对于已声明的属性，这比单纯测试提供了更强的保障，尤其是在逐行评审不太现实的情况下。

过去，证明对于日常软件来说成本太高。你需要专家、不熟悉的语言、比代码大许多倍的证明，而且证明的开发需要数年时间。但从那以后，两件事发生了变化。首先，编程智能体的最新进展使它们能够在明确定义的规范基础上协助生成形式化证明，这变得越来越可行。其次，智能体现在能更好地帮你编写形式化规范。我们将这种新的软件开发范式称为证明驱动开发（Proof-Driven Development，PDD）。PDD Kit 就是我们为此打造的工具包。

PDD Kit 的工作原理

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

工作流程分为两半（图 1）。首先，团队成员以自然语言评审意图。PDD Kit 会提出一位细致的评审者会问的问题，在此过程中解释相关代码，并将答案记录在一个意图工件中——这是一份连接用户意图与形式化规范或测试的文档。用户意图中可以形式化的部分会被转换为形式化规范，而其余必须凭信任接受的部分则转换为用于测试的非形式化规范。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 中的每一个结果都会说明它依赖于哪种验证方式： 

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

两者的分界线是可信计算基（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 的职责。

第一步：写代码之前先提问

PDD Kit 的规划工作流 pdd-plan 会读取代码，并在编写任何内容之前，在决策（Decisions）标签页中提出问题。当问题依赖于代码的工作方式时，卡片会先解释那部分内容：目标、各部分如何配合，以及涉及的具体函数，这样你无需打开源代码就能回答。 

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. 第一张决策卡片。仅凭“只有输入正确密码才行”这一条，也会被一个拒绝所有登录的系统满足。双向证明可以排除这种情况。

这个问题看起来迂腐，但其实很重要。“只有密码正确才能获得令牌”排除的是坏情况——错误密码获得令牌，而拒绝所有登录的系统则完美遵守这一承诺。“正确密码总是有效”是排除上述情况的另一半。形式化地说，第一个是蕴含（token ⇒ 密码正确），第二个是其逆命题。两者合在一起构成“当且仅当”。智能体独自工作时会在不告知你的情况下只选其一，但在这里，开发者选择了双向都验证。

第二步：人类可读的意图图谱

随着对话的进行，PDD Kit 会在计划顶部持续更新一个草稿区（rough work），让用户可以跟踪重要概念，而不必在长篇对话中来回滚动查找已达成的内容。它包括正在指定的登录流程的流程图、一份说明哪些内容将被证明、哪些内容将被信任的规格全景图，以及在图示有帮助时的一个心智模型。对于登录，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. 同一句话的两种读法。它们只在一个单元格上不同，而这个单元格改变了证明需要确立的内容。

第 3 步：证明登录函数

在任何东西被构建之前，PDD Kit 会要求团队对整个方案签字确认。它的初稿只证明了登录核心处的决策——选定表并用密码做门控——而保持其周围的处理程序受信任且经过测试。这是一个合理的默认选择，也是 PDD Kit 推荐的方案，但开发者想要更多。处理程序正是等待查询结果并签署令牌的地方，而这种胶水代码恰恰是重构时可能悄悄调换两行代码之处。因此在意图评审时，开发者选择为登录处理程序单独编写一个 async 规约，让证明覆盖这段胶水代码，而不是信任它（图 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. 证明登录的更多部分意味着信任更多的小包装函数。卡片会在开发者做出选择之前说明这一点。 

这个选择把几乎所有内容都移入了证明，留给登录处理程序的只剩下解包请求。一个新的 async 函数 login_flow 承载了从请求字段一直到令牌或 HTTP 错误的契约。随后 PDD Kit 把修订后的方案带回，重新进行签字确认，因为符合你的意图并不等于证明，它也不会自动批准新的信任或更大的范围。 

第 4 步：证明的边界

关于一个程序，有很多东西是没法证明的，而登录几乎撞上了其中的大部分：

  • 验证器看不到的代码。bcrypt 的哈希、sqlx 的查询和 jsonwebtoken 的签名都位于其他 crate 中，在证明之外。 
  • 关于外部世界的事实。SQLite 当前保存的内容和时钟指示的时间都是程序的输入，不是它的代码能够确立的东西。 
  • 某件事是否完成、多快完成。规约只说明如果 login 给出回答你会得到什么。一个挂起的查询，或一个缓慢的查询，都不会破坏它。 
  • 任何需要人来判断的东西，比如一条错误信息是否有帮助、一个界面是否合理。 
  • 任何没人写下来的东西。证明只覆盖其规约，对规约之外的需求不做任何说明。 

这就是经验验证发挥作用的地方。PDD Kit 明确列出受信任边界，也就是这个证明所依赖的 TCB 部分。它把每个受信任的部分包装在一个带假定契约的小函数里，使用 Verus 的 #[verifier::external_body] 或 external_fn_specification，要求开发者逐一接受它们，并为每个假定的条款在方案中写入测试。对于 login，开发者签字确认了六个部分：

  • 两个查询，Customer::find_by_email 和 Admin::find_by_username。每个被 await 且成功的查询都精确返回其对应表中该 email 或 username 的那一行，或者不返回任何行。 
  • check_password，围绕 bcrypt::verify 的一个薄包装。它只在 bcrypt 无法读取已存储的哈希时报错，而 Ok(true) 恰好表示密码正确。 
  • generate_token，它在配置的密钥下精确签署所给定的 claims，并在签署失败时报告 500。 
  • expiry_from_now，它读取时钟并写入恰好 24 小时后的过期时间。 
  • database_error，它把失败的查询转换成如今带 sqlx 错误信息的 500。 
  • 登录处理程序外壳，它解包请求并把请求字段原封不动地传递给 login_flow。 

在规范中，lookup 将其代码保留在原处，并从外部通过 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）。每个假设的子句随后会在计划的“经验验证”部分获得一次实证检查，在任何测试存在之前以 Given/When/Then 场景的形式编写（图 10）。一条条目在被执行之前标记为 planned，之后它会记录命令的结果以及运行时所针对的提交。

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 的计划内测试，在测试存在之前编写。计划将通过的测试标记为证据，而非证明。 

计划对无人承诺的内容同样明确：login future 是否会完成、超出范围的时钟不会 panic、关于尝试的时机或频率的任何内容，以及其他端点如何读取 role。 

第 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，它把密码检查和令牌绑定在一起。例如，设想一个 bug：登录时用一个账户检查密码，却为另一个账户签发令牌。Bob 用自己的正确密码登录，却拿回了 Alice 账户的令牌。每一步单独看都没问题，但这个子句能抓住它，因为密码检查和令牌必须指向同一个账户。这正是测试套件很少想到要去找的那种接线 bug。规范还必须谈及 SQLite、bcrypt 和 JWT，却不用真正运行它们。它通过未解释函数来实现——只有名字、没有内容的名字：customer_on_file(email) 和 admin_on_file(username) 表示数据库保存的行，bcrypt_verdict(password, hash) 表示 bcrypt 会说什么，token_claims(token, secret) 表示令牌携带的内容。除了第 4 步的可信契约所承诺的内容之外，Verus 对它们一无所知。证明说的是“无论数据库里存了什么，login 都会正确处理它”，而一个可信契约说“查找返回数据库保存的内容”。 

/// 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，但它是一个永不运行的数学定义，只出现在契约中。这样的代码被称为幽灵代码，因为验证器会检查它，但编译器会把它从程序中抹去。有了它，开发者的两句话请求最终变成了对 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. 两句话的请求和 Both ways 的决定最终成为对 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 是 async 的：它会 await 一个数据库查询。Verus 可以为 async 函数加契约，但有一条值得了解的规则（图 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 await 查找并调用 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), 
} 

在计划返回给你之前，两个审查者智能体会对从意图工件派生出的形式化规范进行挑错，以确保高质量的翻译，使规范与你的要求相符，且不会承诺超出证明所能展示的范围。规范细化在后台运行并接受用户的实时反馈，不断迭代，直到审查者一致认为规范是可靠的。 

第 6 步：证明、检查、补齐缺口 

开发者对规范的审签到此结束。其后的所有内容——实现与证明——都由机器检查，这就是为什么本文花在规范而非证明上。开发者签字确认后，一个 构建计划 阶段（图 16）将批准的计划交给 pdd-prove，由它把计划转换成一个小型任务图（图 16）。对于登录功能，这是七个任务：让 backend crate 中的 login.rs 在 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 下通过编译，且不改变任何契约所承诺的内容；遇到问题时会停下来询问，而不是削弱契约。 

每个任务都运行同一个循环： 

  • 一个编码智能体编写实现和证明，Verus 则依据派生的形式化规范对它们进行检查。 
  • 受信边界中的所有内容都会得到计划所要求的测试。 
  • 一个 LLM 验证器并排阅读计划、规范和结果，寻找缺口：既没有证明也没有通过检查的需求。缺口会被发回编码智能体，直到没有剩余为止。如果规范本身存在缺口，例如两个需求相互矛盾，则会作为一项决策返回给开发者。 

证明的好坏取决于其规范，因此 pdd-prove 也会检查规范。当模型编写自己的规范，或被调优来产出证明时，它往往会落在弱不变量上：那些能够通过验证却几乎不排除任何情况的条款。它们确实证明了某件事，只是很少是你真正关心的那件事。我们称之为“氛围验证（vibe verification）”。这就是为什么确保你的意图与智能体对齐如此重要，也正是 PDD Kit 的擅长之处。 

这个循环严格禁止移动目标。如果某个异步构造无法在固定的 Verus 版本中表达，任务会停下来询问团队，而不是切换到非异步的辅助函数或削弱某个契约。 

PDD Kit 是如何消除各类 bug 的？变异检查（mutation check）是 PDD Kit 防范“凭感觉验证”的手段。pdd-prove 会在代码的一个临时副本中为每个 ensures 子句植入一个 bug，比如拒绝所有用户，或者先检查用户名再检查邮箱，然后 Verus 必须在该子句的目标范围内拒绝每一个变异体。如果一个变异体通过了，就意味着那个子句没有约束任何东西，它会作为一个缺口被反馈回来。 

第 7 步：在审查已验证代码的同时审查意图

当任务通过后，pdd-prove会打开 pull request。它们会添加一个 verified/ crate，其中包含login_flow、它的各个部分、它们的证明，以及带有测试的可信包装器，并将真正的登录处理程序改道经过login_flow，同时保留现有的 HTTP 状态码。你验证过的逻辑会集成并加固你的生产登录路径，而不是它的一个副本。 

开发者无需对生成的代码进行穷尽式的逐行审查即可合并。审查其实一直在意图工件上进行，团队在那里拥有最终决定权。我们把更多的审查重点从代码审查转移到了意图审查。这个 pull request 充当了收据，其描述将每一条登录要求都标记为已形式化验证或已实证检验。 

合并是证明融入团队日常工作流的地方。PDD Kit 的 pdd-ship 工作流会把 Verus 检查加入 CI，与实证测试并列，这样之后每一次对登录的改动，无论来自人还是智能体，都必须继续针对同一份规范通过证明，而一个失效的证明会像失败的测试一样让构建失败。由于一个证明覆盖所有输入，PDD Kit 会剪除那些只重复验证已证明内容的测试，例如针对密码门槛的基于示例的测试，并保留那些守护可信边界的测试，因此 CI 同时变得更强也更精简。 

证明说了什么、没说什么 

“完全验证”很容易被夸大，所以我们在此明确说明我们声称的到底是什么。

  • 已证明。login_flow、login_core、lookup_target、decide_login和issue_token 的函数体对每一个输入都满足其契约。登录会选择正确的表，将请求中的密码与其所指定账户的存储哈希进行比较，签发一个带有该账户 id 及其所在表赋予角色的 token，并拒绝其他一切情况，返回现在的 400、401 或 500 状态码且不签发 token。 
  • 可信且经测试。两个数据库查询、基于 bcrypt 的check_password 、时钟、token 签名、数据库错误消息以及处理程序的请求解包都在证明之外，各自位于开发者已接受的一个假定契约之后。针对真实 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 的重心在于先把意图弄对的原因。我们会从 bug 代价最高的地方入手，比如登录、支付或权限，然后逐一验证代码库的其余部分。

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 工作流会针对每个条款植入一个 bug，以捕捉那些虽然通过验证却什么也没排除的条款。错误的规约仍然可能出现，这就是 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

#产品更新#Agent#编码#部署/工程#Microsoft