TLA+ for All: Running Model Checking in a Python Notebook
If you've ever been curious about formal methods but got stuck on the setup, you're not alone. TLA+ is a powerful tool for specifying and verifying concurrent and distributed systems, but getting started can feel like an uphill climb. Installation hassles, tooling confusion, and steep learning curves can scare off even the most enthusiastic engineers.
But what if using TLA+ was as simple as opening a Python notebook?
That’s exactly what we—Konstantin Läufer and George K. Thiruvathukal from Loyola University Chicago—set out to explore in our recent work. Instead of wrangling installations and custom IDEs, we’re bringing TLA+ to Google Colab, where anyone can try it instantly in a web browser. There is no setup required, and no friction—just pure, interactive model checking.
Why This Matters
TLA+ has been around for decades, originally developed by Leslie Lamport—who also gave us LaTeX (still our favorite writing tool) and a Turing Award-winning researcher in distributed systems. His work has shaped how we think about correctness in complex, concurrent systems. Companies like Amazon, Microsoft, and Google use TLA+ to verify mission-critical software, proving its real-world impact.
So if TLA+ is so widely used, what is the problem? Adoption outside of hardcore verification circles is limited. Too many engineers and students abandon it before they even get to the good parts.
Our approach removes these barriers by:
- Letting you run TLA+ models in a Python notebook—no separate tools or plugins (kernels) are needed. It just works.
- Supporting interactive experimentation—modify models and check results instantly.
- Making formal methods more accessible to students, engineers, researchers, and other educators.
We’ve been teaching formal methods at Loyola some time now, and this notebook-based approach is transforming how students engage with TLA+. They’re experimenting more, testing their own models, and—dare we say it—actually enjoying model checking.
How It Works
Rather than asking students to install TLA+ tools manually, our notebook does the work for them. Here’s what happens behind the scenes:
- TLA+ tools are installed dynamically (inside the notebook).
- A model is downloaded from GitHub.
- Model checking runs using TLC (TLA+'s standard model checker).
- Results appear instantly, with helpful (pretty) formatting.
- Users can interactively evaluate expressions using a small Python helper.
That’s it. No custom Jupyter kernels. No wrestling with environment variables. Just open the notebook and start modeling.
Why Use a Notebook Instead of an IDE?
Some might argue that notebooks aren’t the best environment for software development. We vehemently agree! But for learning, experimenting, and teaching, they’re perfect. You get:
- Immediate execution without configuring an IDE.
- A clear, step-by-step workflow that makes TLA+ feel approachable.
- Collaboration features, since notebooks can be shared effortlessly.
- Lecture Mode, since notebooks are much like lecture outlines. You can present them in class, with the added advantage of showing how they work-or don't work-in real time.
And when students are ready to move on to more complex projects, they can easily transition to full-fledged TLA+ development environments like the TLA+ Toolbox or the VSCode extension.
Where We’re Headed Next
This is just the beginning. We’re planning to expand this approach with:
- Better visualization tools to help students understand execution traces.
- Integration with other formal methods tools, like Alloy.
- More polished notebooks for self-paced learning and workshops.
Our goal is to make TLA+ something anyone can try in five minutes. If we can lower the barriers, more people can benefit from formal methods without getting lost in convoluted setup details.
Try It Yourself
Want to see TLA+ in action without installing anything? Check out our open-source notebook and start experimenting today. We’d love to hear your feedback!