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

This page is outdated. Since 2020, we have been developing Apalache at Informal Systems.

Critical distributed systems are designed to tolerate faults of individual components: they must work even if some of their components fail. In APALACHE, we address three technical and methodological challenges:

  • Symbolic model checking techniques for TLA+.
  • Domain-specific abstractions for fault-tolerant TLA+ designs.
  • Parameterized model checking techniques for an unbounded number of components.

Some of the challenges were mentioned in the position paper (2015).


Bounded model checking modulo theories (BMCMT). As a first step towards more advanced techniques for TLA+, we are currently developing a symbolic model checker that is working under the following assumptions:

  1. As in TLC, all specification parameters are fixed and finite, e.g., the system is initialized integers, finite sets, and functions of finite domains and co-domains.
  2. As in TLC, all data structures evaluated during an execution are finite, e.g., a system specification cannot operate on the set of all integers.
  3. Only finite executions up to a given bound are analysed.

The current version of the tool will most likely crash on your own TLA+ code. When the tool is ready for early testing by the users, we will issue an announcement.

Given a TLA+ specification, with all parameters fixed, our model checker performs the following steps:

  1. BMCMT automatically extracts symbolic transitions from the specification (see our paper at ABZ’18). This allows us to partition the action Next into a conjunction of simpler actions A1, …, An.
  2. BMCMT translates the operators Init and A1, …, An to SMT formulas. This allows us to explore bounded executions with an SMT solver, for instance, with Microsoft Z3 or CVC4. For instance, a sequence of k steps, all of which execute action A1, will be encoded as Run(k) == [[Init(s0)]] ∧ [[A1(s0, s1)]] ∧ … ∧ [[A1(sk-1, sk)]]. To find an execution of length k leading to an unsafe state sk, one can add [[Bug(sk)]] to the formula Run(k). Here, [[_]] is the translation function from TLA+ to SMT. Importantly, the values for the states s0, …, sk are not enumerated as in TLC, but have to be found by the SMT solver.

This technique follows the approach of bounded model checking (BMC) that was pioneered by [Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu’99]. Bounded model checking was quite a success for bug finding and verification of C code, e.g., see the tool CBMC by Daniel Kroening et al. Whereas classical BMC uses of-the-shelf SAT solvers (Boolean logic), our tool encodes bounded model checking queries in SMT, which supports first-order theories of integers, uninterpreted functions, arrays, etc. The main challenge of our work lies in defining the translation function [[_]] to SMT. We are preparing a technical report on this topic.

We will give more details in the upcoming talk at the TLA+ community event.


ThanhHaiTran_Photo © Sara Meister jure

Related projects

Parameterized model checking of fault-tolerant distributed algorithms. To see the papers, benchmarks, and tools, check our Byzantine Model Checker .

Recent papers

[17] Extracting symbolic transitions from TLA+ specifications
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
Science of Computer Programming, volume 187, pages 102361, 2020.
[bibtex] [pdf] [doi]
[16] Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
30th International Conference on Concurrency Theory (CONCUR 2019) (Wan Fokkink, Rob van Glabbeek, eds.), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1–33:15, 2019, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf] [doi]
[15] Verifying Safety of Synchronous Fault-Tolerant Algorithms Bounded Model Checking
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, pages 357–374, 2019.
Note: A pre-print including the proofs is available at: https://hal.inria.fr/hal-01925653
[bibtex] [pdf] [doi]
[14] TLA+ model checking made symbolic
Igor Konnov, Jure Kukovec, Thanh-Hai Tran
PACMPL, volume 3, number OOPSLA, pages 123:1–123:30, 2019.
[bibtex] [pdf]
[13] Extracting Symbolic Transitions from TLA+ Specifications
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
Abstract State Machines, Alloy, B, TLA, VDM, and Z, pages 89–104, 2018.
[bibtex] [pdf] [doi]
[12] Reachability in Parameterized Systems: All Flavors of Threshold Automata
Jure Kukovec, Igor Konnov, Josef Widder
29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 19:1–19:17, 2018.
[bibtex] [pdf] [doi]
[11] BmcMT: Bounded Model Checking of TLA+ Specifications with SMT
Igor Konnov, Jure Kukovec, Thanh-Hai Tran
2018, Presentation at the TLA+ Community Meeting, Oxford, UK, July.
[bibtex] [pdf]
[10] Synthesis of Distributed Algorithms with Parameterized Threshold Guards
Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem
OPODIS, volume 95 of LIPIcs, pages 32:1–32:20, 2017.
[bibtex] [pdf]
[9] Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347–366, 2017.
[bibtex] [pdf] [doi]
[8] On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability
Igor V. Konnov, Helmut Veith, Josef Widder
Inf. Comput., volume 252, pages 95–109, 2017.
[bibtex] [pdf] [doi]
[7] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719–734, 2017.
Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327
[bibtex] [pdf]
[6]Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, 2017, Springer.
Note: to appear
[5] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
ACM SIGACT News, volume 47, number 2, pages 53–64, jun 2016.
[bibtex] [pdf]
[4] Parameterized Systems in BIP: Design and Model Checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis
27th International Conference on Concurrency Theory (CONCUR 2016) (Josée Desharnais, Radha Jagadeesan, eds.), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:16, 2016, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[3] What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6–21, 2016, Springer International Publishing.
[bibtex] [pdf]
[2] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]
[1] Challenges in Model Checking of Fault-tolerant Designs in TLA+
Igor Konnov, Helmut Veith, Josef Widder
2015, Presentation at the 8th International Workshop on Exploiting Concurrency Efficiently and Correctly, San Francisco, CA, USA, July.
[bibtex] [pdf]


Igor Konnov
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien

Room: HD 03 13 (how to get there)
Phone: +43 (1) 58801 – 184 807
Email: konnov@forsyte.at
Web: http://forsyte.at/~konnov/

Latest News

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Full news archive