Document Type
Article
Publication Date
2-8-2025
Publication Title
Figshare
Pages
1-3
Abstract
TLA+ is widely recognized for its effectiveness in specifying and verifying concurrent and distributed systems. However, for educators and practitioners, barriers to adoption include installation complexity and tooling setup. In the proposed presentation, we demonstrate a lightweight, easily shareable, and fully reproducible approach to running TLA+ in a Python notebook hosted on Google Colab without requiring new tools or custom Jupyter kernel development. By creating an environment where users can experiment with TLA+ models instantly, we lower these barriers and demonstrate the suitability for education and outreach.
Recommended Citation
Laufer, Konstantin and Thiruvathukal, George K.. TLA+ for All: Model Checking in a Python Notebook. Figshare, , : 1-3, 2025. Retrieved from Loyola eCommons, Computer Science: Faculty Publications and Other Works, http://dx.doi.org/10.6084/m9.figshare.28376276.v1
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Copyright Statement
© The Author(s), 2025.
Comments
Author Posting © The Author(s), 2025. This is a pre-print article.