This paper demonstrates a framework for distributed protocols. The framework makes it possible to:
- walk through the states of system
- verify invariants of the system
- derive/verify implementations directly from the specifications
Point 3 separates it from other such proof assistants like TLA+ or Coq, which fall short on ensuring that the implementation follows specifications. The paper introduces a few fundamental distributed protocols which can then be combined to create more complex protocols. It uses type classes to make the implementation flexible and extensible.