We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.
@article{arxiv.2605.06118,
title = {TACO: A Toolsuite for the Verification of Threshold Automata},
author = {Paul Eichler and Tom Baumeister and Mouhammad Sakr and Mahboubeh Kalateh Dowlati and Marcus Völp and Swen Jacobs},
journal= {arXiv preprint arXiv:2605.06118},
year = {2026}
}