TLA+ for All: Running Model Checking in a Python Notebook

TLA+ for All: Running Model Checking in a Python Notebook#

We published a project embedding TLA+ model checking directly into a Python notebook environment, making formal verification accessible without any installation. Users can write specifications, run the TLC model checker, and visualize behaviors in-browser.

Read the full paper details