tlaplus-research-projects APALACHE Abstraction-based parameterized TLA+ checker: Bringing state-of-the-art model checking to TLA+