Awesome Open Source
Awesome Open Source

APALACHE project

A symbolic model checker for TLA+

master: Build Status     unstable: Build Status

Apalache translates TLA+ in the logic supported by the SMT solvers, for instance, 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.


Check the releases page.

We recommend you to run the latest docker image apalache/mc:latest and checkout the source code from master, which accumulate bugfixes over the latest release, see the manual. To try the latest cool features, check the unstable branch.

Getting started

Read the user manual.


We are collecting apalache benchmarks. See the Apalache performance when checking inductive invariants and running bounded model checking. Version 0.6.0 is a major improvement over version 0.5.2 (the version reported at OOPSLA19).

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.

Get A Weekly Email With Trending Projects For These Topics
No Spam. Unsubscribe easily at any time.
scala (2,436
smt (23
tla (18
model-checking (17

Find Open Source By Browsing 7,000 Topics Across 59 Categories