Examples of efficiently using Apalache for model checking TLA+ and Quint specifications. If you are looking for general TLA+ examples, check TLA+ Examples.
| Specification | Author | Customer | Syntax | Description |
|---|---|---|---|---|
| Ben-Or 83 | Igor Konnov | Fun project | TLA+ | Checking safety of Ben-Or's probabilistic consensus that tolerates Byzantine failures. |
| distributed-termination-detection | Giuliano Losa | TLA+ | Formalization of a distributed termination-detection algorithm, including a proof checked with Apalache | |
| labyrinth | Igor Konnov | Fun project | TLA+ | Simple exploration in a 2D-labyrinth |
| matter-labs-chonkybft | Igor Konnov, Denis Kolegov | Matter Labs | Quint | BFT consensus by Matter Labs |
| tendermint-accountability | Zarko Milosevic, Igor Konnov | Informal Systems | TLA+ | BFT consensus in Tendermint/CometBFT blockchains |
| tendermint-light-client | Josef Widder, Igor Konnov | Informal Systems | TLA+ | Light client for Tendermint/CometBFT blockchains |
| TetraBFT | Giuliano Losa | TLA+ | Checking safety and liveness of TetraBFT consensus | |
| tla-apalache-workshop | Igor Konnov et. al. | Informal Systems | TLA+ | Apalache examples produced when teaching TLA+ at Informal Systems |
| zksync-governance | Denis Kolegov, Igor Konnov | Matter Labs | Quint | Specification of the ZKsync Governance smart contracts |
Note: Whenever a specification cannot be directly included in this repository, we give proper links to the specifications in the employer's or customer's GitHub repository.