Using TLA+ to prove EC - Githubissues

filecoin-project / consensus

Filecoin consensus work

Other

42 stars 5 forks source link

Using TLA+ to prove EC #33

Open sternhenri opened 5 years ago

sternhenri commented 5 years ago

@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 commented 5 years ago

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