Using TLA+ to prove EC

[sternhenri]

@jbenet and @porcuquine talked about TLA+ and the utility of checking EC, PoReps and other algorithms with TLA+. Here's some about TLA+ if the idea seems attractive.

From Lamport:

• Intro to TLA+: https://www.youtube.com/watch?v=-4Yp3j_jk8Q
• TLA+ course lectures: https://www.youtube.com/playlist?list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD (the outfits, i can't even -- <3 troll)
• TLA+ guide: https://lamport.azurewebsites.net/tla/tla2-guide.pdf

This one is pretty good and approachable from a practicality perspective:

• Intro: https://www.youtube.com/watch?v=_9B__0S21y8
• Guide: https://learntla.com

PlusCal:

• http://lamport.azurewebsites.net/tla/pluscal.html

Good first intro:

• https://pron.github.io/posts/tlaplus_part1

[sternhenri]

We are moving forward with TLA+ training. More to come...