TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

TraceExplorer help text - #393 February 18, 2020 quaeler
TLC help text - #393 February 17, 2020 quaeler
Monolith and variable output improvements - #393 February 16, 2020 quaeler
Improving TLC error message for temporal existential quantifier in sp… February 13, 2020 quaeler
Improving TLC error message for temporal existential quantifier in sp… February 13, 2020 quaeler

web site: update MacOS version February 7, 2020 damiendoligez
1.4.4 : fix release date in two more places February 4, 2020 damiendoligez
release 1.4.4: change the date to February 2020 February 4, 2020 damiendoligez
web site : a few minor corrections that were overlooked in the previo… February 4, 2020 damiendoligez
update the Web site for release 1.4.4 and fix broken links February 4, 2020 damiendoligez

RT @lemmster: A first user manual for apalache, the symbolic model checker of #tlaplus: https://t.co/KpQ5NkdHfa

4 days ago
RT @lemmster: If you learned #tlaplus with Lamport's video course, how long did it take you to watch & comprehend each individual videos?

6 days ago
RT @lemmster: Combine IOExec with the Trace and ToJsonObject operators and you can post the current #tlaplus error trace - encode… https://t.co/LJfDeuHzKg

7 days ago
RT @lemmster: A new version of the #tlaplus proof system (TLAPS) has been released: https://t.co/rbilFBLgjl

7 days ago
RT @lemmster: Stephan Merz's chapter on #tlaplus is freely available at: https://t.co/wLlUrfmty2

4 weeks ago