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 264 topics
Experimenting with PlusCal / TLA+ at Dropbox Elliott Jin 8/25/16
[Dr. TLA+ Series] Fast Paxos - Cheng Huang (Monday, August 29th, 10-11:30am PDT) Cheng Huang 8/23/16
LTL axiomatic system fl 8/15/16
Jumping to end of process in PlusCal? Elliott Jin 8/6/16
TLA+ Video Course Leslie Lamport 7/28/16
Any examples of a specification of an S3-like object store API? Steve Loughran 7/27/16
Next-state involving existential quantifier using PlusCal? Elliott Jin 7/25/16
Ethereum Heist Ron Pressler 7/23/16
[Dr. TLA+ Series] Raft - Jin Li (Thursday, July 21st, 10-11:30am PDT) Cheng Huang 7/22/16
TLA+ community event 2016 Stephan Merz 7/22/16
Mixing TLA+ and SOS Behrooz Nobakht 7/18/16
specify some action eventually will never happen Gao Neal 7/14/16
[Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT) Cheng Huang 7/14/16
Analysis: Runway, a new formal specification system Andrew Helwer 7/5/16
Where is the model value symmetry set specified in the Toolbox? Andrew Wilcox 7/4/16
The quantity of mathematics fl 7/4/16
Formal methods for the application programmer Andrew Wilcox 7/3/16
Parsing Error in Consensus.tla Christian Spann 7/1/16
Proving partial correctness of the SetGCD algorithm in the hyperbook Jens Weber 6/25/16
Announcing Sbuilder - a tool to generate TLA+ model for business IT systems jarjuk 6/16/16
More topics »