Implement formal model for Swarm's syncing protocol with TLA+

[nonsense]

At the moment we don't have a formal model of Swarm's syncing protocol. We have it documented in the Orange Papers, and @gbalint made a presentation on it, and then we have the implemented code in swarm-network-rewrite.

I believe it would be very beneficial to implement a formal model of the protocol with TLA+, so that we can run it through a model checker, with at least a small number of nodes, so that we:

1. Have a simpler explanation and formal documentation of the protocol.
2. Have higher confidence level that the protocol works and that our assumptions hold.

Here are a few resources for those of you who are not aware of TLA+:

1. TLA+ homepage - https://lamport.azurewebsites.net/tla/tla.html
2. Use of formal methods at AWS - http://lamport.azurewebsites.net/tla/amazon.html
3. Elastic.com (ElasticSearch) use of TLA+ to model the consensus algorithm within ES - https://www.elastic.co/elasticon/conf/2018/sf/reliable-by-design-applying-formal-methods-to-distributed-systems
4. Tackling concurrency bugs with TLA+ - https://www.youtube.com/watch?v=_9B__0S21y8 - by Hillel Wayne https://twitter.com/hillelogram
5. Leslie Lamport's video course on TLA+ - https://lamport.azurewebsites.net/video/videos.html

It goes without saying that a formal model of the protocol does not guarantee that we will implement it correctly in Go (or whatever) code, but I think it will be much easier to have a correct Go implementation once we have a defined formal model which does not trigger errors on the model checker.

Let me know what you think.

cc @zelig @nagydani @homotopycolimit

---

Here are a few repos with more elaborate examples:

1. Dockerfile for TLA+ toolset - https://github.com/talex5/tla
2. https://github.com/elastic/elasticsearch-formal-models
3. https://github.com/ahelwer/tla-experiments
4. https://github.com/Shopify/ghostferry/tree/master/tlaplus