如果将设计本身视为一个可分析的系统，那么在编写代码之前就可以发现一些最严重的系统缺陷。这正是 Hillel Wayne 演讲的主题：他解释了形式化方法的原则如何帮助检查未来的系统，并在问题演变为运行时错误之前发现弹性、并发和故障方面的问题。
Wayne从一个他称为“任务执行器”的简化示例开始：系统检查任务是否已经完成，然后标记完成，之后执行任务。这个顺序看似合理，但在执行过程中发生故障时就会崩溃。如果任务在被记录为完成后发生重试，任务实际上可能不会被执行。将完成记录移到执行之后，则会出现另一个问题：两个并发执行器可能在任何一个执行器记录完成之前都执行同一任务，从而导致任务被执行两次。
这不仅是理论问题；演讲将其与包裹发送系统可能重复发送订单、调度系统可能将同一预约安排给两个人，以及应用安装机制在请求重复时可能进入破坏性行为等示例联系起来。
从定义“正确”意味着什么开始
Wayne建议将系统要求表述为二值性质：要么为真，要么为假。例如，任务不得执行超过一次，这是防止坏事发生的安全性质；任务至少执行一次，这是确保所需事件发生的活性性质。
演讲强调，性质的强度并不相同。能够每秒处理10,000个查询的系统，会自动满足每秒处理两个查询这一性质，但反之则不成立。因此，通过一项强性质可能证明一组较弱性质都成立，而较弱性质失败则有助于缩小故障原因的范围。Wayne将这一思想与测试金字塔联系起来：大量单元测试可能比数量有限的端到端测试更有助于诊断错误。
简化模型揭示核心问题
Wayne不主张完整呈现系统的所有细节，而是建议构建一个抽象模型，仅包含必要的最少状态：算法当前所处的阶段、任务是否已被标记为完成，以及任务执行的次数。这样就可以探索可能的状态和系统可能经过的路径，包括故障和重试状态。
在形式化方法中，可以使用逻辑公式对这一模型和这些性质进行编码，然后使用模型检查器和SMT求解器等工具进行检查。但演讲中的实用思想并不要求直接使用这些工具；工程师可以通过跟踪状态和可能的转换来采用同样的思维方式。
并发与故障中的“敌手”因素
Wayne建议将每个不确定性来源，例如用户输入、并发、随机性、超时和服务器中断，都视为一个总是选择最坏可能结果的“敌手”。如果系统可能无限重试，那么这个敌手就会每次都选择故障，从而揭示出活性性质并没有得到保证，即使理论上成功是可能的。
他还说明，存在并发执行器时，需要将一些变量表示为每个进程本地的变量，将另一些变量表示为系统与外部世界共享的变量。通过探索不同的执行顺序，可以到达任务被执行两次的状态，即使每个执行器单独看来都是正确的。
假设是设计的一部分
系统的正确性不仅取决于其性质，还取决于它运行环境的假设。某种设计可能需要一个关于进程绝不会发生故障的强假设，而另一种设计则可以在故障只发生有限次数的情况下运行。Wayne指出，重新安排步骤可能减轻对活性的假设，但也可能增加安全性要求，例如需要保证同一时间只有一个执行器。
当运行环境发生变化时，情况也会改变。依赖数据库的强一致性，然后转向最终一致性，可能会使此前成立的性质不再得到保证，即使系统代码没有变化。因此，不应将服务提供商或数据库的假设视为外部细节；它们是设计正确性的直接条件。
实际会发生什么变化？
这种方法的实际价值并不在于取代测试，也不在于主张每个项目都使用形式化工具，而在于使设计问题更加严谨：可能有哪些状态？事件最糟糕的排列是什么？我们真正能够控制什么？哪些假设是团队无法保证的？所需性质越强，或者环境越不可预测，系统就越需要复杂的设计，或者需要放宽所需性质，例如将“处理所有消息”这一条件改为“处理消息，或将其发送到死信队列”。
Wayne将这些思想作为源自形式化方法的思维工具来介绍，而不是将其视为可以直接取代工程判断的现成方案。每个系统仍然面临一个开放问题：所使用的模型和假设有多准确；如果遗漏了某种状态，或团队假设了环境并不保证的行为，那么分析可能证明的只是一个与真实系统并不相像的模型是正确的。