3 ms·

Nice to have the TLA+ spec in the repo. Though it doesn't have the details on leader election. https://github.com/xline-kv/Xline/blob/master/curp/tla%2B/curp.t

• thamer 3y ago
  For those interested in this sort of thing, see also Raft's TLA+ specification: https://github.com/ongardie/raft.tla https://github.com/ongardie/raft.tla
• b0in 3y ago
  The CURP paper doesn't define a new leader election algorithm and assumes you use an existing one like raft¹. Xline is using raft based on the readme https://github.com/xline-kv/Xline/tree/master/curp/tla%2B https://github.com/xline-kv/Xline/tree/master/curp/tla%2B ¹warning, I skimmed and ctrl-fd for "leader election"