Apalache Symbolic Model Checker

Apalache is an alternative to TLC for checking TLA+ specifications. While TLC is an explicit-state model checker, Apalache is a symbolic model checker. It checks safety for bounded executions and inductive invariants for unbounded executions, assuming that all data structures are finite. It also has an experimental implementation for liveness checking via liveness-to-safety reduction. The tool leverages the SMT solver Z3, from Microsoft Research.

To run it, you need Java runtime environment version 17 (LTS) or 21 (LTS).

You can find the latest documentation on Apalache and the tutorials in the Apalache Manual.

Since Apalache is implementing an approach to model checking that is completely different from TLC, many examples that work very well may have suboptimal performance in Apalache, and the other way around. To this end, we are collecting examples of efficiently using Apalache.