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 424 topics
Doubt about refinement Pedro Paiva 2/20/18
new to TLA: difference between if-then-else and logic or Yong Liu 2/19/18
Google Summer of Code Stephan Merz 2/19/18
TypeOK => TypeOK' with no other assumptions 2/19/18
Spec Review Request Jamie White 2/14/18
Hard Drive Usage 2/14/18
Help with proving an obligation 2/13/18
cannot install tlaps Nobutaka Toyoda 2/10/18
Pedro Paiva 2/10/18
Is possible to use TLA+tools to generate test cases on implemenetation jarjuk 2/9/18
The function return the index of element in a queue the anh pham 2/6/18
TLA+ Toolbox 1.5.6 release Markus Alexander Kuppe 2/2/18
Why Amazon Chose TLA+ Chris Newcombe 2/1/18
Verification of Temporal Property Stephen 2/1/18
MIT license? Michael Collins 1/29/18
What is a TLA formula and a Temporal formula? Stephen 1/27/18
Modelling thread preemption Catalin Marinas 1/26/18
TLAPS and primitive-recursive functions Andrew Helwer 1/23/18
TLA+ parser (Haskell library) Reto 1/22/18
Confusion on "invariant under stuttering" Stephen 1/20/18
More topics »