跳到正文
Microsoft Research· Alex Lavaee, Matthai Philipose·· 3 小时前精选AI 评分64

微软研究院发布 PDD Kit，用形式化证明验证智能体编写的全栈 Web 应用

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

AI 导读

微软研究院联合 GitHub Next 推出研究原型 PDD Kit，把用户意图转成 Verus 形式化规范，再证明智能体生成的代码对每个输入都满足该规范，证明覆盖不到的部分回退到测试。

推荐理由

微软研究院与 GitHub Next 展示了用形式化证明约束智能体生成代码的完整流程，读者可据此理解审查重心从代码转向意图的可行性。

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

概览

  • 面向日常软件的形式化方法。 PDD Kit 帮助你将自己的意图转化为形式化规约，然后证明你的智能体所编写的代码对每一个输入都满足该规约，并在证明无法覆盖之处使用测试。它把形式化方法从少数专家的细分工作，带给没有形式化方法背景的工程师和日常应用，比如这里展示的全栈 Web 应用。
  • 随着 AI 智能体生成越来越多的代码，逐行进行详尽的人工审查可能变得难以扩展。 计划本应是用户与编码智能体之间的契约，但实际上没有任何机制强制智能体遵守它。智能体编写的测试通常检查的是它构建了什么，而不是你要求了什么。 
  • PDD Kit 让智能体遵守计划。 它与您协作，将您的意图转化为 Verus (opens in new tab) 中的形式化规约，证明智能体的代码对每个输入都满足该规约，并在证明无法覆盖之处回退到测试。
  • 我们在一个全栈 Web 应用上进行了尝试。 在 GitHub Next 的 Chopin (opens in new tab) 中，我们使用 PDD Kit 对一个 Rust (opens in new tab) 店面 Pet Store 的登录逻辑进行了形式化验证。Verus 强化了代码并发现了现有缺陷，证明了相对于规约不存在登录缺陷。开发者审查了意图，从未逐行阅读生成的代码。 

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

编码智能体现在常常一次交付完整功能，往往涉及数万甚至数十万行代码。因此，逐行阅读拉取请求无法适应这种新的工作方式。现在，大多数团队转而投入计划与相关测试：向智能体描述他们想要什么，来回沟通直到计划和拟议的测试看起来正确，然后交给智能体去实现。 

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

那么，随着智能体生成越来越多的代码，如何可靠地扩展审查？智能体代码会以两种细心的审查者通常能发现的方式失败：遗漏了明显必要的东西，或者做了明显错误的事情。仅靠测试无法弥合这一差距，因为测试只覆盖程序所能做的一小部分。弥合这一差距需要另一种机制，这就是证明的用武之地。

审查问的是“这看起来对吗？”证明回答的是“这正确吗？”数学证明表明代码对每一个输入都满足其规约，包括测试套件可能遗漏的输入。对于已规约的属性，这比仅靠测试提供了更强的保证，尤其是在逐行审查不切实际的情况下。

过去，形式化证明对日常软件来说成本过高。你需要专家、陌生的语言、比代码大许多倍的证明，而且证明往往要花数年时间开发，但此后有两件事发生了变化。首先，编码智能体的最新进展使它们越来越能够根据定义良好的规格帮助生成形式化证明。其次，智能体现在能更好地帮助你编写形式化规格。我们把这种新的软件开发范式称为证明驱动开发（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 的工作。

第 1 步：先提问，后写代码

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。第一张决策卡。“只有密码正确才能拿到令牌”本身也能被一个拒绝所有人的登录满足。证明两个方向才能排除这种情况。

这个问题看似吹毛求疵，但很重要。“只有密码正确才能拿到令牌”排除了坏情况，即错误密码拿到令牌，而一个拒绝所有人的登录完美地遵守了这个承诺。“密码正确就一定能用”是排除它的另一半。形式上，第一个是蕴含（令牌 ⇒ 正确密码），第二个是它的逆命题。合在一起构成“当且仅当”。放任智能体自行处理，它会不告诉你就选一个方向，但在这里开发者选择了两个方向。

第 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. 同一句话的两种解读。它们只在一个单元格上不同，而那个单元格改变了证明必须确立的内容。

第 3 步：证明登录函数

在开始构建任何东西之前，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 将修订后的计划带回进行新一轮签署，因为符合你的意图并不等于证明，而且它不会批准新的信任或更广的范围。 

第 4 步：证明止于何处

关于程序，有很多事情你无法证明，而登录几乎撞上了其中大多数：

  • 验证器看不到的代码。 bcrypt 的哈希、sqlx 的查询和 jsonwebtoken 的签名位于其他 crate 中，在证明之外。 
  • 关于外部世界的事实。 SQLite 当前持有什么以及时钟显示什么时间，是程序的输入，而不是其代码能够确立的东西。 
  • 某事是否完成以及完成得多快。 规范说明的是如果登录应答你会得到什么。挂起的查询或缓慢的查询不会破坏其中的任何东西。 
  • 任何必须由人判断的事情，比如错误消息是否有帮助或屏幕是否合理。 
  • 任何没有人写下来的东西。 证明覆盖其规范，对其之外的任何需求不置一词。 

这就是经验验证的用武之地。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）。随后，每个被假设的子句都会在计划的“经验验证”部分获得经验性检查，并在任何测试存在之前写成 Given/When/Then 场景（图 10）。在运行之前，条目会标记为已计划，运行后则记录命令的结果及其运行所针对的提交。

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

计划同样明确说明了没有人承诺的内容：登录 future 最终会完成、超出范围的时钟不会 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，这把密码校验与令牌绑定在一起。例如，设想一个 bug：登录时用某个账户校验密码，却为另一个账户签发令牌。Bob 用自己的正确密码登录，拿回的却是 Alice 账户的令牌。每一步单独看都没问题，但这个子句能抓住它，因为密码校验和令牌必须指向同一个账户。这正是测试套件很少想到去查找的那类接线 bug。规范还必须在不实际运行 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，但它是一个从不运行的数学定义，只出现在契约中。这样的代码被称为幽灵代码，因为验证器会检查它，但编译器会把它从程序中擦除。有了它，开发者那两句话的请求最终变成 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 子句。其中四个保留当前的拒绝行为，因此店面（storefront）和现有 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 映射了整个 spec 文件，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), 
} 

在计划返回给你之前，两个审查代理会从意图工件中对推导出的形式化 spec 挑毛病，以确保高质量的翻译，使 spec 与你要求的一致，并且不会承诺超出证明所能展示的内容。spec 精化在后台运行，并接收实时用户反馈，反复迭代，直到审查者一致认为 spec 是可靠的。 

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

对 spec 签字确认是开发者审查的终点。此后的一切——实现和证明——都由机器检查，这就是为什么本文把时间花在 spec 上而不是证明上。开发者签字确认后，一个 Build plan 阶段（图 16）将已批准的计划交给 pdd-prove，后者将其转化为一个小型任务图（图 16）。对于 login，那是七个任务：让 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. Build plan 将已批准的 spec 转化为开发机器上的七个任务。第一个任务让 login.rs 在 Verus 下构建，而不改变任何契约所承诺的内容，并且会停下来询问，而不是削弱契约。 

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

  • 编码代理编写实现和证明，Verus 根据推导出的形式化 spec 检查它们。 
  • 可信边界内的任何内容都会获得计划所要求的测试。 
  • 一个 LLM 验证器并排阅读计划、规范和结果，并寻找缺口：没有证明也没有通过检查的需求。缺口会返回给编码代理，直到没有缺口为止。如果规范本身有缺口，例如两个需求相互矛盾，它会作为决策返回给开发者。 

证明的好坏取决于其 spec，所以 pdd-prove 也会检查 spec。当模型编写自己的 spec，或被调优以生成证明时，它往往会落在弱不变量上：这些子句能通过验证，但几乎排除不了任何东西。它们证明了某些东西，但很少是你关心的东西。我们称之为“氛围验证”。这就是为什么确保你的意图与代理对齐如此重要，也是 PDD Kit 擅长的地方。 

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

PDD Kit 如何消除各类 bug？变异检查是 PDD Kit 防范“感觉式验证”的手段。pdd-prove 会在代码的临时副本中，针对每个 ensures 子句植入一个 bug，比如拒绝所有人，或在检查邮箱之前先检查用户名，而 Verus 必须在其针对的子句上拒绝每一个变异体。如果有变异体通过了，就说明该子句没有约束任何东西，它会作为缺口被反馈回来。 

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

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

开发者无需依赖对生成代码进行详尽的逐行审查就能合并。审查其实一直发生在意图工件上，团队在那里拥有最终决定权。我们将更多审查重点从代码审查转移到了意图审查。拉取请求充当收据，其描述将每项登录需求标记为已形式验证或已经验检查。 

合并是证明融入团队正常工作流的地方。PDD Kit 的 pdd-ship 工作流会将 Verus 检查与经验测试一起添加到 CI 中，因此之后对登录的任何更改，无论是人还是代理做出的，都必须继续针对同一规范进行证明，而损坏的证明会像失败的测试一样使构建失败。而且由于证明覆盖所有输入，PDD Kit 会修剪那些只重新检查已被证明内容的测试，例如密码门控的基于示例的测试，并保留那些守护可信边界的测试，因此 CI 同时变得更强、更精简。 

证明说明了什么、没说明什么 

“完全验证”很容易被过度宣传，所以这里明确我们到底在声称什么。

  • 已证明。 login_flow、login_core、lookup_target、decide_login 和 issue_token 的函数体对每个输入都满足其契约。登录会选择正确的表，将请求中的密码与它所指定账户的存储哈希进行比较，签发一个带有该账户 id 及其表所赋予角色的令牌，并以当前的 400、401 或 500 拒绝其他所有情况且不签发令牌。 
  • 可信且已测试。 两次数据库查找、check_password 基于 bcrypt 的部分、时钟、令牌签名、数据库错误消息以及处理器的请求解包都位于证明之外，各自处于开发者已接受的假定契约之后。针对真实 bcrypt、真实 SQLite schema 和真实路由器的测试覆盖了它们。 
  • 已假定。 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 对这项合作的支持。

FAQ

  • 是的，而且没错，确实会。证明表明代码满足规范，而不是表明规范就是你的本意。这就是为什么 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 将更多审查流程转向验证代码应做什么，同时使用形式化验证来提供额外保证，确保实现满足这些需求。开发者审查自然语言计划、形式化规范以及不在证明范围内的可信组件。由此产生的拉取请求记录了哪些内容经过了形式化验证、哪些经过了测试，以及哪些地方可能需要额外审查。在 Pet Store 全栈 Web 应用上，这种方法减少了对生成代码进行逐行详尽审查的依赖。

  • 我们选择 Verus，是因为它允许我们直接验证 Rust 代码，这与 PDD Kit 将形式化验证集成到现有 Rust 开发工作流中的重点相一致。 其他证明语言（如 Lean、F*、Rocq）采用不同的形式化验证方法，各有其权衡。PDD Kit 背后的技术也可以帮助它们发挥作用。

在新标签页中打开

文章 使用 PDD Kit 对智能体编写的全栈 Web 应用进行形式化验证 首次出现在 Microsoft Research。

来源：Microsoft Research · microsoft.com

Microsoft / CopilotAgent 智能体AI 编码开源生态论文研究#论文/研究#Agent#编码#开源/仓库#Microsoft