Apalache is a symbolic model checker for TLA+ and Quint. I started the project at TU Wien in 2016 and continue to maintain it with other contributors.
It is both a research tool and part of my practical work on distributed protocols: turning specifications into models we can explore, checking invariants, and investigating unexpected behavior.
The project today
The Apalache repository is the place to find the source code, releases, and ongoing development. The project website contains documentation and tutorials.
I also work on Hardened Testing of TLA+ Model Checkers, supported by the TLA+ Foundation. This project tests TLC and Apalache through fuzzing, differential testing, and regression tests.
Background
My work on Apalache has continued through TU Wien, Inria, the Interchain Foundation, Informal Systems, and my independent practice. Apalache has moved records the project's history and move to its own GitHub organization in 2024.
For applications to real protocols, see my portfolio and technical write-ups.