Here is the list of the TLA+ language features that are currently supported by Apalache, following the Summary of TLA+.

Safety vs. Liveness

At the moment, Apalache is only able to check invariants and inductive invariants. Which means that you can only check safety properties with Apalache, unless you employ a liveness-to-safety transformation in your spec. In general, we do not support checking liveness properties. If you would like to see liveness implemented, upvote the liveness feature.


Module-Level constructs

EXTENDS moduleβœ”-A few standard modules are not supported yet (Bags and Reals)
CONSTANTS C1, C2βœ”-Either define a ConstInit operator to initialize the constants, use a .cfg file, or declare operators instead of constants, e.g., C1 == 111
VARIABLES x, y, zβœ”-
ASSUME Pβœ” / βœ–-Parsed, but not propagated to the solver
F(x1, ..., x_n) == expβœ” / βœ–-Every application of F is replaced with its body. Recursive operators need unrolling annotations.
f[x ∈ S] == expβœ” / βœ–-Recursive functions are only supported if they return integers or Booleans.
INSTANCE M WITH ...βœ” / βœ–-No special treatment for ~>, \cdot, ENABLED
N(x1, ..., x_n) == INSTANCE M WITH...βœ” / βœ–-Parameterized instances are not supported
THEOREM Pβœ” / βœ–-Parsed but not used
LOCAL defβœ”-Replaced with local LET-IN definitions

The constant operators


/\, \/, ~, =>, <=>βœ”-
\A x \in S: p, \E x \in S : pβœ”-
CHOOSE x \in S : pβœ”/βœ–-Similar to TLC, we implement a non-deterministic choice. We will add a deterministic version in the future.
CHOOSE x : x \notin Sβœ–?That is a commonly used idiom
\A x : p, \E x : pβœ–NEVERUse the versions above
CHOOSE x : pβœ–NEVERUse the version above


Note: only finite sets are supported. Additionally, existential quantification over Int and Nat is supported, as soon as it can be replaced with a constant.

=, /=, \in, \notin, \intersect, \union, \subseteq, \βœ”-
{e_1, ..., e_n}βœ”-Empty sets {} require type annotations
{x \in S : p}βœ”-
{e : x \in S}βœ”-
SUBSET Sβœ”-Sometimes, the powersets are expanded
UNION Sβœ”-Provided that S is expanded


DOMAIN fβœ”-
[ x \in S ↦ e]βœ”-
[ S -> T ]βœ”-Supported, provided the function can be interpreted symbolically
[ f EXCEPT ![e1] = e2 ]βœ”-


Use type annotations to help the model checker in finding the right types. Note that our type system distinguishes records from general functions.

r[e]βœ”/βœ–-Provided that e is a constant expression.
[ h1 ↦ e1, ..., h_n ↦ e_n]βœ”-
[ h1 : S1, ..., h_n : S_n]βœ”-
[ r EXCEPT !.h = e]βœ”-


Use type annotations to help the model checker in finding the right types. Note that our type system distinguishes tuples from general functions.

e[i]βœ” / βœ–-Provided that i is a constant expression
<< e1, ..., e_n >>βœ”-Use a type annotation to distinguish between a tuple and a sequence.
S1 \X ... \X S_nβœ”-
[ t EXCEPT ![i] = e]βœ”/βœ–-Provided that i is a constant expression

Strings and numbers

"c1...c_n"βœ”-A string is always mapped to a unique uninterpreted constant
STRINGβœ–-It is an infinite set. We cannot handle infinite sets.
d1...d_nβœ”-As long as the SMT solver (Z3) accepts that large number
d1...d_n.d_n+1...d_mβœ–-Technical issue. We will implement it upon a user request.

Miscellaneous Constructs

IF p THEN e1 ELSE e2βœ”-Provided that both e1 and e2 have the same type
<<<<<<< Updated upstream
CASE p1 -> e1 [] ... [] p_n -> e_n [] OTHER -> eβœ”-See the comment above
CASE p1 -> e1 [] ... [] p_n -> e_nβœ”-
CASE p1 -> e1 [] ... [] p_n -> e_n [] OTHER -> eβœ”-Provided that e1, ..., e_n have the same type
CASE p1 -> e1 [] ... [] p_n -> e_nβœ”-Provided that e1, ..., e_n have the same type
>>>>>>> Stashed changes
LET d1 == e1 ... d_n == e_n IN eβœ”All applications of d1, ..., d_n are replaced with the expressions e1, ... e_n respectively. LET-definitions without arguments are kept in place.
multi-line /\ and \/βœ”-

The Action Operators

[A]_eβœ–-It does not matter for safety
< A >_eβœ–-
UNCHANGED <<e_1, ..., e_k>>βœ”-Always replaced with e_1' = e_1 /\ ... /\ e_k' = e_k
A βˆ™ Bβœ–-

The Temporal Operators

The model checker assumes that the specification has the form Init /\ [][Next]_e. Given an invariant candidate Inv, the tool checks, whether Inv is violated by an execution whose length is bounded by the given argument.

Except the standard form Init /\ [][Next]_e, no temporal operators are supported.

Standard modules

Integers and Naturals

For the moment, the model checker does not differentiate between integers and naturals. They are all translated as integers in SMT.

+, -, *, <=, >=, <, >βœ”-These operators are translated into integer arithmetic of the SMT solver. Linear integer arithmetic is preferred.
\div, %βœ”-Integer division and modulo
a^bβœ” / βœ–-Provided a and b are constant expressions
a..bβœ” / βœ–-Sometimes, a..b needs a constant upper bound on the range. When Apalache complains, use {x \in A..B : a <= x /\ x <= b}, provided that A and B are constant expressions.
Int, Natβœ” / βœ–-Supported in \E x \in Nat: p and \E x \in Int: p, if the expression is not located under \A and ~. We also support assignments like f' \in [S -> Int] and tests f \in [S -> Nat]
/βœ–-Real division, not supported


<<...>>, Head, Tail, Len, SubSeq, Append, \o, f[e]βœ”-The sequence constructor <<...>> needs a type annotation.
EXCEPTβœ–If you need it, let us know, issue #324
Seq(S)βœ–-If you need it, let us know, issue #314
SelectSeqβœ–-will not be supported in the near future


IsFiniteβœ”-Always returns true, as all the supported sets are finite
Cardinalityβœ”-Try to avoid it, as Cardinality(S) produces O(n^2) constraints in SMT for cardinality n


f @@ a :> bβœ”-Extends the function relation with the pair <<a, b>>


Not supported, not a priority