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

概览

面向日常软件的形式化方法。PDD Kit 帮助你将自己的意图转化为形式化规格，然后证明你的智能体编写的代码对每个输入都满足该规格，并在证明无法覆盖之处使用测试。它把形式化方法从狭窄的专家工作带给没有形式化方法背景的工程师，也带给日常应用，比如这里展示的全栈 Web 应用。

随着 AI 智能体生成越来越多的代码，逐行进行详尽的人工审查可能变得难以扩展。计划本应是用户与编码智能体之间的契约，但实际上没有任何机制强制智能体遵循它。智能体编写的测试通常检查的是它构建了什么，而不是你要求了什么。

PDD Kit 让智能体遵守计划。它与用户协作，将意图转化为 Verus（在新标签页中打开）中的形式化规格，证明智能体代码对每个输入都满足该规格，并在证明无法覆盖之处回退到测试。

我们在一个全栈 Web 应用上进行了尝试。在 GitHub Next 的 Chopin（在新标签页中打开）中，我们使用 PDD Kit 对 Rust（在新标签页中打开）店面应用 Pet Store 的登录逻辑进行了形式化验证。Verus 强化了代码并发现了既有缺陷，证明了相对于该规格不存在登录缺陷。开发者审阅了意图，从未逐行阅读生成的代码。

计划是智能体应当遵循的契约，但没有任何机制约束智能体去遵循它。

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

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

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

播客系列

理念

聆听微软研究界成员讨论驱动其研究的信念、影响其研究的经历与思想家，以及其所瞄准的积极人类影响。

立即收听

在新标签页中打开

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

过去，证明对于日常软件来说过于昂贵。你需要专家、不熟悉的语言、比代码大许多倍的证明，而且证明需要数年才能开发出来，但此后有两件事发生了变化。首先，编码智能体的最新进展使其越来越能够从定义良好的规格帮助生成形式化证明。其次，智能体现在能更好地帮助你编写形式化规格。我们将这种新的软件开发范式称为证明驱动开发（PDD）。PDD Kit 是我们为此提供的工具包。

PDD Kit 的工作原理

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

该工作流分为两半（图 1）。首先，团队成员用通俗语言审阅意图。PDD Kit 会提出细心审查者会提出的问题，在过程中解释相关代码，并将答案记录在意图工件中，这是一份连接用户意图与形式化规格或测试的文档。用户意图中可形式化的部分被转换为形式化规格，其余必须被信任的部分被转换为用于测试的非形式化规格。PDD Kit 自动生成证明，表明代码满足所推导出的形式化规格，并为非形式化规格生成高质量测试。你不需要任何形式化方法背景。

图 1. 使用 PDD Kit 的证明驱动开发。团队成员确定意图。Verus 和测试套件使代码遵守它。

因此，PDD Kit 中的每个结果都会说明它依赖哪种验证：

形式化验证是数学证明，表明代码对其规格对每个可能的输入都满足，由称为验证器的工具检查。对于当前的 PDD Kit，该验证器是 Verus（在新标签页中打开），这是一种用于 Rust 的证明语言，由微软研究院、卡内基梅隆大学、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 中的整个请求只有两句话：

验证 backend/src/handlers/auth.rs 中的登录逻辑。以下是我的需求：

只有使用正确密码才能获得令牌。

只有管理员账户才能获得管理员令牌。

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

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

PDD Kit 的规划工作流 pdd-plan 会阅读代码，并在编写任何内容之前，在“决策”标签页中带着问题回来。当某个问题取决于代码如何工作时，卡片会先解释那部分：目标、各部分如何配合，以及涉及的确切函数，这样你无需打开源代码就能回答。

图 2. 第一张决策卡。“只有使用正确密码”这一条本身，也会被一个拒绝所有人的登录所满足。对两个方向都进行证明即可排除这种情况。

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

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

随着对话的进行，PDD Kit 会在计划顶部保持一个粗略的工作区，以便用户可以跟踪重要概念，而无需在冗长的聊天记录中回滚查找已达成一致的内容。它包括正在被规格化的登录流程图、将要证明什么和将要信任什么的规格全景图，以及在图片有帮助时提供的心智模型。对于登录，PDD Kit 画了一个售票台（图 3）。

图 3. PDD Kit 对登录的心智模型。你发送的字段选择窗口，窗口选择表并随之选择角色，在密码匹配之前不会打印任何内容。

在它下面，意图图将每项需求与开发者自己的话联系起来，并记录它是如何被确定的（图 4）。每个条目都链接到对其进行建模的形式化规格部分，以及覆盖它的测试，规格部分会展示 Verus 合约的片段，并加以注释，以便开发者看到形式化规格如何对其意图建模。

图 4. 决策后的意图图条目：登录只有使用该账户的正确密码才能获得令牌，并且始终如此。流程图展示了密码检查可能结束的每一种方式。

图 2 中的决策卡正是智能体否则会默默解决的那种歧义。图 5 展示了这种差异在纸面上看起来有多小：两种解读在单个单元格上不一致，即正确密码却未获得令牌。

图 5. 同一句话的两种解读。它们在一个单元格上不同，而那个单元格改变了证明必须确立的内容。

第 3 步：证明登录函数

在构建任何东西之前，PDD Kit 要求团队对整个计划签字确认。它的初稿证明了登录核心的决策，即选择表并以密码为门控，并将围绕它的处理程序保持为受信任和受测试的。这是一个合理的默认值，也是 PDD Kit 推荐的，但开发者想要更多。处理程序是查找被等待、令牌被签名的地方，而这段胶水代码正是重构可能悄悄交换两行的地方。因此在意图审查时，开发者选择为登录处理程序赋予自己的异步规格，这样证明也覆盖那段胶水代码，而不是信任它（图 6）。

图 6. 证明更多登录逻辑意味着信任更多小型包装器。卡片在开发者选择之前就说明了这一点。

这一选择几乎把所有内容都移入了证明，让登录处理程序除了解包请求之外无事可做。一个新的异步函数 login_flow 承载从请求字段一直到令牌或 HTTP 错误的契约。随后 PDD Kit 将修订后的计划带回以进行新一轮签字确认，因为符合你的意图并不等于证明，而且它不会批准新的信任或更广的范围。

第 4 步：证明止步之处

关于一个程序，有很多事情你无法证明，而登录会碰到其中大部分：

验证器看不到的代码。bcrypt 的哈希、sqlx 的查询和 jsonwebtoken 的签名位于其他 crate 中，在证明之外。

关于外部世界的事实。SQLite 现在持有什么以及时钟显示什么时间，是程序的输入，而不是其代码能够确立的东西。

某事是否完成以及完成得多快。规格说明的是如果 login 给出答案你会得到什么。挂起的查询或缓慢的查询不会破坏其中的任何内容。

任何必须由人判断的事情，比如错误消息是否有帮助或屏幕是否合理。

任何没有人写下来的东西。证明覆盖其规格，并且对规格之外的需求只字不提。

这就是经验性验证的用武之地。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 从外部获得契约：

/// 按精确电子邮件查找客户。 /// 受信任，未证明：SQL 查询在 sqlx 中运行，Verus 无法检查。 /// `login_flow` 的每一项客户承诺都依赖于此。 #[verifier::external_fn_specification] pub async fn ex_customer_find_by_email(pool: &sqlx::SqlitePool, email: &str) -> (r: Result, sqlx::Error>) ensures // 当查询成功时，它返回恰好对应此电子邮件的 // 客户行，若不存在则返回 None。 r matches Ok(found) ==> found == customer_on_file(email@), { Customer::find_by_email(pool, email).await }

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

/// 读取时钟并计算令牌 24 小时后的过期时间。 /// 受信任，未证明：chrono 的时钟在证明之外。 /// 如果时间超出范围，它会 panic，与今天的登录一样； /// 该 panic 不在承诺范围内。 #[verifier::external_body] pub fn expiry_from_now() -> (r: Expiry) ensures // 过期时间恰好是时钟读数之后 24 小时（86,400 秒）。 r.exp as int == r.now as int + 86_400, { ... }

图 7 将这三个层次放在一起：Verus 证明了什么、人们接受并由测试检查什么，以及没有人承诺什么。

图 7. 登录证明止于何处。Verus 对每个输入都证明核心部分。人们接受受信任环，并由测试检查它。计划列出了没有人承诺的内容。

图 8 映射了哪些内容被证明、哪些内容被信任。每个信任决策都是一张独立的卡片。它展示了 Verus 将凭信念接受的子句、开发者正在接受的内容，以及如果假设有误，哪一项承诺会失效（图 9）。随后，每个被假设的子句都会在计划的“经验验证”部分接受经验检查，并在任何测试存在之前写成 Given/When/Then 场景（图 10）。条目在运行之前标记为“已计划”，运行之后则记录命令的结果及其运行所针对的提交。

图 8. 登录中哪些内容被证明、哪些内容被信任。绿色函数由 Verus 对每个输入进行证明。琥珀色部分受信任，由开发者接受，并由计划 §4.1 中计划的测试进行检查。

图 9. check_password 的信任卡片。Verus 凭信念接受这两个子句，因此由人接受它们，并由两个测试检查它们。

图 10. 为受信任的 check_password 计划的测试，在测试存在之前编写。计划将通过的测试标记为证据而非证明。

计划同样明确说明了没有人承诺的内容：登录 future 最终会完成、超出范围的时钟不会 panic、任何关于尝试时机或速率的内容，以及其他端点如何读取角色。

第 5 步：阅读规格

意图工件是团队审阅的内容。它是 PDD Kit 作为 Verus 合约编写的正式规格的通俗语言版本。你可能会想，现在是不是得有人去读证明而不是读代码了。没有人需要这样做，因为编码智能体编写证明，而 Verus 会检查证明的每一步。如果 Verus 接受该证明，那么无论有没有人读它，它都成立。证明所依据的是规格，所以人们审阅的是规格，而这份规格短到几分钟就能学会阅读。每个函数都有一个 ensures 块：关于其结果 r 的陈述，这些陈述必须对每一种可能的输入都成立。Verus 在你构建时检查它们，如果任何子句哪怕对一种输入可能失败，构建就会失败，Verus 会指向那个子句。每个子句读起来都像 if-then，图 11 拆解了针对开发者第一个需求的子句。

图 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 步中受信任合约所承诺的内容。证明说的是“无论数据库持有什么，登录都会正确处理它”，而一个受信任合约说“查询返回数据库所持有的内容”。

/// 当登录进行查找时，数据库为 /// 恰好这个 email 持有的 customers 行（如果有）。 /// 保持抽象：只有 `Customer::find_by_email` 的 /// 受信任合约说明了它是什么。 pub uninterp spec fn customer_on_file(email: Seq) -> Option; ... /// bcrypt 对 `password` 与存储的 `hash` 给出的判断： /// 当它就是生成该 hash 所用的密码时为 Some(true)， /// 不是时为 Some(false)，bcrypt 无法读取该 hash 时为 None。 /// 保持抽象：其含义属于 bcrypt，通过 `check_password` 被信任接受。 pub uninterp spec fn bcrypt_verdict(password: Seq, hash: Seq) -> Option;

/// 根据 bcrypt 的判定，该密码与存储的哈希相匹配。 pub open spec fn password_matches(password: Seq, hash: Seq) -> bool { bcrypt_verdict(password, hash) == Some(true) }

在这些之上，named_account(email, username) 说明一次登录命名的是哪个账户：发送了 email 时，是 email 对应的 customers 行；否则是 username 对应的 admins 行；否则没有。它写起来像 Rust，但它是一个数学定义，从不运行，只出现在合约中。这样的代码被称为幽灵代码，因为验证器会检查它，但编译器会把它从程序中擦除。借助它，开发者两句话的请求最终变成了 login_flow 上的八个 ensures 子句（图 12）。

/// 一次登录命名的账户：发送了 email 时，是 /// email 对应的 customers 行（角色 "customer"）， /// 否则是 username 对应的 admins 行（角色 "admin"），否则没有。 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, }, } }

图 12. 两句话的请求和“两种方式”决策最终变成了 login_flow 上的八个 ensures 子句。其中四个保留了今天的拒绝行为，因此店面（storefront）和现有 API 测试继续正常工作。

下面是完整的合约，其文档注释已精简。每个子句上方都有意图工件向团队展示的通俗英文注释：

/// 完整的登录流程，端到端等待：从 /// 请求的字段到令牌或 HTTP 错误。 /// ... pub async fn login_flow(pool: &sqlx::SqlitePool, config: &Config, email: Option, username: Option, password: &str) -> (r: Result) ensures // 既没有 email 也没有 username：返回 400 和今天的消息。 email is None && username is None ==> (r matches Err(AppError::BadRequest(m)) && m@ == missing_identity_text()), // 只有登录所指定账户且密码正确时才返回令牌；令牌携带该账户的 id 及其所在表的角色。 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), // 为指定账户提供正确密码时总能获得令牌，除非查找或签名失败导致 500。 (named_account(email, username) matches Some(a) && password_matches(password@, a.password_hash)) ==> (r is Ok || r matches Err(AppError::Internal(_))), // 登录指定的账户不存在时返回 401，除非查找失败导致 500。 ((email is Some || username is Some) && named_account(email, username) is None) ==> (r matches Err(AppError::Unauthorized) || r matches Err(AppError::Internal(_))), // 账户存在且 bcrypt 能读取其哈希，但密码错误时返回 401，除非查找失败导致 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(_))), // 账户存在但 bcrypt 无法读取其存储的哈希时返回 500 且不返回令牌。 (named_account(email, username) matches Some(a) && bcrypt_verdict(password@, a.password_hash) is None) ==> r matches Err(AppError::Internal(_)), // 管理员角色仅适用于通过用户名找到的 admins 行，且不发送电子邮件。 (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), // 电子邮件登录的令牌始终携带客户角色。 (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 的一个无公理的非解释模型：

/// 询问 bcrypt `password` 是否与存储的 `hash` 匹配。 /// 受信任，未证明：Verus 无法检查 bcrypt 的哈希计算， /// 因此假定此包装器的契约成立。 /// `login_flow` 的每一个密码承诺都依赖于它。 #[verifier::external_body] pub fn check_password(password: &str, hash: &str) -> (r: Result) ensures // 当且仅当 bcrypt 能读取存储的哈希时，bcrypt 才回答 (Ok)。 r is Ok bcrypt_verdict(password@, hash@) is Some, // 其答案即其判定：正确密码为 true， // 任何其他密码为 false。 r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b), { bcrypt::verify(password, hash).map_err(|e| e.to_string()) }

其上的文档注释说明了依赖于它的是什么：login_flow 的每一个密码承诺。每次登录都终结于少数几个位置之一，其中只有一个位置有令牌（图 13）。证明一次性覆盖了所有这些位置。

图 13. 登录可能结束的每一种方式，来自计划。

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

login_flow 上的文档注释正是这样说的：

/// ……不承诺 future 会完成。 pub async fn login_flow(...) -> (r: Result)

图 14. 对于同步 fn 和异步 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 // 当发送了电子邮件时，电子邮件优先：客户会按该电子邮件被精确搜索。 email matches Some(e) ==> r == Ok::(LookupTarget::CustomerByEmail(e)), // 没有电子邮件时，用户名会将搜索 // 发送给管理员，按该用户名精确搜索。 email is None && username matches Some(u) ==> r == Ok::(LookupTarget::AdminByUsername(u)), // 两者都没有时，登录因缺少身份而被拒绝。 email is None && username is None ==> r == Err::(LoginError::MissingIdentity),

pub fn decide_login(target: &LookupTarget, found: Option, password: &str) -> (r: Result) ensures // 未找到行：以 Unauthorized 拒绝，// 与密码错误给出相同答案。 found is None ==> r == Err::(LoginError::Unauthorized), // 仅当找到的行其存储哈希与密码匹配时，// 才返回声明。 r is Ok ==> found is Some && password_matches(password@, found->Some_0.password_hash@), // 找到的行使用正确密码时总能获得声明。 found matches Some(a) && password_matches(password@, a.password_hash@) ==> r is Ok, ... // 在 admins 表中搜索会给出角色文本 "admin"。 r matches Ok(c) && target is AdminByUsername ==> c.role@ == admin_role(), // 在 customers 表中搜索会给出角色文本 "customer"。 r matches Ok(c) && target is CustomerByEmail ==> c.role@ == customer_role(),

login.rs 概览

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

图 15. login.rs 的各部分，按文件顺序排列。灰色是头文件和类型，紫色是仅出现在契约中的数学，琥珀色是受信任的，绿色是已证明的。

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

/// 连接池对证明不透明：只有 /// 查找操作的契约说明了它返回什么。 #[verifier::external_type_specification] #[verifier::external_body] #[verifier::reject_recursive_types(DB)] pub struct ExPool(sqlx::Pool); ... /// 一个 customers 行，其字段对证明可见。 #[verifier::external_type_specification] pub struct ExCustomer(Customer);

而 LoginError 将决策与 HTTP 响应分开，这正是 issue_token 能把每种拒绝固定到当前状态码的原因：

/// 登录为何拿不到令牌。 pub enum LoginError { /// 既未发送邮箱也未发送用户名：400 Bad Request。 MissingIdentity, /// 无此账户，或密码不匹配：401 Unauthorized。 Unauthorized, /// bcrypt 无法读取存储的哈希，附带其消息：500 Internal。 UnreadableHash(String), /// 查找查询失败：500 Internal，附带 sqlx 的消息。 Database(sqlx::Error), }

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

第 6 步：证明、检查、弥合差距

签署规格是开发者审阅的终点。此后的一切——实现与证明——都由机器检查，这正是本文把时间花在规格而非证明上的原因。开发者签署后，Build plan 阶段（图 16）会把已批准的方案交给 pdd-prove，后者将其转换为一个小型任务图（图 16）。对于登录，这包括七个任务：让 login.rs 在后端 crate 中于 Verus 下通过构建，证明决策、令牌和整个流程，然后为受信任包装器和端到端登录编写测试。

图 16. Build plan 将已批准的规格转换为开发机器上的七个任务。第一个任务让 login.rs 在 Verus 下通过构建，且不改变任何契约所承诺的内容；遇到问题时停下来询问，而不是削弱契约。

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

编码智能体编写实现和证明，Verus 依据推导出的形式化规格对它们进行检查。

受信任边界内的任何内容都要接受方案所要求的测试。

LLM 验证器并排阅读方案、规格和结果，寻找缺口：没有证明也没有通过检查的需求。缺口会退回给编码智能体，直到不再有缺口。如果规格本身存在缺口，例如两条需求相互矛盾，则会作为待决事项退回给开发者。

证明的好坏取决于其规格，因此 pdd-prove 也会检查规格。当模型编写自己的规格，或被调优以生成证明时，它往往会落在弱不变式上：这些子句能通过验证，却几乎排除不了任何情况。它们证明了某些东西，但很少是你真正关心的东西。我们称之为“氛围验证”。这就是为什么确保你的意图与智能体保持一致如此重要，也正是 PDD Kit 擅长之处。

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

PDD Kit 如何消除各类缺陷？变异检查是 PDD Kit 防范“氛围验证”的手段。pdd-prove 会在代码的临时副本中，针对每条 ensures 子句植入一个缺陷，例如拒绝所有人，或在检查邮箱之前先检查用户名，而 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 且不签发令牌来拒绝其他一切情况。

受信任并经过测试。两处数据库查询、基于 bcrypt 的 check_password、时钟、令牌签名、数据库错误消息以及处理器的请求解包都位于证明之外，各自处于开发者已接受的假定契约之后。针对真实 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 对本次合作的支持。

常见问题

确实如此，而且答案也是肯定的。证明只能表明代码满足规格，而不能表明规格就是你的本意。这正是 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 背后的技术也可以帮助它们发挥作用。

高级首席研究员

了解更多

研究领域

编程语言与软件工程

系统与网络

相关实验室

微软研究院 Catalyst Lab