Comment by ngruhn

To me the modeling is not that hard but I struggle to come up with properties/invariants.

Take something like Google Docs. I'm sure they have some websocket protocol to handle collaborative text editing:

- establish connection

- do a few retries if connection is lost

- always accept edits even when there is no connection

- send queued edits when connection is back

- etc

But what properties can you imagine here?

We never enter an error state? Not really. Error states are unavoidable / outside the control of the system.

We always recover from errors? Not really. Connection might never come back. Or the error requires action from the user (e.g. authentication issues).