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

What this post added

Details the process of formally modeling the legacy gossip-based reconfiguration protocol in TLA+, characterizing its bugs with a model checker, and iteratively developing modifications to lead to a safe, logless reconfiguration protocol design. Explores single-node changes and their limitations, and demonstrates how TLA+ and TLC were used to discover and fix safety issues, ultimately accelerating design and delivery timelines while maintaining a high correctness bar.