MongoDB的极端建模实践：TLA+规范与实现的一致性检查

MongoDB工程师尝试使用TLA+规范和两种一致性检查技术（追踪检查和测试用例生成）来验证其产品的实现是否符合规范。追踪检查实验在MongoDB服务器上进行，目标是验证Raft共识协议的实现；测试用例生成实验在MongoDB移动SDK上进行，目标是验证操作转换算法的实现。结果表明，追踪检查因多线程程序状态快照的难度和规范与实现的差异而失败，而测试用例生成成功发现了算法中的一个错误，并实现了100%的代码分支覆盖率。该文章总结了经验教训，并介绍了近年来该领域的研究进展，强调了持续一致性检查对TLA+主流化的重要性。