主要观点：在 MongoDB 中进行一致性检查，2020 年作者与同事对两个产品进行实验，包括 trace-checking 服务器和生成 MongoDB Mobile SDK 的测试用例，虽实验有失败教训但仍认为 trace-checking 有价值，后续五年该领域有进展，如多种测试用例生成和 trace-checking 技术的改进。
关键信息：

• 介绍 eXtreme Modelling 软件方法，包括多规格建模、随实现演化等，用于解决一致性检查问题。
• trace-checking 实验中选择 RaftMongo.tla 规格测试 MongoDB 服务器，通过随机测试、收集执行轨迹等步骤，虽失败但得出重要教训。
• Max 用测试用例生成法检查 MongoDB Mobile SDK 的 Operational Transformation 实现，发现算法中的 bug 并实现 100%分支覆盖。
• 后续五年在测试用例生成和 trace-checking 技术方面有诸多进展，如不同语言的相关系统和工具开发。
  重要细节：
• MongoDB 通常部署为副本集，通过 Raft 类似协议达成共识，RaftMongo.tla 规格检查相关不变量。
• 实验中为 MongoDB 服务器添加追踪代码，用 Python 脚本生成 Trace.tla 文件并通过 TLC 模型检查，因难以获取多线程程序状态等原因实验失败。
• Max 手动将 MongoDB Mobile SDK 的 OT 算法从 C++翻译为 TLA+，用模型检查器输出状态图生成 C++单元测试，实现高分支覆盖。
• 后续进展中各技术在不同语言和系统中的应用及改进，如 Mocket 系统、多粒度规格等。