TLA+ specification for the Raft consensus algorithm
Switch branches/tags
Nothing to show
Clone or download
Latest commit 34cdd49 Aug 22, 2016
Failed to load latest commit information. README: Mention PR#4 Aug 22, 2016
raft.tla Fix AppendEntries to only send one entry at a time Dec 2, 2014

Formal TLA+ specification for the Raft consensus algorithm. This is slightly updated compared to the dissertation version.

For more information, see Chapter 8 (Correctness) and Appendix B (Safety proof and formal specification) in .

If you're trying to run the TLA+ model checker on this specification, check out Jin Li's changes in Pull Request #4.

Copyright 2014 Diego Ongaro.

This work is licensed under the Creative Commons Attribution-4.0 International License .