eSpark用TLA+证明没有设计能满足全部3条规则，随后舍弃了其中一条

eSpark Learning是一家面向小学的教育科技提供商，它为每个客户运行一套人工、半定期的配置流程，该流程需要协调多个第三方系统，并直接修改客户的IT网络。随着用户群增长，工作量变得难以为继——支持团队意识到，仅为了跟上进度，每年就需要新增一名全职员工。领导层一直认为自动化该流程过于危险：一个错误就可能触及客户的网络，并导致合同丢失。

工程师Hillel Wayne最近在一个批量上传项目中使用了形式化规约（TLA+风格），通过在编写代码之前捕获架构缺陷，将交付时间缩短了一周。项目经理定义了自动化替代方案必须保证的三项属性，才能确保安全。Wayne用一种规约语言对系统建模，并通过模型检查器运行，模型检查器会穷尽模拟规约允许的每一种场景，并在发现违反规则的场景时返回一条具体轨迹。

经过两天的建模，每一种设计要么立即失败，要么包含一个微妙的缺陷，该缺陷可能在生产环境中潜伏数月而无人察觉，然后才崩溃。有些设计满足了三项必需属性中的两项，但没有一个满足全部三项。Wayne没有随便选一个然后寄希望于运气，而是把项目经理带入建模产物中，具体展示了每种设计将如何失败，并询问业务可以舍弃哪项属性。

内部设计专家确定，有一项属性只需要通常成立，而非始终成立。随着这一单一取舍被缩小范围，模型检查器确认若干设计现在可以工作，团队构建了其中之一。这个自动化配置服务此后多年运行无事故，其存续时间超过了构建它的工程师的任期。

模型检查器证明没有设计能满足全部3条规则；进行协商

用规约语言建模的丢弃成本很低；而一个基本建成的代码库则不然，因此在实现之前测试每一种设计想法，避免了浪费工程时间。

模型检查器返回一条具体的失败轨迹，这比抽象的风险警告更能说服非工程师的利益相关者。

在编写代码之前揭示“这些设计没有一个满足全部三项需求”，将隐含的、未经审视的假设转变为项目经理实际可以做出的明确决策。

当你尝试的每一种设计似乎都失败时，先对设计空间进行形式化建模。模型检查器将模糊的风险感转化为具体的、可协商的取舍，你可以在编写任何代码之前提出。

这个自动化配置管理服务高效运行了多年，远远超过了构建它的工程师的任期。Wayne随后全职从事形式化规约顾问工作，并撰写关于这一实践的文章，包括一本关于该主题的书，以及为Alloy规约语言编写文档的工作。