learning:start

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Learning TLA+ and Model Checking ======

This page lists some external resources one could use to learn more about TLA+ and related topics.

First things first: 


  - Setup your IDE. Visual Studio code with tlaplus plugin [[using:vscode|tlaplus plugin]] is recommended. 
  - If you have questions or if you feel stuck at any point, reach out to the [[:community|community]].

Then as good kickstart to TLA+, start with [[https://www.youtube.com/watch?app=desktop&v=tw3gsBms-f8|Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1]] and [[https://www.youtube.com/watch?v=8-Bc5Lqgx_c|Part 2]]. It is a good introduction on TLA+ and uses Paxos and Consensus as an example.

After that, you can start digging into Lamport’s video course available on the [[https://lamport.azurewebsites.net/video/videos.html|website]]. If you prefer a written medium, [[https://lamport.azurewebsites.net/tla/book.html|Specifying systems]]: by Leslie Lamport is still the reference book for TLA+ and its tools. It’s well written and easy to follow.

After learning some TLA+, it might be helpful to start learning some Pluscal. Checkout the [[./pluscal.md|pluscal]] page for more info and some resources.

Don’t just learn the theory, start by solving some small [[learning:exercises|exercises]].


----

  * [[https://members.loria.fr/SMerz/papers/tla+logic2008.pdf|The Specification Language TLA+]]: Another good manuscript by Stephan Merz explaining TLA+ specification language: Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. The fnal Sect. 7 contains some concluding remarks.

===== Resources =====

A collection of resources about TLA+ can be found on the [[https://github.com/tlaplus/awesome-tlaplus|awesome-tla+]] repository. Feel free to contribute with your useful links.

<nspages -tree -r -exclude -subns -pagesInNs -h1 -textNs="Browse Topics:">