主要观点：MongoDB 通过副本集提供高可用性和容错性，副本集内的数据库写操作在顺序日志（oplog）中复制并应用到所有副本，共识协议保证多数节点提交的 oplog 条目写入持久化。随着时间推移，需要改变副本集内的服务器集合，即动态重配置，2019 年需实现新的安全重配置协议，在最小化对现有基于闲聊的重配置协议更改的同时，利用 TLA+和模型检查工具快速开发并实现新协议。

关键信息：

• 副本集操作 Raft 类似共识协议，oplog 保证写入持久化。
• 动态重配置是副本集内关键操作，需保证正确性。
• 2019 年开发新安全、无日志重配置协议，以解决现有协议的正确性问题。
• 利用 TLA+和 TLC 快速迭代设计，仅几周就完成设计并几个月内投入生产。
• 讨论了正式建模现有协议、发现并迭代修改以达到安全协议设计的过程。

重要细节：

• 原有基于闲聊的重配置协议与主 oplog 完全解耦，存在安全性问题，需开发新协议。
• 模型检查工具帮助精确刻画现有协议缺陷，引导修改。
• 实验中逐步引入单节点更改规则、配置提交规则、oplog 提交规则等，以解决安全性问题。
• 理解到配置可视为无日志状态机，需为其分配主节点任期等。
• 最终协议通过多轮模型检查和验证，运行可靠，实现和协议比原设计更简单。
• 整个过程仅用一周得到草案协议，两周通过正确性检查，三个月完成实现，证明了正式方法的价值。新协议已在 MongoDB 4.4 中运行数年，无重大协议漏洞。相关论文和规范可在特定仓库中找到。