TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

What if every action could use all the variables? Would we need to define Init? January 21, 2019
Help with running TLC in distributed mode (ad hoc) January 20, 2019
Can TLAPS check any termination proofs? January 19, 2019
Fairness for interruptable process January 18, 2019
Simpler method of making multiple changes to a function in a single step January 16, 2019

RT @lemmster: The upcoming TLC profiler - on which I have been working on for much longer than intended - will help identify expe… https://t.co/yZeftYWe5i

2 weeks ago
TLA+ Conference September 12, 2019 in St. Louis, MO, USA: https://t.co/hK1y3Z5pY8 #tlaplus

3 weeks ago
RT @talex5: Experiences using @tlaplus to understand Xen's vchan protocol: https://t.co/ueNzjIX2gu @OpenMirage @QubesOS

3 weeks ago
RT @pressron: Verifying Software Traces Against a Formal Specification with TLA+ and TLC https://t.co/OS9KfgJu1o

1 month ago
RT @pressron: A TLA+ specification of Tic-Tac-Toe in the Behavioral Programming style, after https://t.co/F04UNz34wi by David Har… https://t.co/eGC1xoOj2Q

2 months ago