TLA+ formal specification of Ceph consensus algorithm

Hello, My name is Afonso Fernandes, and I am a student at the University of Porto. I am writing a formal specification in TLA+ of the paxos consensus algorithm implemented in Ceph as part of my master thesis. The specification is in the following repo, along with instructions to run, some description and current results of the model. https://github.com/afonsonf/ceph-consensus-spec I decided to write the specification to better understand the consensus algorithm used in Ceph. Although it is based on paxos, which has detailed formal proofs, the implemented version makes some deviations from the "original" one, making it, in my opinion, somewhat difficult to make a parallel between the two. Therefore, I think a formal specification can be helpful in further development of Ceph. Some of the useful things that can be done with this model are: * Prove safety and liveness properties of the implemented algorithm. Test new versions of the algorithm to see if the properties still hold. * Visualization of the algorithm. Possibility of creating traces of segments of the algorithm and see how the variables change (example: https://github.com/afonsonf/ceph-consensus-spec/tree/main/trace-example). * Make interactive visualizations of the algorithm (such as this one: https://github.com/will62794/tlaplus_animation/blob/master/examples/Elevato…). * Analyse statistics of the state machine generated from the algorithm. * Debug the algorithm. Search behaviours that lead to certain configurations and study what can happen from there. In conclusion, I would like to ask the opinion and, if possible, some criticism or suggestions about the specification (the specification probably has errors because I may have misinterpreted some parts of the code). The main topics that I think I may have got wrong are summarized in the section "Deviations and abstractions from the original source" in the description file: https://github.com/afonsonf/ceph-consensus-spec/blob/main/description.md. Thank you for reading and all the help is welcomed! Best Regards, Afonso Fernandes