raft VS rqlite

Author seems to be using https://github.com/ailidani/paxi for actual implementation and proof.

I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright

The issue is that rust is a very large language and it's hard to get it right.

I have a python implementation of raft over here:

https://github.com/adsharma/raft/tree/master/raft/states

That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages.

The issue with TLA+ proofs such as:

https://github.com/fpaxos/raft.tla

is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec.

So how do we check and transpile?

* https://www.philipzucker.com/Modelling_TLA_in_z3py/

https://github.com/adsharma/raft

Bug reports welcome

Seems like you could do the same with rqlite [1], since SQLite supports JSON.

[1]: https://rqlite.io

rqlite[1] creator here, happy to answer any questions about rqlite, this latest release, and how it works.

[1] https://rqlite.io

I found simple distributed RQlite https://github.com/rqlite/rqlite based on raft and sqlite. How hard is to add it?

rqlite[1] creator here, happy to answer any questions. rqlite also supports read-only nodes, which can also help with reads at the "edge". It probably wouldn't scale to 100s of nodes, it is an option.

"rqlite supports adding read-only nodes. You can use this feature to add read scalability to the cluster if you need a high volume of reads, or want to distribute copies of the data nearer to clients – but don’t want those nodes counted towards the quorum. These types of nodes are also known as non-voting nodes."

[1] https://rqlite.io/

[2] https://rqlite.io/docs/clustering/read-only-nodes/