The Symbolic Model Checker for TLA+

View the Project on GitHub informalsystems/apalache

"Apalache Logo"


Apalache translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3. Apalache can check inductive invariants (for fixed or bounded parameters) and check safety of bounded executions (bounded model checking). To see the list of supported TLA+ constructs, check the supported features. In general, Apalache runs under the same assumptions as TLC.

To learn more about TLA+, visit Leslie Lamport’s page on TLA+ and see his video course. Also, check out TLA+ language manual for engineers.



Academic papers

To read an academic paper about the theory behind Apalache, check our paper at OOPSLA19. Related reports and publications can be found at the Apalache page at TU Wien.