PDD Kit 带来的新问题：创始人该如何审查 AI 产品的“已验证”承诺

一个功能即使拒绝所有客户，也可能满足“绝不能让不该进入的人进入”这条要求。对于请 AI 做一个“安全功能”、随后把绿色通过标记当成交付完成的创始人，这种可能性值得认真对待。

11 月 5 日，微软研究院介绍了 PDD Kit：把开发者意图连接到形式化规格和经过检查的证明，证明覆盖不到的部分再交给测试。演示围绕一个 Rust 网店的登录逻辑展开。对非技术创始人而言，值得关注的变化是：团队需要把“究竟希望功能怎样运行”变成一项明确的审查工作，而不只是放在无人能解释的实现前面的一句话。

本文面向准备验收 AI 构建客户功能的小团队，提供一份客户承诺审查表、一套验收会议流程，以及上线边界。核心判断是：既要问谁必须被挡住，也要问符合条件的客户应该得到什么，再为每项承诺写明条件和失败后的恢复办法。

我们没有运行 PDD Kit、复现演示，也没有测量开发效率。发布材料来自项目作者。下文的产品场景和审查流程是我们提出的方法，并非真实客户的实验结果；本文也不构成任何具体应用安全性的证明。

1. 先改变审查方式，再判断是否采用工具

GitHub Next 项目页说明，PDD Kit 仍是研究原型，目前验证的是 Rust。对于使用其他技术栈的产品，这是实际的采用边界。今天就能借鉴需求审查的思路，并不意味着明天就能把原型接入自己的构建工具。

安排试点之前，请技术负责人分别确认：能否获得原型使用条件、现有语言是否适用、把目标性质写成规格需要多少工作，以及后续由谁维护证明。某一项得到肯定回答，不代表其他问题都已解决。不要因为演示中的验证步骤看起来很快，就决定重写整个应用。

责任分工也会随之改变。创始人不必逐步阅读数学证明，才能决定客户的订阅变化后是否应立即失去访问权；但在工程师编码之前，必须把这条政策想清楚。熟悉账单例外的可能是客服负责人，熟悉权限执行的可能是工程师。双方都不应默默替另一方做决定。

GitHub Next 将 Chopin描述为协作式规划环境，同样处于研究原型阶段。共享规划有助于暴露分歧，却不会自动证明商业决策正确。只要功能涉及客服处理、产品规则和实现边界，就应让相应负责人参与同一次讨论。

眼前最有用的行动，是让团队在实现形成惯性之前说清楚期望行为。“取消订阅到底意味着什么”这样的分歧，写需求时讨论的成本，通常比上线后进入客服队列再处理更容易控制。即使完全不采用这个原型，这项工作也值得做。

2. 理解几个术语，才能质疑正确的对象

规格说明要检查什么行为。形式化证明是在给定规格和假设下建立数学结论。测试则运行选定的场景，观察发生了什么。它们回答的问题不同：测试通过不会因此变成证明，证明也不会替团队选择产品需求。 Verus 指南介绍了针对用户提供的规格，静态验证 Rust 代码的方法。指南同时明确，目前的目标不包括验证 Verus 自身，也不包括验证 Rust/LLVM 编译器。这些边界提醒我们，不能把“所有可能输入”随意扩展成对线上服务每一层都成立的承诺。 可信计算基，英文缩写 TCB，指证明所依赖、但没有由这份证明本身检查的组件和假设。创始人更需要听懂的是：如果某个假设组件的行为不同，哪一项客户承诺会变得不可靠？只拿到一串库名称，还不足以做出判断。 安全性质用于排除不希望发生的结果；进展或可用性要求则关注有用的事情是否发生，往往还涉及时间和依赖条件。它们可以帮助团队提问，但不能当作可以互换的形式化保证。某条规则约束函数结束后返回的结果，不一定证明函数能够结束。 Verus 代码仓库提供工具源码和项目文档，便于检查实现与项目状态。它不是对 PDD Kit 应用演示的独立复现。微软和 GitHub Next 的相关页面也不能算成两次独立的性能确认。本文提出的是这些边界支持的审查问题，并不声称已经测得可靠性提升。

3. 把正向权益写在禁止事项旁边

从实际产品简报中的一句话开始：“只有付费会员才能下载报告。”它规定了限制。如果系统谁都不让下载，也遵守了这条限制，却没有交付任何会员价值。缺失的问题是：付费会员应当得到什么，需要满足哪些条件？

设想一家虚构的研究服务 Harbor Notes，创始人小林希望用 AI 构建工具加入付费报告访问功能。Harbor 是教学场景，不是 YBuild 客户。这里有三个关键对象：会员、工作区和报告。报告可能已经就绪、仍在生成，或暂时不可用。支付状态与工作区成员关系也可能各自发生变化。

小林把要求改为：当前属于某工作区、且具有相应权益的会员，可以获取该工作区已经就绪的报告；其他用户不能获取。如果报告尚未生成完成，页面应说明状态，不能假装文件已经存在。如果暂时无法确认账单状态，产品应执行事先写明的临时政策，并给用户提供恢复途径。

这仍然是一份产品要求，不是形式化规格。它的价值在于，团队终于能够提出具体异议：所有者离开工作区之后，是否继续保留访问权？取消续费，是立即失去权益，还是到已付费周期结束才失效？报告创建人离开之后，其他成员还能不能读取旧报告？这些都是产品决策，“付费”两个字不会自动给出答案。

审查时应成对展示场景：先展示不符合条件的人被拒绝，再展示依赖正常时符合条件的人成功获取报告。还要确认，在整条流程中关联的始终是同一个报告、工作区和身份。另一个账号成功，不等于当前客户成功。工程师决定如何建模或测试之前，这样的讨论能先暴露政策缺口。

4. 分开处理资格、依赖故障和等待

最难处理的情况往往不是简单的“允许”或“拒绝”。老客户打开报告时，Harbor 的账单服务可能刚好不可达；文件可能已经写入存储，却尚未出现在应用索引里；权限检查也可能通过，但最终下载失败。这些状态应分别定义，并明确处理人。

对每个依赖，都要决定用户能看到什么，以及系统允许做什么。临时账单故障不应悄悄变成“客户没有付费”的永久结论；但无法确认状态，也不该变成向所有人开放权益。团队可以为已确认身份的老成员提供有限缓存访问，也可以暂缓敏感下载。选择取决于数据和政策，本文不提供一刀切的答案。

等待同样需要产品决策。一个永远转圈的页面，也许从未返回禁止返回的结果，却已经把用户晾在原地。应说明界面如何报告延迟、哪些操作可以安全重试、未解决问题由谁接手，以及最终结果怎样通知用户。时间目标应根据自己的服务能力制定，不要照搬某次演示中的数字。

Stripe 的 Webhook 文档给出了一个不能只假设理想流程的具体原因：事件送达顺序不受保证，同一事件也可能重复送达。如果产品靠账单通知更新权益，就需要问清楚：收到新状态之后，又来了一条旧通知，会怎样处理？针对本地决策的证明，无法弥补未经审查的上游状态假设。

因此，Harbor 的验收会议要分别回答三个问题：谁有资格、判断资格所需的证据是否可用，以及交付是否完成。客服应能区分这些原因，同时不泄露敏感账号信息。把所有问题塞进一个“访问被拒绝”分类，会让故障诊断和用户恢复都更困难。

5. 沿客户旅程审查，不止盯着被证明的组件

登录成功，不等于有权读取某一份报告。身份认证确认你是谁；授权判断这个身份能否对指定资源执行指定操作。Harbor 两者都需要。正确登录的客户，仍可能请求另一个工作区的报告。

OWASP 授权指南建议默认拒绝，并对每一次请求检查权限。可以据此追问：整条客户旅程里的权限究竟在哪里执行？仅仅把下载按钮隐藏起来，不能证明下载接口已经检查了用户与工作区的关系。

用普通语言列出流程：登录、选择工作区、请求报告、接收文件、打开分享链接。每经过一个环节，就说明谁作访问决定，决定针对什么资源。请工程师标明哪些部分处于形式化结论范围内，哪些经过了实际测试，哪些仍未检查。剩余不确定性是否适合本次发布，则需要创始人作出判断。

客户沟通也应单独审查。OWASP 身份认证指南解释了为什么通用的认证错误提示有助于防止账号枚举，同时讨论了易用性取舍。恢复流程要有帮助，但不能随口透露别人的账号是否存在。客服内部掌握的细节，可以比公开错误提示更多，两者仍应保持一致。

在 Harbor，小林请同事扮演一位下载失败的合法会员，完整走一遍流程：用户能否判断应等待、重试还是联系支持？给客服的查询编号能否定位这次失败，而不暴露其他工作区的数据？这些观察无法由针对某个较窄函数的证明替代。验收客户功能，必须包括这段体验，不能只验收决策逻辑。

6. 用客户承诺审查表，让遗漏留在明处

把下面的表复制到功能简报中。这些行是建议讨论的场景，不是 benchmark，也不是穷尽一切的安全检查清单。请用自己的政策替换 Harbor 的选择，并逐项记录：准确需求、已有证据、覆盖范围、未决问题、负责人，以及它对上线决定的影响。

如果只覆盖了一小部分，就不要把整行标成“已证明”。“权限决策在成员查询结果足够新的假设下已获证明；交付与界面经过测试”，这样的表述才有信息量。“下载已验证”并不能告诉发布负责人究竟在接受什么。

空白格代表需要做的决定，而不是应该藏起来的失败。有些行可以不适用：公开的静态报告就没有成员资格撤销规则。但要写清不适用的原因，以便今后公开功能增加付费限制时，团队知道哪些问题需要重新审查。

一个填好的 Harbor 条目可以是：“需求 H-01，修订 A：当前成员可以在已付费周期内下载自己工作区中已就绪的报告。假设：成员关系和权益查询结果足够新，文件存储可用。证据：计划中，尚未运行证明或测试。负责人：产品负责人决定资格，工程师负责执行。上线影响：依赖正常且客户合法时必须能成功获取报告，同时必须拒绝访问无关工作区，否则不开放付费使用。”

这是一条建议采用的验收记录，并不表示 Harbor 已经通过。如果实现对所有合法请求都返回临时错误，团队就必须检查成功要求和故障例外，不能因为拒绝统计看起来很漂亮就接受结果。

把审查表和功能验收记录放在一起。独立飘在别处的文档，很容易在智能体修改实现、或创始人修改政策之后过时。记录需求的版本标识，以及当时所审查的实现版本。如果无法把证据和当前功能对应起来，就应先把状态视为未知，直到有人完成核对。

7. 让验收会议检验理解，而不是只看绿色结果

邀请产品负责人和实现负责人参加。如果故障状态最终由客服或运维处理，也把他们纳入。一次选一条客户旅程，不要试图验收整个应用。提前发出政策问题，让会议真正解决决策，而不是奖励临场最会说技术术语的人。

先从合法客户应该得到的结果开始。请产品负责人解释，为什么这个人符合条件。随后一次改变一个事实：撤销成员资格、切换工作区、延迟账单证据，或者让报告保持未完成状态。实现负责人应说明现在适用哪条要求，而不只是展示测试套件全绿。

再问：验证通过，究竟建立了什么结论？要求团队用一句话说清性质、假设和实现版本。如果团队无法把这句话讲明白，创始人就无法负责任地把它变成对客户的承诺。补救办法可能是解释得更清楚、缩小范围，或者补做工作，要看缺的究竟是什么。

重试路径要单独讨论。Stripe 的幂等请求文档介绍了用幂等键帮助避免 API 重试时重复执行操作的机制。它只适用于文档所支持的请求及其具体行为，不会自动让 Harbor 后续的权益更新、邮件或报告任务都变得幂等。要问清楚，跨越这些步骤时，系统如何识别“这是同一次业务操作”。

会议最后应形成实际决定：必须实现哪些行为，哪些假设由谁接受，哪些证据尚在计划中，以及谁有权放行。尚未运行的测试仍叫计划；其他实现版本的演示，仍然只说明那个版本。这些区分可以避免验收变成仪式，同时也允许团队诚实地开展范围有限的试点。

8. 按错误承诺的代价，决定投入多少验证工作

当目标性质清晰、错误后果重要、团队又能长期维护规格时，形式化验证才更值得投入。权限决策、范围明确的分配规则，可能是较容易收窄的起点。一个持续变化、连成功标准都模糊的完整产品，不适合作为第一次尝试的范围。

问清楚，为这项工作拨出资源，意味着停止、增加或推迟什么。小团队眼前最有价值的行动，可能是澄清权益政策，补上缺失的服务端权限检查，而不是研究新的证明工具。这是工作顺序的选择，不说明证明没有价值。反过来，如果同一个关键决策总在反复修补，而团队又有合适的专业能力，就可能值得采用更强的方法。

可以考虑三种选择。开展探索：有一个错误代价高、能够准确表达的性质，也有技术负责人评估适用性。先借鉴审查方法：技术栈或使用条件不匹配，但需求确实模糊。暂缓采用：功能当前最大的不确定性来自客户需求、主观质量，或根本不在拟验证范围内的运维依赖。

不要把 AI 输出的不确定性，和输出外围的确定性规则混为一谈。Harbor 可以用模型撰写报告，但谁有权下载报告是另一个问题。访问决策经过证明，不能说明报告内容正确、及时、有用，或值得购买。后面这些承诺，要用适合内容本身的证据去评估。

第一份交付物可以是一段范围收窄的说明，而不是采用某工具的命令：“我们先审查已就绪报告的工作区权益决策，并明确账单证据不可用时的处理。”工程师据此才能评估可行性；创始人也能判断，这项投入是否真的对应了产品最大的未决风险。

9. 限定上线承诺，并规定何时重新审查

发布决定应以审查表里尚未解决的问题为依据。如果缺失规则可能暴露其他工作区的报告、正向权益尚未定义，或关键依赖假设无人负责，就应阻断敏感客户场景的推广。如果剩余不确定性已经清楚，且试点人群与数据条件适合，可以考虑有限的内部试用。这些是建议的决策规则，不是安全保证。

如果功能上线，要准确描述检查了什么。“我们在已记录假设下验证了指定的访问决策，并测试了交付路径”，比“我们的 AI 应用已经在数学上没有漏洞”更有信息量。即使是前面那句较窄的描述，也只有在团队真的具备相应证据时才能使用。本文不会赋予读者的应用这种资格。

列出必须重新审查的变化：取消政策调整、引入新身份服务、修改账单事件处理、增加分享入口，或改动规格本身。证明可能依旧成立，但产品已经开始承诺另一件事。绿色结果没变，不能替未审查的客户预期变更放行。

分别观察有用的成功和有害的失败。合法客户完成旅程、不合法请求被拒绝、未解决案例，以及恢复结果，分别反映产品的不同方面。定义统计分母，别把成功访问减少误读成安全提升。这些是建议观察的项目，我们没有采集 Harbor 或 PDD Kit 的实际结果。

在 AI 能产出更多实现的今天，PDD Kit 为认真审查需求提供了及时的理由。创始人的下一步很具体：挑选一个后果重要的功能，把客户应得的结果写在限制旁边，再请团队说明每项结论到哪里为止。这样，发布讨论才能围绕客户真正拿到的产品展开，证据也才能与承诺相匹配。

参考资料

• 微软研究院：PDD Kit 演示，2026 年 11 月 5 日。
• GitHub Next：PDD Kit 项目及当前范围。
• Verus 源码仓库。
• Verus 指南：概览与排除范围。
• GitHub Next：Chopin 研究原型。
• OWASP：授权指南。
• OWASP：身份认证指南。
• Stripe：Webhook 事件送达行为。
• Stripe：幂等请求。