Rapid Prototyping a Safe, Logless Reconfiguration Protocol for MongoDB with TLA+

In 2019, MongoDB's replication team embarked on developing a new, safe reconfiguration protocol for their database systems, addressing the known bugs and limitations of the existing legacy protocol. This new protocol, designed to be logless and to minimize changes to the existing gossip-based system, had to ensure high availability and fault tolerance when dynamically reconfiguring replica sets. By utilizing formal specification and model checking tools like TLA+ and TLC, the team rapidly iterated on their design, ensuring rigorous correctness while simplifying the protocol's implementation. The resulting protocol demonstrated novel performance benefits by decoupling reconfiguration from the main database operation log and enhanced reliability by eliminating the need for dual protocol maintenance. Since its implementation in MongoDB 4.4, the protocol has proven robust and reliable, serving as a foundation for additional features while avoiding major bugs, thus underscoring the value of formal methods in protocol design and optimization.