using:apalache:start

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

====== Apalache Symbolic Model Checker ======

[[https://apalache-mc.org/|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 [[https://github.com/Z3Prover/z3|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 [[https://apalache-mc.org/docs/|Apalache Manual]].

===== Examples of efficiently using Apalache =====

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 [[https://github.com/konnov/apalache-examples|examples]] of efficiently using Apalache.