来自Marc's Blog的文章：不变性是推理算法、数据结构和分布式系统的强大工具。对于您设计或实现的任何复杂系统或算法，都值得考虑一组不变性。以这样的方式构建您的实现也是值得的，即使是全局不变性也可以轻松地以确定性和可重复的方式进行测试。
示例：系统设计
在使用 AWS Lambda 的容器加载系统时，我们需要确保在垃圾收集期间不会丢失块。这种高并发的大规模分布式系统可能非常难以推理，因此我们需要从一组不变量开始思考。正如我们在论文中所说：
过去的分布式垃圾回收经验告诉我们，这个问题既复杂（因为块引用树是动态变化的），又有独特的风险（因为这是我们系统中删除客户数据的唯一地方）。
尽管如此复杂，系统不变式却相对简单：
- 所有新的数据块都被写入处于活动状态的根中。
- 所有读取的数据块都在活动状态或已停用状态的根下。
- 根以单调的方式在激活、退役、过期和删除状态中移动。它们永远不会在这个状态链中向后移动。
- 只有被过期根引用的数据块才能被删除。
- 只有当根的所有块都被删除后，根才能移动到已删除状态。
只要系统保留了这些不变式，即使面对任意的并发和规模，也不会丢失任何数据。这几个不变式比完整的系统实现更容易推理，把它们写下来后，我们就能提出一个清晰的形式论证，说明为什么这些不变式是足够的。
示例：分层导航HNSW
Hierarchical Navigable Small World Graphs（层次可导航小世界图）是一种流行的数据结构，用于在大量高维向量集上执行近似 K 最近邻搜索。HNSW 的核心概念并不难，但推理起来却比我们日常接触的大多数算法都要困难。向量的大尺寸、大数据和图连接的复杂性使得在调试器中对 HNSW 进行推理非常困难。
但是，通过对不变式的思考，我们可以发现许多实现上的错误。插入新元素后，数据结构中哪些事情必须为真？向下传递到搜索每一层的入口点集合必须符合哪些条件？
例如
- 入口点必须出现在最高层。
- 每一层都是上一层的子集2。节点不会随着层数的增加而消失。
- 每个节点都可以从入口点的最高处进入。
- 所有节点都出现在第 0 层。
- 每一层大约比上一层大 e 倍。
其中一些不变式的测试成本相当高，比如最后一个需要 O(N log N) 的工作量。在生产实现中的每一步都断言这些不变式并不总是切实可行的，但在单元测试中测试这些不变式却非常实用。我的经验是，推理、列出并测试这样的不变量，是比通过接口测试更好的测试方法。
实例：Paxos
Paxos 是出了名的难以推理。我不会假装自己觉得它很容易，但我相信人们之所以费尽心思，是因为他们没有足够重视《Paxos 简明教程》的第 2.2 节。在这一节中，Lamport 逐步阐述了实现共识的一系列不变式。首先是一些不正确的变量：
P1.接受者必须接受它收到的第一个提议。
在确定正确的不变式之前，需要分层请求。值得注意的是，在这一发展过程中，不变式从可以在单个节点上轻松断言的东西，转变为整个系统的更大属性，而这种属性只能由某个无所不知的更高权力机构来真正断言。
在实际系统中，甚至在集成测试中，都很难实现这种全知全能。在像 TLA+ 的 TLC 这样的模型检查器中，这是很微不足道的，但这对真正的实现并没有多大帮助。全知断言全局不变式是确定性模拟测试（如动荡）所赋予的最强大能力之一。在模拟器中，你可以停止时间，检查不变式，然后确定性地向前滴答。这里的 "你 "指的是测试。与调试器不同，测试可以轻松实现自动化和重复性。它们还能检查人类永远无法在头脑中保持正确的东西。
比如 Paxos 的关键不变式：
P2c 。对于任意 v 和 n，如果发布了一个值为 v 且编号为 n 的提案，那么存在一个由大多数接受者组成的集合 S，该集合 S 要么 (a) S 中没有接受者接受过编号小于 n 的提案，要么 (b) v 是 S 中接受者接受的所有编号小于 n 的提案中编号最高的提案的值。 |
Multipaxos、Raft 以及几乎所有其他分布式协议都有类似的不变式。在我看来，对它们进行推理并自动测试是一种未得到充分重视的超级能力。
总结
事实证明，在编写密集的算法代码、捕获业务逻辑以及实现分布式系统时，它非常有用。这也是十年前TLA+强烈吸引我的原因之一。TLA+思考正确性的方式都是基于全局不变量。