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 251 topics
Parsing Error in Consensus.tla Christian Spann 1:33 AM
Formal methods for the application programmer Andrew Wilcox 12:24 AM
[Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT) Cheng Huang 6/28/16
The quantity of mathematics fl 6/27/16
Proving partial correctness of the SetGCD algorithm in the hyperbook Jens Weber 6/25/16
Ethereum Heist Ron Pressler 6/17/16
Announcing Sbuilder - a tool to generate TLA+ model for business IT systems jarjuk 6/16/16
Function domains in TLAPS Ron Pressler 6/14/16
Peano.tla fl 6/9/16
specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface Jason Aten 6/6/16
pvs, temporal logic and stacks fl 6/6/16
TLA in InfoQ article Matt Singletary 5/24/16
Using TLA+ for data modeling Chris Newcombe 5/22/16
TLC and RealTime Chris Pacejo 5/21/16
Robin Milner Space and Motion of Communicating Agents Frank Colcord 5/16/16
introducing "Dr. TLA+ Series" Cheng Huang 5/14/16
modeling resets Brian 5/12/16
Very simple question by TLA newcomer Petar Vukmirovic 5/8/16
Why Amazon Chose TLA+ Chris Newcombe 5/8/16
TLA Toolbox: installation problem Dr. Tianxiang Lu 5/4/16
More topics »