Formal TLA+ specification for the Raft consensus algorithm, which has been extended to generalize to utilize Flexible Quorums.
For more information, see Chapter 8 (Correctness) and Appendix B (Safety proof and formal specification) in https://github.com/ongardie/dissertation .
Copyright 2016 Heidi Howard. Copyright 2014 Diego Ongaro.
This work is licensed under the Creative Commons Attribution-4.0 International License https://creativecommons.org/licenses/by/4.0/ .