Apalache is a symbolic model-checker for the specification languages TLA+ and Quint. Apalache checks safety of bounded executions (bounded model-checking), inductive invariants (for fixed or bounded parameters), and temporal properties.
The project was started by Igor Konnov as a research project at TU Wien in 2016, and continued at VeriDis (Inria Nancy), Interchain Foundation, and Informal Systems. I joined the project in 2022 at Informal Systems, contributing to various parts of the system, including
- Apalache Cloud, a proprietary parallel version of the model-checker,
- Nitpicker, a property-based consistency checker for Apalache’s SMT encodings,
- the Quint-to-Apalache IR transpilation,
- and many internal fixes and updates.
Many researchers and engineers have contributed to Apalache, including: Igor Konnov, Jure Kukovec, Thanh Hai Tran, Shon Feder, Gabriela Moreira, Rodrigo Otoni, Andrey Kupriyanov, and Philip Offtermatt. Apalache is currently hosted at Informal Systems.