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 his Video course.
Check the releases page.
We recommend that you run the latest stable docker image apalache/mc:latest,
or checkout the source code from master, which accumulates bugfixes over the
latest release. For more information, see [the manual][manual-docker].
To try the latest cool features, check out the unstable branch.
- Read the Apalache user manual.
- Consult the (WIP) Idioms for writing better TLA+.
- Consult the (WIP) TLA+ language manual for engineers.
- Join the chat in the Apalache zulip stream.
- Contribute to the development of Apalache.
-
Check Tendermint specs to see how we use TLA+ and Apalache at Informal to design and specify protocols for the Tendermint blockchain.
-
To see more examples, check the standard repository of TLA+ examples.
-
How TLA+ and Apalache Helped Us to Design the Tendermint Light Client. Interchain Conversations 2020 (December 2020).
-
Model-based testing with TLA+ and Apalache. TLA+ Community Event 2020 (October 2020).
-
Type inference for TLA+ in Apalache. TLA+ Community Event 2020 (October 2020).
-
Formal Spec and Model Checking of the Tendermint Blockchain Synchronization Protocol 2nd Workshop on Formal Methods for Blockchains (July 2020).
-
Showing safety of Tendermint Consensus with TLA+ and Apalache. Dev session at Informal Systems (May 2020).
-
TLA+ model checking made symbolic OOPSLA 2019 (October 2019).
-
Bounded model checking of TLA+ specifications with SMT TLA+ Community Event 2018 (July 2018).
We are collecting apalache benchmarks. See the Apalache performance when checking inductive invariants and running bounded model checking. Versions 0.6.0 and 0.7.2 are a major improvement over version 0.5.2 (the version reported at OOPSLA19).
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.