A specification of the Chain Replication protocol for storage services written in TLA+ (incomplete).
This project was created for Robbert van Renesse's CS 6480: Systems and Formal Methods class in the Spring 2020 semseter. The original goal was to specify the entire chain replication protocol, but because of the COVID-19 epidemic the semester was disrupted and the project was left unfinished. This is a specification of the client interface to the protocol; I had originally wanted to specify the protocol itself as well and show that the client interface was a refinement of the protcol.