paxi VS awesome-distributed-systems

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/

Distributed systems is a very broad research topic nowadays, so it might make sense to check conferences covering a narrower topic, e.g. Cloud computing. Google Scholar might give some useful results for more specific search terms.

The reading lists for distributed systems university courses might also be interesting as well as this "awesome" link list on github:

https://github.com/theanalyst/awesome-distributed-systems

I would this link if anyone is ever looking - https://github.com/theanalyst/awesome-distributed-systems

And do not miss https://github.com/theanalyst/awesome-distributed-systems

https://www.cs.rutgers.edu/~pxk/417/readinglist.html

https://github.com/theanalyst/awesome-distributed-systems

https://dancres.github.io/Pages/