Experiments with TLA+.
Some readings:
- The Future of TLA+
- TLA⁺ is more than a DSL for breadth-first search
- Why I use TLA+ and not(TLA+)
- Learn TLA+ with a focus on PlusCal
- TLA+ Examples
Related tech stack:
- Quint: A modern and executable specification language based on TLA+, developed by
- PlusCal: a gateway language to TLA+
- Apalache: A symbolic model checker for TLA+ specifications, via translation to SMT solvers such as Microsoft Z3
- TLAUC: The TLA⁺ Unicode Converter
- haybale: Symbolic execution of LLVM IR, written in Rust