Skip to content
forked from ongardie/raft.tla

TLA+ specification for the Raft consensus algorithm

Notifications You must be signed in to change notification settings

styvane/raft.tla

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

11 Commits
 
 
 
 

Repository files navigation

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 https://github.com/ongardie/dissertation .

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 https://creativecommons.org/licenses/by/4.0/ .

About

TLA+ specification for the Raft consensus algorithm

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • TLA 100.0%