Presentation: How to Find Resilience Bugs in Systems that Don't Exist

如何在尚未存在的系统中发现弹性漏洞 - InfoQ

InfoQ 首页 演讲 如何在尚未存在的系统中发现弹性漏洞

架构与设计

InfoQ 认证的AI辅助工程计划（在线，10月19日）：构建支撑工具的框架。

如何在尚未存在的系统中发现弹性漏洞

点赞

新下拉阅读列表

• 阅读列表

查看演讲

• 垂直

• 水平

• 全屏

速度：

• 1x

• 1.25x

• 1.5x

• 2x

44:12

摘要

Hillel Wayne 讨论了形式化方法原理（如属性强度、状态空间验证和环境假设）如何帮助软件工程师尽早发现关键架构漏洞。他分享了实用的思维模型，如“对抗性非确定性”，用于在不依赖复杂数学工具的情况下推理并发、边界情况和分布式系统故障。

个人简介

Hillel Wayne 是《程序员的逻辑》和《学习TLA+》的作者。他通过严谨的设计和验证帮助公司更高效、更低成本地构建系统。

关于会议

软件正在改变世界。QCon伦敦通过促进知识和创新在开发者社区中的传播，赋能软件开发。作为以实践为导向的会议，QCon专为技术团队负责人、架构师、工程总监和项目经理设计，这些人群在团队中影响着创新。

INFOQ 活动

• 2026年10月29日，东部时间下午1点 从Token到功能：为AI辅助工程构建成本归因架构 演讲者：Martin Reynolds - Harness首席技术官，Barani Mohandoss - Trimble云治理、FinOps与E-工具总监

演讲实录

Hillel Wayne：我的工作有点奇怪。公司支付我来查找尚未存在（或更准确地说，尚未构建完成）系统的漏洞。他们带着想要构建的系统构想来找我，但又担心系统出错会导致客户流失，于是请我检查他们的描述，看看是否存在严重漏洞。在极限编程和敏捷团队成长的经历让我最初觉得这种做法是禁忌。毕竟，我们都知道只有在拥有完整可测试的代码系统（可能在生产环境中）时，才能发现漏洞。实际上，这对我们所有人来说都是一个相对简单的流程。为了证明这甚至可行，让我们通过“事务执行者”示例来演示。

事务执行者执行某个事务。它首先检查该事务是否已被标记为完成。然后将其标记为完成。最后实际执行该事务。有谁想指出这个事务执行者的问题吗？没错，你发现了尚未存在系统中的漏洞。问题在于我们都知道实际系统不会这样运作。真实系统会像这样运作：执行事务可能失败。如果失败，我们需要重试。重试时，我们会检查事务是否被标记为完成，发现已被标记，于是就永远不会再执行该事务。这就是一个漏洞。客户可能尝试通过修改流程来修复这个问题：先执行事务，然后再标记为完成。这样即使失败重试，事务仍会被标记为完成，因此可能最终能完成执行。

这引入了一个新的漏洞。即使我们完全消除其失败的可能性，这个漏洞依然存在，它就是“双执行者”漏洞。当存在两个执行者时，第一个执行者可能完成某个操作，但在此标记为完成之前，第二个执行者可能启动并执行相同操作，导致该操作被重复执行。这也会引发另一种类型的漏洞。在座各位中，有谁构建过类似“执行者”的系统吗？因为这是一个非常现实系统的抽象版本，我在设计中经常看到这种系统。在现实世界中，我也多次目睹这种系统失败。我曾见过包裹发送系统最终以一半价格向用户发送两份包裹，这对消费者来说是好事，但会让公司感到沮丧。我也见过排班系统意外地为同一时段分配两个人，我真不想在别人耳边大喊大叫地解释我的观点。

虽然我可能想聆听他们的演讲，这会让我难以发表自己的观点。我甚至见过最糟糕的情况：某个系统允许用户在设备上重复安装同一款应用，这似乎不如前两种情况严重。我想到一个特定的系统，当它试图安装某个应用时，如果用户要求安装相同的软件，它会先停止运行，然后在设备上随机删除文件。

范围 - 形式化方法

希望我已经说明，我们都能在系统描述中隐含而直观地发现漏洞。我的工作是对这一过程的显式化，它被称为形式化方法。其核心思想是将系统用数学符号进行编码，然后通过工具探索整个状态空间来发现系统中的错误。我从事这项工作已有8到10年时间，并经常谈及它。我从中发现了两件事：第一，任何关于形式化方法的演讲只能有一个结论，那就是你应该尝试形式化方法。不过，这其实是一个非常糟糕的会议演讲，因为大多数工程师并不需要形式化方法，就像大多数工程师不需要学习图形编程或地理信息系统一样。形式化方法对某些人非常有用，但对更多人来说并不必要。第二，使用形式化方法改变了我对常规软件的看法，我认为这种改变对人们理解软件开发非常有价值。

与其谈论形式化方法本身，我更想分享从形式化方法中学到的、在日常编码中应用的理念。我们将探讨三个不同方面：属性、验证和环境。或者用更通俗的说法，系统正确性的含义、如何验证这种正确性，以及最初使正确性成为可能所需的条件。

属性

让我们从系统正确性的含义开始。为了形式化这一概念，我们引入了“属性”（property）的概念。属性是正常运行的系统应该满足的条件。如果属性不成立，说明系统存在某种错误，需要修复。值得注意的是，属性本质上是布尔值，要么为真，要么为假，不存在部分为真的情况。例如，系统具备“99.999%（五个九）的可用性”就是一个可验证的属性。如果系统每年停机时间超过5.5分钟，就说明该属性不成立，需要构建更复杂的系统或更换云服务提供商。这个属性虽然重要，但验证起来相对复杂。我们通常更关注那些可以自动验证且易于检查的属性。

一个典型的例子是系统发送的所有消息都符合相应的模式（schema）。建议参考Ian Cooper的演讲，他讨论了如何在系统中强制实施此类属性。属性可以比这更详细，也可以更底层。甚至像单元测试这样的操作本身也是一种属性。例如，测试“max(1,2,3)的输出为3”就体现了“给定输入总是产生特定输出”的属性。如果系统对特定输入没有产生预期输出，说明系统存在问题，必须修复。我们之前讨论的“thing doer”组件在失败时涉及两个属性：一是“不重复执行操作”（安全性属性，防止不良事件发生），二是“至少执行一次操作”（活性属性，确保良好事件发生）。

我之前提到属性是布尔值，这引出了一个非常有趣的结论。设想一个系统能够处理每秒10,000次查询的属性，再设想所有满足该属性的系统集合。现在考虑另一个属性“能够处理每秒2次查询”，并设想所有满足该属性的系统集合。显然，能够处理10,000次查询的系统集合是能够处理2次查询系统集合的真子集。如果一个系统满足处理10,000次查询的属性，那么它必然满足处理2次查询的属性。我们可以将这种关系称为“蕴含”（implication），这是数学中非常有用的结论。

其他满足这种蕴含关系的属性例子包括：如果系统没有内存错误，就必然没有“使用已释放内存”的错误；如果实现了“恰好一次投递”（exactly once delivery），就必然同时满足“至少一次投递”和“最多一次投递”；类似地，符合GDPR合规性意味着网站每个页面都必须有Cookie弹窗。值得注意的是，左侧属性（如“无内存错误”）比右侧属性（如“无使用已释放内存错误”）更难满足。但如果你知道左侧属性成立，就自动意味着右侧属性也成立。这为我们提供了属性强度的概念：左侧属性比右侧属性更强。某些属性比其他属性更强，这对验证工作至关重要。例如，如果我们知道一个强属性（如“用户使用优惠券购买商品的测试通过”）成立，就自动意味着所有弱属性（如“系统处理订单的基本功能正常”）也成立。

你可以使用优惠券并完成订单。如果运行这个测试并通过，那么即使假设性地运行这些测试也无需进行。另一个后果实际上更为重要，即逆否命题的后果。请注意在这个空间中存在三个不同的区域：同时满足10,000和2 QPS的区域、满足2但不满足10,000的区域，以及都不满足的区域。不存在满足10,000 QPS但不满足2 QPS的区域。如果10,000蕴含2，那么2不成立时10,000也必然不成立。如果一个系统在每秒3次查询时就会崩溃，显然无法处理10,000次查询。这被称为逆否命题，并引出了一个非常有趣的结论。如果我们拥有一组较弱的属性，并且知道其中某个属性不满足（例如实际上无法添加运费），那么我们甚至无需查看更强的属性，也已知其不成立。

当你试图找出系统的问题时，哪一种更有帮助：知道这个测试失败，还是知道70个测试通过而这个测试失败？哪一种能更有效地定位错误？第二种。在实践中，强属性通过通常表明系统是正确的，而弱属性失败则能解释系统为何不正确。这实际上解释了我们在验证系统时的许多实践方式。回想测试金字塔模型，我们有少量的端到端测试，一些集成测试，以及大量的单元测试。我们之所以这样安排，有诸多原因，但其中一个关键原因是：我们经常需要调试有缺陷的系统，而非验证正确的系统。这意味着单元测试能提供比单个端到端测试更多关于潜在问题的信息，这也是我们通常需要大量单元测试的原因。

在我们的“thing doer”中，我们有两个版本的“thing doer”，两个不同的系统，以及两个属性：我们不会重复执行操作，且至少执行一次操作。现在我们有了这些属性，下一步是找出如何以某种方式表示系统，使其能够验证这些属性或证明其错误。与之前一样，我们可以直观地进行，但此处的目标是找到某种严谨的流程。然后我们可以将这种方法应用于更复杂的系统，其中这些关系可能并不明显。在形式化方法中，我们首先将系统编码为一组逻辑公式，然后将属性编码为另一组逻辑公式（可能是线性或时序逻辑公式）。接着我们尝试运行某种模型检查器、SMT求解器或证明助手来完成验证。

我们不会涉及这些内容，因为再次强调，这并非关于使用这些工具。而是关于像这些工具一样思考。我们如何以一种可验证的方式表示系统？此处的目标是抽象化。我们希望找到一个尽可能简单的系统，能够覆盖预期的行为。最简单的系统相比更复杂的现实系统将具有更少的错误模式。同时，如果小型系统中存在问题，大型系统中必然也存在该问题。如果“thing doer”会失败，“package sender”也一定会失败，而且可能问题更严重。这并非完美，但这是快速发现危险漏洞的一种非常经济的方式。

在最高层次上，执行者所处的实际状态是什么？我将提出三种状态。第一种是，由于我们正在运行一个算法，我们当前处于算法的哪一步。这将是一个枚举值，包括检查（check）、标记（mark）、执行（do）和完成（done）。如果处于检查步骤，意味着我们即将进行检查。如果处于执行步骤，我们即将执行操作或失败。我们还需要一个布尔值来表示是否已将该事物标记为完成。在实际系统中，这可能表现为数据库记录、某个文件或时间戳。布尔值就足以完成这种分析。最后，我们还需要知道该事物被执行的次数。仅仅用布尔值来表示是否完成是不够的，因为我们希望确保它不会被重复执行两次，因此必须使用整数。

这就是我们真正需要的状态，以表示整个系统。从这里可以看出，其实已经有一个非常有用的洞察：步骤（step）和标记（marked）是机器变量，它们是我们自己设计的系统内部状态。而完成次数（done）是一个世界变量，它代表现实世界中的某些外部因素。这种区别对我们非常重要，因为机器变量完全在我们的控制范围内，我们可以按照自己的意愿设计系统，对这些值进行任何操作。而世界变量，我们控制的范围非常有限，我们只能做某些事情，但无法随心所欲。如果我真的想，我可以设计一个系统，让标记从真变为假。但如果完成次数是2，我无法将其改回1。我永远无法撤回这个包裹。

我们已经明确了状态，现在是时候确定系统实际上能够执行哪些操作了。首先要做的是确定系统可能的初始配置。只有一种情况：我们处于检查步骤，未将其标记为完成，且执行次数为零。从这里开始，我们问：在检查步骤中可能发生哪些可能的演化？这是确定性的，意味着在这个步骤中只有一种可能的事件发生。我们将进入标记步骤。我们已经看到标记是假的，因此我们从检查步骤进入标记步骤，而不是直接进入完成步骤。从这里再次只有一种可能的步骤，我们从标记步骤进入执行步骤。然而在这里，我们有两种可能的事件发生：我们可以执行该操作，或者失败。

当从给定时间点、给定系统状态出发时，可能发生多件事情，这被称为非确定性。我们可以进入完成步骤，同时将执行次数设置为1，或者失败并回到检查步骤进行重试，此时标记为真且执行次数不为零。一旦完成这些，我们必须探索这两种可能的状态，确定从这些状态中可能发生什么。这两种情况再次都是确定性的。从右侧状态，我们可以尝试重试，回到检查步骤，但发现它已经被执行过，因此会回到完成步骤。同样地，如果在这里重试，我们会发现它已经被执行过，因此进入完成步骤。如果我们在这里尝试重试，就会回到这里。

这是系统所有可能的配置。我们称其为状态空间。这些独立的个体称为状态，每个状态都有其状态。这个词存在歧义。系统中所有可能的路径称为行为。我会尽量使用“路径”这个词，因为它更口语化，尽管我认为“行为”是更专业的术语。

验证

现在我们有了状态空间，必须验证我们的属性。首先从“我们不会重复做某事”这个属性开始，这要简单得多，因为这就是我们所说的不变量，即在每个状态下都必须成立的条件。我会用数学方式表达为：在任何情况下，执行次数都少于2次。如果你查看实际的符号表示，它们会使用一种奇怪的平方符号，但我会用“always”来明确表达。要验证这个属性，我们只需遍历所有可能的状态，检查是否满足该属性。例如，这里这个状态在0处完成，满足该属性。同样，这个状态、那个状态、那个状态、那个状态也都满足。每个状态都满足该属性，因此该属性成立。至于底部属性，我们称之为活性。

这不是一个状态属性。如果是的话，我们会在初始状态立即失败，因为在初始状态我们尚未执行。实际上这是一个路径属性。在这条顶部路径中，我们进入了一个已经执行的状态，因此这条路径满足该属性。而这条路径则不满足。如果我们进入这里这个状态，即检查为0的状态，我们无法进行任何操作使执行次数变为1。由于至少有一条路径不满足该属性，整个系统也不满足该属性。这在现实世界中可能导致潜在的错误。V1满足一个属性但不满足另一个属性，这是不好的。那V2呢？在V2中，我们采用检查、执行、标记的顺序，而不是检查、标记、执行。新的状态空间如下所示。从状态空间来看，我们现在似乎满足了下方的属性。即使我们失败，在执行步骤后，我们会回到一个仍然可以到达完成步骤的状态。看起来这个属性得到了满足。如果你现在离开，你将被严重误导。

在解释为什么你会被严重误导之前，我们必须讨论另一个属性，即上方的安全属性。我之前说过，当有两个执行者时，这个属性会失败。问题是，我们如何在两个执行者的情况下使用探索状态空间的方法？这涉及两个方面。第一，决定哪些变量是每个进程的局部变量，哪些是整个系统的全局变量。像执行次数这样的世界变量几乎普遍是全局变量。它们在所有进程和外部世界之间共享。另一方面，机器变量可能依赖于其他因素。我将主张这些变量可能在某个地方共享数据库，因此标记将是一个全局变量。每个进程所在的步骤是局部的。每个进程都有自己的步骤，我们从检查、检查开始。标记是一个全局变量，初始值为false，执行次数为0。

下一个问题是，我们如何表示并发性？我们如何决定哪个进程先执行？这正是非确定性。我可以声明蓝色进程先执行，或者红色进程先执行。从这里开始，我可以继续选择红色执行或红色执行。我可以一直这样下去。最终，我会到达一个点，即这个操作已经执行了两次，顺序可能是蓝色、蓝色、红色、红色，或者红色、蓝色、蓝色、红色，或者蓝色。我们可以指出，上述属性并未被“doer mark 2”所满足。这就是属性检查。

不过在实际应用中，我们通常不会用这种方式在脑海中进行推演。原因在于，我们处理的通常不是12个状态，而是800个，甚至更可能是1000万或1亿个状态。这就是工具的工作方式。这是工具可以完成的事情。它的工作原理相同。我们从初始状态开始，然后找出从该初始状态出发的所有可能后续状态，接着在找到的每个状态中重复这一过程。有时这会带我们回到已经见过的状态，这没有问题。这仅仅意味着我们找到了到达同一状态的不同路径。我们继续这样做，希望状态空间是有限的。最终，我们遍历了整个状态空间，并可以检查其属性。我之所以介绍这种暴力分析方法，是因为这就是工具的工作方式。

我认为这是最好的演示，证明这完全可行，而不是魔法。再次强调，这并不是我们通常在脑海中进行推演的方式。当你深入研究形式化方法时，你会逐渐培养出对系统可能出错方式的直觉。这种直觉的运作方式是利用所谓的对抗性非确定性，或者称为“恶作剧者”。你将系统中的所有非确定性来源——如随机性、用户输入、并发性、us-east-1区域在某天早晨是否决定优先处理等——在抽象层面上全部替换为“恶作剧者”。每当遇到非确定性选择时，你都会询问“恶作剧者”应该发生什么，而“恶作剧者”总会给出最糟糕的答案。一旦你足够熟练，你可以在脑海中非常有效地进行这种推演，总是设法找出最糟糕的可能情况。

正是这个“恶作剧者”导致该系统实际上不满足下方的属性。请思考一下，我们从“检查”步骤开始，进入“执行”步骤。这时“恶作剧者”出现了。我们询问“恶作剧者”，应该发生什么？是执行操作还是失败？“恶作剧者”回答：失败。好的，我们又回到这里。再次尝试，我们进入“执行”步骤。我们询问“恶作剧者”，应该发生什么？是执行操作还是失败？“恶作剧者”回答：失败。然后我们回到“检查”步骤，再次进入“执行”步骤。我们观察“恶作剧者”，并得出结论：不，这属性显然未被满足。简单来说，如果我们存在这样的循环，就有可能无限次进入循环而永远无法到达有效状态。这就是简单的情况。

更糟糕的情况是这样的。即使我们移除了失败状态，这种情况也无法满足活性要求。这是怎么发生的呢？我们进入检查状态，然后进入执行状态。这时问题出现了。我们会问：问题，你为什么会出现在这里？这里存在确定性，甚至没有任何可能发生的事情。问题会说，然后你问：问题，接下来会发生什么？问题会回答：比如陨石撞击。或者更现实地说，比如服务器宕机、超时，或者延迟过高导致在期望的时间窗口内没有收到响应，或者任何可能导致系统无法按预期执行的因素。

环境

这让我想到了本次讨论的最后一个方面：环境。环境指的是所有需要为系统正常运行而成立的假设。在最初的执行者设计中，我们需要假设系统永远不会崩溃，以保证活性。这个假设可能合理也可能不合理，但很可能是我们必须接受的。比如尝试点击一个点击器时，你必须假设它总是能正常工作，因为如果在你按下按钮之前它突然起火，这完全是一个合理的错误。如果没有能力声明系统总能取得进展，你就根本无法拥有任何属性。这再次强调了属性是超出我们控制范围的事物。这些假设通常来自我们无法控制的其他系统。如果供应商决定将消息传递方式从始终一致改为最终一致性，你又能怎么办？

你或许可以更换供应商，但无法要求他们恢复旧的行为。这是一个非常合理的假设。如果我们加入失败状态，现在就需要一个更严格的假设：执行操作永远不会失败。这要少得多合理性。如果我看到客户说：“我们只是假设这个操作永远不会失败”，我会直接说：“你的系统存在缺陷”。这可能会促使我们转向使用V2版本。在这种情况下，V2版本不再需要假设执行操作永远不会失败。我们可以采用一个更弱的假设：执行操作仅失败有限次数。即使我们在这一阶段失败一百万次，但在第一百万零一次时，我们仍然会越过这个阶段。我们完成了，已经满足了活性要求。这种非常精细的假设正是形式化方法的强项。它迫使你深入思考系统中涉及的各种类型假设。我还想指出，“执行操作永远不会失败”和“执行操作仅失败有限次数”在定性上非常相似，即使在定量上存在差异。

这又让我们回到强项与弱点的问题上。某些假设比其他假设更强，就像某些属性比其他属性更强一样。零失败比有限失败是一种更强的属性。强一致性比最终一致性是一种更强的假设。当我们拥有更强的假设时，可以在相同系统复杂度下实现更强的属性。相应地，较弱的假设可以通过系统设计进行补偿。我曾经在一家公司工作，我们确信每个用户都会在纽约时间下午4点停止使用我们的软件。这使得部署变得异常简单。我们只需在晚上6点左右关闭所有服务，进行更新后再重新启动。我们拥有一种非常强的假设，使我们能够轻松保证部署属性。想象一下谷歌也这样做。

想象一下这个场景，这会非常有趣。不过，还有一点需要指出的是，不同系统在保证不同属性时需要不同级别的假设。这种关系并非单调递增。系统设计并不必然在相同假设下使所有属性更容易保证。我们在版本2中再次看到了这一点。在版本2中，我们需要较弱的假设来保证活性，但需要更强的假设来保证安全性。我们需要假设同一时间只有一件事执行者在运行。在版本3的执行者中，可能存在不需要这些强属性的情况。它可能仅在有限失败的情况下运行，同时即使存在多个执行者，也能保证安全性。如果这样的系统存在，它可能比版本1或版本2都要复杂得多。

我通过经验发现，系统复杂度、希望保证的属性以及假设强度之间存在某种关系，其中任何一个因素可以固定，而另外两个因素会随之变化。例如，如果你想在相同假设水平下保证活性，比如消息传递的可靠性，是否所有消息都被处理？你实际上可以通过弱化属性来实现这一点。从“所有消息都被处理”弱化为“所有消息要么被处理，要么进入死信队列”。同样，以飞船为例，飞船甚至无法假设RAM会保持一致性。宇宙射线和辐射效应会不断改变RAM的状态。它们需要为相同级别的属性设计更复杂的系统。

另一个后果是，弱化假设往往会削弱你拥有的属性。如果你使用一个固定系统，它能正常运行并保证所有属性，但随后弱化当前运行环境中的一项假设，它可能不再满足原本的属性。我发现这在实践中常常导致大量错误，人们为某个运行环境构建系统时，它能正常工作，但一旦运行环境发生变化，系统就会出现问题。我反复提到这个例子，因为它是我最反感的情况。当客户将数据库从“我们总是立即提供更新信息”改为“我们可能在五分钟之后提供信息，最终会保持一致性”时，我们原本依赖强一致性设计的系统就会失效。当系统切换为更弱的假设时，我们的属性开始失效，而他们的需求可能被满足，但我们的系统却无法满足。这些就是我经常从形式化方法中借鉴的三种视角。

总结我刚才谈到的内容，系统有假设和属性，它们之间存在强弱关系。某些属性比其他属性更强，某些假设也比其他假设更强。对于给定的属性和假设，系统复杂度取决于这两者的平衡。系统需要更复杂的机制来处理更强的属性，但面对更强的假设时却需要更简单的实现。强属性体现正确性，当它们通过验证时，我们就能确认系统是正确的。弱属性体现错误性，它们用于调试问题根源。我们可以通过简化模型发现系统中的真实错误。最后，要警惕“小妖精”（gremlin）。我讨厌这个词，但最终这一切都源于软件的数学分析。我们不必亲自进行这些数学分析，但仍然可以享受它带来的好处。我们在许多领域都看到了这种现象，包括形式化方法、函数式编程和类型系统。我发现这些背后的数学理论非常酷，也很高兴它们能为我们带来如此多的实际好处。

资源

我想谈谈一些资源。如果你听完这场关于形式化方法的演讲后，仍然想学习形式化方法，那我只能说我失败了。我正在开发一个名为learntla.com的资源，旨在教授一种名为TLA+的形式化方法，这种方法在业界相对流行。它非常适合并发系统分析和错误查找。当然，这并不是唯一的形式化方法。这不像Emacs和Vim之争那样存在教条主义的分歧。如果你之后来找我，告诉我你正在使用的系统，我可以判断TLA+是否最适合你，或者推荐其他方法的资源，比如Alloy、P、Quint或PRISM。或者，你也可以直接雇佣我来协助你。

我也这么做。不过，正如之前提到的，我真正着迷的是如何从数学视角推导出对日常软件工程有帮助的洞见。正因如此，过去三到四年我一直在撰写一本名为《Logic for Programmers》的书。这本书涵盖形式化方法，同时也涉及属性测试、状态测试、基于契约的设计、SMT求解和逻辑编程等内容。如果这对你有吸引力，我实际上已经完成了首印版本，使其成为一本可以购买的实体书。如果你感兴趣，可以通过这个链接以优惠10美元的价格购买当前版本的PDF，当最终版本完成时，PDF会自动更新至最终版本。

问答环节

参与者1：你在遗留的混乱系统中应用形式化方法，与从零开始的新项目（Greenfield项目）相比，是否发现有什么不同？

Hillel Wayne：确实如此。在Greenfield项目中应用它要容易得多。在遗留系统中有一个有趣的现象，更容易展示其价值。原因在于，在Greenfield系统中，你很难论证某个发现的特定错误实际上是真实存在的，我们之后可能会发现。而在遗留系统中，你可以这样说明：我建模了我们旧系统中存在这个关键错误，两秒内就发现了它，然后展示：现在我们已经证明它可以发现我们实际遇到的真实错误，那么就用它来建模过去的变更吧。实际上，我就是通过这种方式开始从事这项工作的。当时有一些系统运行得非常糟糕，我们基本上打补丁，结果变得更糟，他们再打补丁，又变得更糟。当我们思考另一个补丁时，我正在研究这些方法。我意识到：我成功地用50行规格说明重现了过去五次导致严重问题的情况。这个新补丁还有其他导致严重问题的地方。我们暂时不要实施它。

Weakly：我好奇的是，当我们谈论这些属性时，当我们谈论证明某些内容时，通常很容易在小而独立的组件中展示、演示或整理这些内容。如果你有多个不同的组件，并希望将它们作为一个整体进行推理时，组件之间无法组合，属性也不一定能够组合。在现实世界中，你发现哪些实用的策略可以解决这个问题？

Hillel Wayne: 一般来说，这在技术领域是一个重大问题。在任何领域中，这都是一个普遍存在的难题。各个组件可能各自独立正确，但它们之间的相互作用可能导致整体系统崩溃。这种现象被称为功能交互或边界错误。Nancy Leveson 写了一本非常优秀的书，名为《Engineering a Safer World》，书中探讨了如何在事故发生后识别这些问题。这基本上是我们目前能做到的最好方式。在形式化方法中，我们可以通过调整抽象程度来实现这一目标。我们可以构建一个高度抽象的系统模型，其中所有组件协同工作，然后通过所谓的“细化”过程，从全局系统中提取一个模块，将其详细化，再将其重新插入到抽象模型中，验证其在其他组件保持抽象状态时的行为是否正确。这个过程可以逐步推进。然而，由于系统复杂性和多层抽象的存在，这个过程非常繁琐且困难。虽然不愉快，但这是可行的。如果这个过程有趣，会有更多人愿意参与。

Participant 2: 你提到假设、属性和系统复杂性之间的相关性。我有时会思考，当假设条件变弱时，是否有时根本无法满足某些属性？有时通过增加系统复杂性反而可以实现。在形式化系统中是否有工具能帮助回答这个问题？是否可以通过调整系统来满足在较弱假设下依然满足属性？

Hillel Wayne: 如果假设条件被削弱，是否可以通过构建更复杂的系统来修复问题，或者这在理论上是不可能的？

Participant 2: 是否可以通过系统修改来实现属性提升，而无需降低原有属性？

Hillel Wayne: 这个问题有两个层面的回答：理论层面和实践层面。从理论角度看，答案是否定的。因为这涉及到如何证明任何事物的问题。确实存在某些方式，通过削弱假设使属性永远无法验证，但要证明这一点并不容易。这又回到了“什么是证明”以及“我们如何证明任何事物”的哲学问题。在实践中，我发现对于给定系统，通过运行多层假设和系统修改的组合分析是可行的。你可以这样表述：在我们的系统设计中，这些属性始终成立；如果满足某个假设，这些属性成立；如果采用更弱的假设，这些属性的弱化版本成立，但强版本不成立；如果某个属性被弱化，系统细化版本可以满足更强的属性。通过工程实践可以实现这些目标，但无法自动推导出某些属性必然无法满足的结论。

Participant 3: 不幸的是，我主要工作在非确定性系统领域，例如智能体或机器学习模型。这些方法在非确定性系统中还能适用多少？是否可以量化解空间的潜在状态空间？是否有方法能帮助在智能体不可避免地陷入失败状态之前发现这些状态？

Hillel Wayne：我认为代理技术面临的挑战在于，它带来了一种我们此前从未见过的非确定性。我们通常认为非确定性是由于现实世界因素的交织导致A或B可能发生。但我觉得AI在某种程度上也存在类似情况，它可能选择A或B。为什么？因为温度参数。目前还没有大量工作将形式化方法应用于确保代理本身正确运行。大部分研究集中在确保代理生成的代码有效，或确保代理运行的流程有效。实际上验证代理自身，目前还没有建立有效的方法。

Participant 3：我在想，如果具备三重组合条件——可以导出内容、能够找到相关链接，以及潜在的组合可能性，比如将三个API组合并赋予代理，可能不会立即报错，但会埋下隐患。

Hillel Wayne：我认为这可以被视为三个API本身的错误。如果人类使用这三个API，是否可能发生错误？如果一个编写质量差的程序使用这三个API，是否可能发生错误？在这种情况下，我认为这是可以验证的。关于代理本身，我无法给出专业回答而不误导你和我自己。我确实不具备相关专业知识。代理和API，这可以说是《龙与地下城》最新版的傻瓜版本。

Participant 4：回到应该具有确定性的系统领域，是否有人尝试从源代码或注释中推导属性或假设？

Hillel Wayne：有。我们可以从多个角度看待这个问题。首先，我们能否从源代码生成规范？实际上已有使用大语言模型进行这项工作的优秀研究。另一个角度是，如果系统是确定性的，可以直接通过代码本身证明其正确性。这涉及到代码形式化验证领域，这是一个充满挑战的复杂领域。例如，你会使用Dafny、Frama-C或SPARK等工具。这可能涉及直接可证明正确的专用语言，或针对现有语言（如Frama-C针对C代码）的增强验证框架，用于证明现有C代码的正确性。

Participant 5：在我工作中，我看到有人使用技能尝试自动化一些初始的漏洞排查和安全审查。在你的经验中，是否有人成功通过技能结合AI采用形式化方法？如果有的话，你看到的是成功案例还是失败案例？

Hillel Wayne：新LLM时代最有趣的事情之一是，它向我们揭示了许多隐藏的偏好。其中一点是，很多人真的想通过在互联网上发布低质量内容来毁掉他人的生活。这也让我意识到，很多人其实很想使用这些形式化方法，只是被进入这一领域的技能门槛所吓退。目前使用LLM编写代码和系统规范的数量大幅增加，这确实是个问题，因为LLM在这方面表现得非常糟糕。当前LLM在正确执行这些任务方面最大的问题是，它们根本无法理解属性。它们完全无法处理活性问题，其安全性属性和不变式通常是这种形式：如果X和Y为真，且已知X为真，那么Y也必须为真。

这种情况可能会改变。这些技术进步得太快、太彻底了，我的判断可能有误。目前要让AI很好地完成这些任务，需要已经有相关经验的人来指导。如果你有经验，它们确实能节省大量重复工作和痛苦，我非常喜欢使用它们。但我也为这种喜欢感到一丝愧疚。

参与者6：你提到自己的形式化方法背景帮助你识别系统中的弱点，那是否也让你形成了构建正确系统的直觉呢？

Hillel Wayne：我认为是的。例如，我现在对任何类型的图数据都充满厌恶，因为循环无处不在。我也明显注意到自己形成了某种直觉，比如：哦，这个系统会失败，因为它存在竞态条件，那我们该如何设计系统来避免这种竞态条件？我觉得自己确实建立了这种直觉，但也有可能这种直觉完全错误，只是我过于自信罢了。我不希望让人觉得只要这么做，你们也会变得精通分布式系统。

参与者7：这会不会很耗时？

Hillel Wayne：是的，这确实耗时。但目标是节省成本，比如用几天时间进行规范定义，就能节省几周的开发时间，或者避免花几周时间向愤怒的客户解释："请不要取消服务，很抱歉我们丢失了您的数据，但不会再发生。"这是一项时间投资。

参与者7：那应该尽早做，这样能节省成本。

Hillel Wayne：确实会很耗时。

查看更多带字幕的演讲

录制时间：

2026年10月14日

由

• Hillel Wayne

#### 相关赞助商

• 《工程领域AI采纳规模化》（O'Reilly出版）- 立即下载

#### 相关赞助商

发现你的测试遗漏的漏洞。Antithesis通过确定性模拟探索数千种故障场景，在漏洞进入生产环境前发现难以复现的错误。了解其工作原理。

#### 本内容属于InfoQ主题

##### 相关主题：

• 开发

• 架构与设计

• 文化与方法

• QCon伦敦2026

• 调试

• 分布式系统

• 并发

• QCon软件开发会议

• 弹性

• 字幕

• 可靠性

• 测试

• 架构

• InfoQ

• 验证

• 相关编辑

• InfoQ热门文章：与Joy Ebertz对话，探讨AI编程的真正含义 GitHub将Copilot运行时迁移到Rust并采用AI辅助重写 调查发现AI生成代码会增加调试和故障率并造成理解鸿沟 Java新闻速递：Grails 8、Open Liberty、GlassFish、Infinispan、LangChain4j、Spock Context 语言模型：通过自我管理上下文提升性能并降低计算成本 本体驱动可观测性：在Netflix规模构建端到端知识图谱