Article · AI translation
一览：让形式化方法走进日常软件开发。PDD Kit 帮助你将意图转化为形式化规范，然后证明智能体编写的代码对每一种输入都符合该规范，并在证明无法覆盖的地方使用测试。它让形式化方法走出小众的专家领域，惠及没有形式化方法背景的工程师和日常应用，例如这里展示的全栈 Web 应用。随着 AI 智能体生成的代码越来越多，逐行详尽的人工审查可能难以扩展。计划本应是你与编程智能体之间的契约，但实际上没有任何机制强制智能体遵守它。智能体编写的测试通常检验的是它构建出的东西，而不是你要求的东西。PDD Kit 让智能体遵守计划。它与你协作，将你的意图转化为 Verus（在新标签页中打开）中的形式化规范，证明智能体的代码对每一种输入都符合该规范，并在证明无法覆盖的地方改用测试。我们在一个全栈 Web 应用上试用了它。在 GitHub Next 的 Chopin（在新标签页中打开）中，我们使用 PDD Kit 对 Pet Store（一家用 Rust（在新标签页中打开）编写的在线商店）的登录逻辑进行了形式化验证。Verus 加固了代码，发现了已有的错误，并证明相对于该规范不存在登录错误。开发者审查了意图，但从未逐行阅读生成的代码。计划是智能体应该遵守的契约，但没有任何约束能确保智能体遵守。如今，编程智能体常常一次就交付完整功能，涉及的代码往往有数万行甚至数十万行。因此，逐行阅读拉取请求中的代码，无法适应这种新的工作方式。现在，大多数团队转而把精力放在计划和相关测试上：向智能体描述他们想要什么，反复沟通，直到计划和拟议的测试看起来合适，再交给智能体实现。这个计划或自然语言规范本应是智能体遵守的契约。然而在实践中，智能体可能偏离它：实现的内容略有不同，然后编写能让自身实现通过的测试，而不是检验它按你的意图编写的代码。由于测试数量多而质量低，持续集成（CI）的负担随之增加；覆盖率看起来不错，但你要求的内容与最终交付的内容之间的差距依然隐藏着，直到错误报告出现或棘手的边界情况浮现。那么，随着智能体生成越来越多的代码，如何可靠地扩大审查规模？智能体编写的代码会以两种通常能被细心的审查者发现的方式出错：遗漏明显必要的内容，或者做了明显错误的事。单靠测试无法弥合这一差距，因为测试只覆盖程序可能行为中极小的一部分。要弥合它，需要另一种机制，而这正是证明发挥作用的地方。审查问的是“这看起来对吗？”证明回答的是“这确实对吗？”数学证明表明，代码对于每一种输入都符合其规范，包括测试套件可能遗漏的输入。对于规范中明确规定的性质，这比单靠测试提供了更强的保证，尤其是在逐行审查不切实际的时候。过去，证明对日常软件开发来说成本太高。你需要专家、需要使用不熟悉的语言，证明的篇幅可能是代码的许多倍，而且开发证明要花上数年；但此后有两件事发生了变化。首先，编程智能体近期的进步，使它们协助根据定义明确的规范生成形式化证明变得越来越可行。其次，智能体现在也能更好地帮助你编写形式化规范。我们把这种新的软件开发范式称为证明驱动开发（Proof-Driven Development，PDD）。PDD Kit 是我们为此打造的工具包。PDD Kit 如何运作：对于形式化方法来说，PDD Kit 的作用大致相当于 Spec Kit（在新标签页中打开）对于规范驱动开发的作用。它作为协作伙伴，在 GitHub Next 的实时多人规划环境 Chopin（在新标签页中打开）中运行，团队和智能体可以在同一份共享文档中制定计划。这个工作流程分为两部分（图 1）。 首先，团队成员用日常语言审查意图。PDD Kit 会提出细心的审查者会问的问题，边进行边解释相关代码，并将答案记录在一份意图文档中。这份文档连接用户意图与形式化规约或测试。用户意图中能够形式化的部分会转化为形式化规约；其余必须基于信任接受的部分则会转化为用于测试的非形式化规约。PDD Kit 会自动生成证明，证明代码满足推导出的形式化规约，并为非形式化规约生成高质量测试。整个过程都不要求你具备形式化方法背景。图 1. 使用 PDD Kit 进行证明驱动开发。团队成员明确意图。Verus 和测试套件据此检验代码。因此，PDD Kit 的每项结果都会说明它依据哪种验证：形式化验证是一种数学证明，证明代码对每一种可能的输入都满足其规约，并由一种称为验证器的工具检查。PDD Kit 目前使用的验证器是 Verus（在新标签页中打开），它是一种用于 Rust 的证明语言，由 Microsoft Research、Carnegie Mellon University、VMware Research、ETH Zurich、MPI-SWS、UNSW Sydney、the University of Texas at Austin、the University of Michigan、the University of British Columbia、the University of Wisconsin–Madison 和 the Weizmann Institute of Science 共同开发。经验性验证通过运行代码并观察其行为来检查代码。它涵盖证明无法触及的部分，例如第三方密码学库或用户界面。它使用单元测试和端到端测试、终端自动化、浏览器智能体，以及处理浏览器无法操作的内容的计算机操作智能体。测试通过只表明代码在所尝试的输入上正常运行，因此 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 当前存储的内容和时钟显示的时间是程序的输入，不是程序代码能够确立的事实。某件事是否会完成，以及完成得有多快。规范说明的是登录流程返回结果时你会得到什么。查询卡住或执行缓慢都不违反它。任何需要由人判断的事情，例如错误消息是否有帮助，或者界面是否合理。任何人都没有写下来的事情。证明只覆盖其规范，对于规范之外的要求不作任何保证。这正是实证验证发挥作用的地方。PDD Kit 会明确说明受信任边界，即此项证明所依赖的 TCB 部分。 它把每个受信任的部分封装进带有假定契约的小函数，使用 Verus 的 #[verifier::external_body] 或 external_fn_specification，让开发者逐一接受，并在计划中为每个假定条款安排一项测试。对于登录，开发者认可了六个部分：两个查找函数 Customer::find_by_email 和 Admin::find_by_username。每次等待完成且成功的查找，都会准确返回其对应表中该邮箱或用户名的记录；若不存在，则返回 None。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 也会指出该子句。每个子句都可以读作一个“如果……那么……”的条件句；图 11 拆解了对应开发者第一项要求的子句。图 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) 表示令牌携带的声明。除了第 4 步中的可信契约所保证的内容，Verus 对这些函数一无所知。证明表明：“无论数据库保存什么，登录流程都会正确处理”；而可信契约则表明：“查询会返回数据库保存的内容。” /// 登录时，数据库为且仅为这个邮箱保存的 /// customers 记录行（如果有）。 /// 保持抽象：只有 `Customer::find_by_email` 的 /// 可信契约说明它是什么。 pub uninterp spec fn customer_on_file(email: Seq) -> Option; ... /// 对于 `password` 和已存储的 `hash`，bcrypt 给出的结果： /// 如果该密码是生成此哈希时使用的密码，则为 Some(true)； /// 如果不是，则为 Some(false)； /// 如果 bcrypt 无法读取该哈希，则为 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) 指明一次登录对应哪个账户：如果提供了邮箱，就是该邮箱对应的 customers 记录行；否则，就是用户名对应的 admins 记录行；再否则就没有对应账户。它的写法类似 Rust，但它是一个永远不会运行、只出现在契约中的数学定义。这样的代码称为幽灵代码，因为验证器会检查它，而编译器会把它从程序中删除。借助它，开发者那两句话的要求最终成为 login_flow 上的 8 个 ensures 子句（图 12）。 /// 一次登录所对应的账户：如果提供了邮箱，则为该邮箱对应的 /// customers 记录行（角色为 \"customer\"）； /// 否则为该用户名对应的 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。 这项只有两句话的请求和“Both ways”的决定，最终变成了 login_flow 上的 8 条 ensures 子句。其中 4 条保留了现有的拒绝行为，因此店面和现有的 API 测试仍能正常工作。下面是完整的契约，文档注释已作删减。每条子句上方都有意图文档向团队展示的通俗英文注释：/// 整个登录过程，从头到尾等待完成：从 /// 请求字段到令牌或 HTTP 错误。 /// ... pub async fn login_flow(pool: &sqlx::SqlitePool, config: &Config, email: Option, username: Option, password: &str) -> (r: Result) ensures // 既没有电子邮件地址，也没有用户名：返回 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 表中的记录时， // 才授予 admin 角色。 (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), // 使用电子邮件地址登录时，令牌始终带有 customer 角色。 (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 能读取存储的哈希值时，它才返回 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）。调用创建 future 时会检查 requires。ensures 描述的是等待该 future 后得到的值。 没有任何保证说 future 一定会执行完毕，因此卡住的查询并不违反任何契约。login_flow 上的文档注释明确写道：/// ... 不保证 future 会完成。pub async fn login_flow(...) -> (r: Result) 图 14。检查契约时，同步函数与异步函数的情况。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 // 提供了电子邮件地址时，以它为准：按该地址精确查询 customers 表。email matches Some(e) ==> r == Ok::(LookupTarget::CustomerByEmail(e)), // 没有电子邮件地址而提供了用户名时，// 按该用户名精确查询 admins 表。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。该文件从上到下分为 4 层：Verus 需要知道的文件头、导入项和类型；对外部世界的抽象视图；将这一视图与实际代码连接起来的受信任契约；以及证明必须满足的 5 个契约。图 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）。对于登录功能，共有 7 项任务：让后端 crate 中的 login.rs 能在 Verus 下构建，证明决策逻辑、令牌逻辑和整个流程，然后为可信包装器和端到端登录编写测试。图 16。Build plan 在开发机器上将获批规范转化为 7 项任务。第一项任务是在不改变任何契约承诺的前提下，让 login.rs 能在 Verus 下构建；如果做不到，就停下来询问，而不是削弱契约。每项任务都遵循同一个循环：编码代理编写实现和证明，Verus 则根据推导出的形式化规范检查它们。可信边界内的任何内容都要接受计划要求的测试。一个 LLM 验证器并排阅读计划、规范和结果，查找缺口：没有证明、也没有通过检查的要求。缺口会交回编码代理处理，直到一个也不剩。如果规范本身存在缺口，例如两项要求相互矛盾，就会交回开发者决策。证明的可靠性取决于规范，因此 pdd-prove 也会检查规范。当模型编写自己的规范，或经过专门调校来生成证明时，往往会采用薄弱的不变式：这些条款虽然能通过验证，却几乎不能排除任何情况。它们确实证明了某些东西，只是很少是你关心的东西。我们称之为“凭感觉验证”（“vibe verification”）。这就是为什么确保你的意图与代理一致如此重要，也是 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 工作流会在 CI 中加入 Verus 检查，与经验性测试并行执行，因此此后无论是人还是代理修改登录功能，都必须继续针对同一规范完成证明；证明失效会像测试失败一样导致构建失败。 由于证明覆盖了所有输入，PDD Kit 会删去那些只是在重复检验已证明结论的测试，例如针对密码验证关卡的示例测试，并保留守护可信边界的测试，使 CI 同时变得更强大、更精简。证明能说明什么，不能说明什么 “完全验证”很容易被夸大，所以这里明确说明我们的主张。已证明：login_flow、login_core、lookup_target、decide_login 和 issue_token 的函数体对所有输入都符合各自的契约。登录流程会选择正确的表，将请求中的密码与其指定账户存储的哈希值进行比对，签发包含该账户 ID 和所属表赋予的角色的令牌，并对其他所有情况沿用目前的 400、401 或 500 响应，且不签发令牌。可信且经过测试：两次数据库查询、基于 bcrypt 的 check_password、时钟、令牌签名、数据库错误消息，以及处理函数对请求的解包，都不在证明范围内；它们各自受开发者接受的一项假定契约约束。针对真实 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 证明，以及覆盖证明所信赖的一切内容的测试。我们希望坦诚说明最薄弱的环节。这些保证的可靠程度取决于 6 个可信部分，其中 2 类承担了大部分关键责任：check_password 支撑着关于密码的每一项保证，而两次查询支撑着关于令牌所指账户的每一项保证。测试为它们提供支持，但没有证明它们。我们预计这一可信边界会随着时间推移显著缩小，使越来越多的代码能够得到形式化验证；我们也希望弄清这种方法能扩展到什么程度。我们真正改变的是人们审查的内容。团队不再主要依靠逐行审查智能体生成的代码，而是用通俗语言审查代码要实现的意图，再由证明确保代码符合这一意图。计划本来就应该是契约，而现在智能体确实必须遵守它。致谢：这项工作由 Microsoft Research Catalyst Lab、GitHub Next 和 Research in Software Engineering（RiSE）小组合作完成。我们感谢 GitHub Next 的 Maggie Appleton 和 Krzysztof Cieślak 在 Chopin 项目上的合作，也感谢 Nikhil Swamy、Lef Ioannidis、Janardhan Kulkarni 和 Shuvendu Lahiri 就形式化验证和意图形式化提供的反馈与讨论。我们还感谢 F*/Pulse 和 Verus 团队的支持。最后，我们感谢 GitHub Next 的 Idan Gazit 对此次合作的支持。 常见问题：如果由 AI 编写规格说明，谁来确保规格说明是正确的？错误的规格说明难道不会让我得到经过验证却仍然错误的代码吗？由你来确保；是的，确实会。证明只能表明代码符合规格说明，不能表明规格说明符合你的本意。这就是为什么 PDD Kit 以现有的意图形式化研究为基础。pdd-plan 工作流会读取你的代码，在编写任何内容之前提出问题，并将你的回答转化为 Verus 规格说明和一份供你批准的通俗语言计划；遇到歧义时，它会标明歧义，而不是猜测。2 个审查智能体检查规格说明，pdd-prove 工作流则针对每个条款植入 1 个错误，以找出那些虽能通过验证、却没有排除任何情况的条款。规格说明仍有可能出错，因此 PDD Kit 强调明确写出需求、识别歧义，并让开发者在验证开始前参与审查和批准规格说明。这与规格驱动开发（SDD）、测试驱动开发（TDD），或者只是让智能体检查自己的工作有何不同？区别在于用什么来确保代码符合计划。方法／用什么检查代码：规格驱动开发／没有机制强制执行规格说明；测试驱动开发／针对部分输入进行测试，而测试往往是为了匹配已经构建的内容而编写的；智能体检查自己的工作／由编写代码的同一个模型检查；证明驱动开发／Verus 自动验证代码满足你批准的规格说明的证明。PDD 保留了 SDD 的规划循环，并且在证明无法覆盖的地方仍然使用测试。测试检查部分输入，而证明则在其声明的假设条件下，确立代码对于形式化模型所涵盖的所有输入都满足指定属性。证明究竟是什么？在哪里运行？它是确定性的，还是另一个语言模型（LM）？又需要多长时间？证明是用 Verus 构造标注的 Rust 代码，由 Verus 使用 Z3 求解器进行机械检查。它在你的 Rust 构建所运行的环境中运行：pdd-prove 工作流在证明过程中运行它，而 pdd-ship 工作流将它加入构建流程和 CI，使证明失效时构建失败。检查是确定性的，不涉及模型。模型编写规格说明、代码和证明，但只有确定性的 Verus 运行结果才能决定是否通过。检查所需时间因代码规模和证明难度而异：小型模块通常只需数秒，较大的代码库则可能需要数分钟。如果验证取代逐行代码审查，我实际上要审查什么？PDD Kit 将审查过程更多地转向确认代码应该做什么，同时利用形式化验证，为实现符合这些需求提供额外保证。开发者审查自然语言计划、形式化规格说明，以及证明范围之外需要信任的组件。由此产生的拉取请求会记录哪些内容经过了形式化验证、哪些内容经过了测试，以及哪些地方可能需要进一步审查。在 Pet Store 全栈 Web 应用中，这种方法减少了对生成代码进行详尽逐行审查的依赖。它只适用于 Rust 吗？为什么选择 Verus，而不是其他验证工具或形式化语言？我们选择 Verus，是因为它允许我们直接验证 Rust 代码，这与 PDD Kit 将形式化验证融入现有 Rust 开发工作流的重点相符。其他证明语言（例如 Lean、F*、Rocq）采用不同的形式化验证方法，各有取舍。PDD Kit 背后的技术也可能有助于应用这些语言。在新标签页中打开。《使用 PDD Kit 对智能体编写的全栈 Web 应用进行形式化验证》一文最先发表于 Microsoft Research。