TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

TLA Homepage
Language
Projects
- TLA+ Tools
- TLAPS: A TLA+ Proof System
Community
TLA+ Search

Search for:

TLA+ Search

TLA+ Google Group

How to collect all states of a behavior? August 10, 2018
How to make a concrete value from RandomElement? August 9, 2018
why `init` will invoke twice August 9, 2018
How to set a default for CHOOSE? August 8, 2018
TLC does not finish, how to debug August 3, 2018

TLA+ Project News

TLAPS Project News

Latest Tweets

RT @lemmster: Quick show of hands if you have relied on TLC's checkpointing within the last year. #tlaplus

7 days ago
RT @daniel_bilar: Instructive: Smoking out concurrency bugs in Java by @Hillelogram via @gnat https://t.co/kSbVj43OJM [TLA+ formal ve… https://t.co/vXgW6nV55n

2 weeks ago
Recordings of last week's #tlaplus community event in Oxford have been made available: https://t.co/aIH6quCB5e

3 weeks ago
RT @lemmster: Anybody has strong feelings about discontinuing support for Java 8 with the next/upcoming TLC release 1.5.8? #tlaplus

3 weeks ago
TLA+ Toolbox 1.5.7 has been released: https://t.co/G9muFEzcp0

3 weeks ago

Proudly powered by WordPress