Features • Installation • Manual • Releases • Chat • Contribute

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.

Tutorials

• Type checking TLA+ with Snowcat

• Extended version of the Apalache tutorial

Talks

• Informal Systems Tutorial: TLA+ Basics

• Extended version of the Apalache tutorial. TLA+ tutorial at DISC 2021 (October 2021).

• 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).

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.