TLA+ for All: Model Checking in a Python Notebook

Document Type

Article

Publication Date

2-8-2025

Publication Title

Figshare

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.

Identifier

10.6084/m9.figshare.28376276.v1

Creative Commons License

Creative Commons Attribution 4.0 International License
This work is licensed under a Creative Commons Attribution 4.0 International License.

Link to Full Text

Share

COinS