This is a discussion group for users of the TLA+ specification language, the PlusCal algorithm language, and their associated tools.
To find out about the languages and tools, see The TLA Home Page 
Posts by non-members are moderated.
We encourage you to join the group.

Showing 1-20 of 354 topics
Toolbox beta release with Unicode support Markus Alexander Kuppe 8/15/17
New to TLA, Can't figure out the example work mo jia 8/15/17
Specify and Verifying temporal properties in TLA+ Toolbox jevitha kp 8/15/17
TLA+ Video Course Leslie Lamport 8/14/17
TLA+ and Reals John Baugh 7/25/17
TLA+ Prover Error reza parvizi 7/19/17
Parse Error reza parvizi 7/19/17
TLC choose a new unique element everytime Shuhao Wu 7/14/17
TLA+ Toolbox installation problem Bilal Mustafa 7/6/17
Confused about depth-first search Chris Pacejo 6/27/17
I've been working on a TLA+ guide Hillel Wayne 6/27/17
How can I check if a variable is stable if once set Christian Spann 6/26/17
Novel queue-lock like concurrent spin-lock formalization in TLA+ Steven Stewart-Gallus 6/24/17
PlusCal call-goto enhancement Chris Pacejo 6/24/17
Ability to use Vim keystrokes with TLA+ Toolbox? Thomas Gebert 6/23/17
Pf2 fl 6/22/17
TLA Toolbox: installation problem Dr. Tianxiang Lu 6/18/17
TLA+ theory blog post series + new subreddit Ron Pressler 6/16/17
Proving equivalence of AlternatingBit to ABCorrectness Wan Azlan 6/11/17
Seq({"xxx"}) is not enumerable 6/2/17
More topics »