Installation • Manual • Releases • Chat • Contribute

Apalache translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3. Currently, Apalache supports three approaches of analyzing TLA⁺ specifications:

1. Randomized symbolic execution to reason about some executions up to length k,

2. Bounded model checking to reason about all executions up to length k, and

3. Inductiveness checking to reason about all executions of all lengths.

To understand, how these three approaches play together, see the [blogpost] on Model checking safety of Ben-Or’s Byzantine consensus with Apalache (2024).

In general, Apalache runs under the same assumptions as the explicit-state model checker 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.

In addition to TLA⁺, Apalache power ups the following projects:

• The Quint language provides an engineer-friendly syntax for writing specifications. Quint uses Apalache as a backend model checker.

• Solarkraft is a tool for runtime monitoring of Soroban smart contracts on Stellar. Solarkraft uses Apalache as a backend model checker.

• Atomkraft is a tool for model-based testing of Cosmos dApps. Atomkraft uses Apalache as a backend model checker.

Success stories

• Specification and Model-checking of the ZKsync Governance Protocol [blogpost] (2024)

• Specification and model checking of BFT consensus by Matter Labs [blogpost] (2024)

• Model checking of the Tendermint light client [results page] (2020)

• Model checking of agreement and accountable safety in Tendermint consensus [results page] (2019-2020)

Tutorials

• Extended version of the Apalache tutorial

• Type checking TLA+ with Snowcat

Theory

To read an academic papers about the theory behind Apalache, check our paper at OOPSLA19 and paper at TACAS23.

Talks

• How TLA+ and Apalache Helped Us to Design the Tendermint Light Client. Interchain Conversations 2020 (December 2020).

• Informal Systems Tutorial: TLA+ Basics

• Model-based testing with TLA+ and 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).

• Type inference for TLA+ in Apalache. TLA+ Community Event 2020 (October 2020).

• TLA+ model checking made symbolic OOPSLA 2019 (October 2019).

• Bounded model checking of TLA+ specifications with SMT TLA+ Community Event 2018 (July 2018).