websites for learning TLA+

Wikipedia

https://en.wikipedia.org/wiki/TLA%2B
https://news.ycombinator.com/item?id=9601770

Lamport's homepage

https://lamport.azurewebsites.net/tla/tla.html
https://lamport.azurewebsites.net/tla/learning.html
https://lamport.azurewebsites.net/video/intro.html
https://news.ycombinator.com/item?id=13918648

video tutorial series:
https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD

TLA+ Github

https://github.com/tlaplus/awesome-tlaplus

https://github.com/tlaplus/DrTLAPlus
https://github.com/tlaplus/Examples - includes DieHard4, DiningPhilosophers, Paxos,

https://github.com/dmilstein/channels

https://github.com/tlaplus-workshops/ewd998

https://github.com/Cjen1/tla_increment

LearnTLA.com - Hillel Wayne

https://learntla.com/
https://news.ycombinator.com/item?id=19661329
https://news.ycombinator.com/item?id=33010645

https://www.hillelwayne.com/post/learntla/ -- announcement about revision to book; points to learntla.com
https://news.ycombinator.com/item?id=31952643

https://hillelwayne.com/talks/distributed-systems-tlaplus/

Hillel Wayne - Designing Distributed Systems with TLA+
https://www.youtube.com/watch?v=ATobswwFwQA

Tackling Concurrency Bugs with TLA+ by Hillel Wayne
https://www.youtube.com/watch?v=_9B__0S21y8

• toy example of money transfer in TLA+
• three real-world cases from Hillel's employer of using TLA+ to check design before implementation

@pressron - Ron Pressler

https://pron.github.io/posts/tlaplus_part1
https://pron.github.io/posts/tlaplus_part2
https://pron.github.io/posts/tlaplus_part3
https://pron.github.io/posts/tlaplus_part4

https://pron.github.io/posts/tlaplus-curryon-talk
Ron Pressler - The Practice and Theory of TLA+
https://www.youtube.com/watch?v=15uy9Ga-14I

TLA+ in Docker in VSCode

A gentle intro to TLA+
https://www.youtube.com/watch?v=D_sh1nnX3zY
Demos a three-state system using VSCode

VSCode plug-in using Docker for TLA+:
https://github.com/kevinsullivan/TLAPlusDocker

My video on how to install TLA+ inside Docker as a plug-in for VSCode:
https://www.youtube.com/watch?v=sLGY7_agg4E

Questions and Answers

https://groups.google.com/g/tlaplus

https://stackoverflow.com/questions/tagged/tla%2b

https://www.reddit.com/r/tlaplus

Blog posts

https://elliotswart.github.io/pragmaticformalmodeling/

http://muratbuffalo.blogspot.com/2022/10/checking-statistical-properties-of.html
https://news.ycombinator.com/item?id=33077898

https://www.mydistributed.systems/2022/06/some-practical-tips-on-using-tla-and-p.html

https://thenewstack.io/tla-the-best-debugger-optimizer-youve-never-heard-of/

https://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/
Deep dive into practical use of TLA+ for real software. Links to github repo with Dockerfile

Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch
https://www.youtube.com/watch?v=qYDcbcOVurc

TLA+ Toolbox for Beginners
https://www.youtube.com/watch?v=U2FAnyPygrA

Modeling Virtual Machines and Interrupts in TLA+ & PlusCal - Valentin Schneider
https://www.youtube.com/watch?v=hlLZi4wfBjs
use of TLA+ at ARM

TLA+ Tutorial 2021 at DISC 2021
https://www.youtube.com/watch?v=NXLJoUKJnDQ

Debugging software designs using testable pseudo-code (Jay Parlar)
https://www.youtube.com/watch?v=LAEXHua4MQQ
Alice and Bob money transfer model (from learntla.com)
utility: first motivating example for why TLA+ provides value to design process

A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness
https://www.youtube.com/watch?v=H7yBYoY7ILc

SREcon20 Americas - Weeks of Debugging Can Save You Hours of TLA+
https://www.youtube.com/watch?v=wjsI0lTSjIo
Uses an example written in C that has a rare deadlock.