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.

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 Mafra, Rodrigo Otoni, Thomas Pani, Andrey Kupriyanov, and Philip Offtermatt.

Apalache is currently hosted at Informal Systems.