Apalache

Perhaps, the most concise summary of Apalache can be found on Leslie Lamport’s page on TLA⁺:

Apalache is an alternative to TLC for checking TLA+ specifications. While TLC is an explicit-state model checker, Apalache is a symbolic model checker. It checks safety for bounded executions and inductive invariants for unbounded executions, assuming that all data structures are finite. The tool leverages the SMT solver Z3, from Microsoft Research.

The canonical version of Apalache is currently hosted under the Github organization github.com/apalache-mc. To see successful applications of Apalache, check Apalache examples.

Currently, Apalache is not funded by any organization. See FUNDING.md for the past funding. The project is de-facto funded by its current maintainers and contributors, including Jure Kukovec, Thomas Pani, and myself. If you would like to sponsor the project, please contact us, or simply sponsor us on GitHub by clicking the “Sponsor” button on the Github page!

I started the research project on Apalache at TU Wien in 2016, after receiving the grant of 539k EUR from Vienna Science and Technology Fund. In 2018, I continued research on Apalache at VeriDis, Inria Nancy. From 2019 to 2023, I was leading industrial adoption of Apalache at Interchain Foundation and Informal Systems. Many researchers and engineers have contributed to Apalache, including: Thanh Hai Tran, Shon Feder, Jure Kukovec, Gabriela Moreira, Rodrigo Otoni, Thomas Pani, Andrey Kupriyanov, and Philip Offtermatt.