Skip to content


Switch branches/tags


Failed to load latest commit information.
Latest commit message
Commit time

Community Repository

This is an open repository dedicated to contributions from the TLA+ community. Here you can submit the snippets, operators, and modules that you wrote for your specifications and that you want to share with the rest of the TLA+ community.

(For us to gauge demand, please star (eyes up and right) this repository if you use the CommunityModules.)

The Modules

Name Short description Module Override? Contributors
Functions.tla Notions about functions including injection, surjection, and bijection. @muenchnerkindl, @quicquid,@lemmy
Folds.tla Basic Fold operator. @quicquid, @muenchnerkindl
Graphs.tla Common operators on directed and undirected graphs. Leslie Lamport, @lemmy, @muenchnerkindl
SequencesExt.tla Various operators to manipulate sequences. @muenchnerkindl,@lemmy, @hwayne, @quicquid
Relation.tla Basic operations on relations, represented as binary Boolean functions over some set S. @muenchnerkindl
FiniteSetsExt.tla An Operator to do folds without having to use RECURSIVE. @hwayne,@lemmy, @quicquid
Bitwise.tla Bitwise And and shift-right. @lemmy,@pfeodrippe
DifferentialEquations.tla see page 178ff of Specifying Systems Leslie Lamport
Json.tla Print TLA+ values as JSON values. @kuujo
SVG.tla see @will62794, @lemmy
ShiViz.tla Visualize error-traces of multi-process PlusCal algorithms with an Interactive Communication Graphs. @lemmy
TLCExt.tla Assertion operators and experimental TLC features (now part of TLC). @lemmy, @will62794
IOUtils.tla Input/Output of TLA+ values & Spawn system commands from a spec. @lemmy, @lvanengelen
Combinatorics.tla (n choose k), factorial, .... @lemmy
BagsExt.tla BagAdd, BagRemove, FoldBag, ... @muenchnerkindl

How to use it

You must be running Java 9 or higher.

Just copy & paste the snippet, the operators, or the set of modules you are interested in.

Alternatively, you can download a library archive and add it to TLC's or the Toolbox's TLA+ library path. The advantage of the library archive is that TLC will evaluate an operator faster if the operator comes with a (Java) implementation (see e.g. SequencesExt.Java). Run TLC with -DTLA-Library=/path/to/lib/archive or add the library archive to the Toolbox (File > Preferences > TLA+ Preferences > TLA+ library path locations). The latest release is at the stable URL Screencast how to install the CommunityModules into the TLA+ Toolbox

Being a community-driven repository puts the community in charge of checking the validity and correctness of submissions. The maintainers of this repository will try to keep this place in order. Still, we can't guarantee the quality of the modules and, therefore, cannot provide any assistance on eventual malfunctions.


If you have one or more snippets, operators, or modules you'd like to share, please open an issue or create a pull request. Before submitting your operator or module, please consider adding documentation. The more documentation there is, the more likely it is that someone will find it useful.

If you change an existing module and tests start failing, check all tests that assert (usually AssertError operator) specific error messages, i.e., line numbers and module names. Note that even an unrelated change further up in the file might have changed the line number and could lead to a failing test case.



ant test