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 updating state and return in a definition May 15, 2019
running TLC on module imported with a parameterized INSTANCE May 13, 2019
A trick for changing multiple function values May 8, 2019
Embedding TLA+ in Latex May 5, 2019
[Noob] veiled passage in "Consensus on Transaction Commit" May 5, 2019

TLA+ Project News

TLAPS Project News

Latest Tweets

"Request for requirements" https://t.co/C8LG8YnzwG

1 week ago
RT @lemmster: [](be suspicious of success) A review of @hillelogram post "Modeling Adversaries with TLA+" with a detailed expl… https://t.co/2L2jkspTzi

1 week ago
RT @lemmster: Looking for input to "Continuous integration support for TLC model checking" (https://t.co/BrQujuW2Vw) #tlaplus #pluscal

1 week ago
Modeling Adversaries with #tlaplus https://t.co/GnVE3v3840

2 weeks ago
RT @lemmster: #tlaplus users please raise your hand if you would watch a spin-off to Lamport's https://t.co/vs2n6IAVE8 starring… https://t.co/0RvpxtvFCX

3 weeks ago

Proudly powered by WordPress