Skip to content


@ECF @tlaplus


  1. TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

    Java 1.2k 91

  2. TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

    TLA 36 9

  3. Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

    TLA 309 10

  4. Java Introduction (each commit introduces a new concept)

    Java 2 2

  5. Proving a blocking queue deadlock free in a dozen different ways

    TLA 30 2

  6. Forked from kaelzhang81/awesome-tlaplus

    A curated list of TLA+ resources.


871 contributions in the last year

Jul Aug Sep Oct Nov Dec Jan Feb Mar Apr May Jun Mon Wed Fri

Contribution activity

July 2020

Created an issue in dgpv/bip32_template_parse_tplaplus_spec that received 1 comment

Evaluate TLA+ expressions on the command-line

The readme claims that one cannot evaluate TLA+ expressions on the command-line. The recent 1.7.0 release added support for trace expression evalua…

1 comment

Seeing something unexpected? Take a look at the GitHub profile guide.

You can’t perform that action at this time.