tikv / raft-rs

Raft distributed consensus algorithm implemented in Rust.
Apache License 2.0
2.86k stars 391 forks source link

Provide formal specification and verification using TLA+ for Raft #539

Closed wego1236 closed 3 months ago

wego1236 commented 3 months ago

We've made a formal specification for Raft in paper "In Search of an Understandable Consensus Algorithm" and a certain scale of model checking to verify the correctness of raft-rs(currently still running). There may exist differences between our specification and Raft in paper or in implementation. Please let us know flaws of specification if you have any question.

wego1236 commented 3 months ago

Okay, I'll go now.