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 346 topics
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
TLA+ community meeting at FLOC 2018? Stephan Merz 6/1/17
Why Amazon Chose TLA+ Chris Newcombe 5/29/17
Interpreting the DieHarder error trace 5/29/17
Paramaterized Instantiation and Universal Quantification Adam Shimi 5/28/17
Modeling memory barriers Randall Nortman 5/27/17
TLC not handling disjunction correctly in special case? Andrew Helwer 5/24/17
Confusion about the model of the specification of InternalMemory in Chapter 5 "A Caching Memory" of the book "Specifying Systems" Hengfeng Wei 5/23/17
TLA+ Video Course Leslie Lamport 5/15/17
Protocol specification liveness Wan Azlan 5/14/17
More topics »