TLA+ tools come with a debugger that allow you to debug your specifications. See it in action:

You will need the SVG extension: https://marketplace.visualstudio.com/items?itemName=jock.svg.

The TLA+ Debugger has a new major capability: interactive state-space exploration. This feature changes how you can interact with your TLA+ specifications by letting you explore the state space of your models interactively, one state at a time.

This represents a shift in how you can work with TLA+ specifications, enabling new workflows for understanding and validating your models.

Interactive state-space exploration allows you to:

• Interactively select the initial state from the set of all initial states satisfying your Init predicate
• Choose successor states by selecting from the set of all valid next states computed by your Next action
• Step backward through the trace to any predecessor state, including all the way back to the set of initial states
• Navigate freely through your specification's state machine using step-in, step-over, and step-back operations

This approach emphasizes the state-machine perspective of TLA+, making it natural to think about your specification as a state transition system rather than just formulas and temporal properties.

When combined with TLA+ animations, interactive state-space exploration truly shines. The textual TLA+ specification is conceptually lifted into the application domain of the system being modeled. Instead of examining raw variable assignments, you can see animated visualizations of your protocol's behavior as you navigate through the state space.

Connecting animations to the debugger is trivial with Watch expressions—simply add a watch for your animation module's AnimView operator, and the debugger will display the SVG visualization for each state as you navigate through the state space.

The first screencast (linked below) demonstrates how to combine the TLA+ Debugger, interactive state-space exploration, Watch expressions, and animations into what becomes effectively a Graphical Debugger for your system or protocol. Notably, the animation module shown in the screencast was generated by AI, following the TLA+ animation guide shipped as part of the new TLA+ MCP server—demonstrating how accessible this workflow can be.

The new "Halt (break) after Init and Next" breakpoint that enables interactive state-space exploration supports breakpoint conditions, which opens up advanced debugging workflows:

• For specs that terminate or deadlock, the breakpoint condition ~ENABLED Next will halt simulation at the terminal state
• Breakpoint conditions are evaluated both after Init (for the set of initial states) and after Next (for successor states)
• The debugger halts even when Next evaluates to FALSE (i.e., when no successor states exist), allowing you to catch deadlocks

Breakpoint conditions, Watch expressions, and the Debug Console now support loading any TLA+ module on the TLA-Library path, even if those modules are not extended by the spec being debugged. This enables new capabilities, such as:

Exporting trace prefixes in various formats (JSON, TLA+, binary, etc.) dynamically during a debugging session. For example, you can evaluate this Watch expression:

LET J == INSTANCE _JsonTrace
    WITH _JsonTraceFile <- "output.json"
IN J!_JsonTrace

This exports the current trace to JSON without needing to preconfigure the debugger or manually trigger violations. Several other export formats are supported via modules:

• _TLCTracePlain - Exports the trace as a TLA+ module with a Trace constant (text format)
• _TLCTrace - Exports the trace in TLC's binary format (designed for very long traces)
• _TLCTESpec - Generates a trace expression specification that can replay the trace as a valid behavior
• _TLCActionTrace - Exports the sequence of actions with their parameters/arguments for minimization workflows
• _TLAPlusCounterExample - Exports the full TLCExt!CounterExample record as a TLA+ module
• _DotTrace - Exports the trace in DOT/GraphViz format for visualization This functionality is showcased in the third screencast.

This export capability is a first step towards the goal outlined in GitHub issue #860: create interesting traces interactively in the debugger, export them, and then have TLC verify repeatedly that these traces remain valid behaviors of the original specification as you update it. This bridges the gap between exploratory debugging and formal verification.

The TLA+ Debugger was first released in 2022 (see publication) and is built on the Debug Adapter Protocol (DAP), which provides a standardized interface between development tools and debuggers. The debugger is available for VSCode and Cursor, but will work in any IDE that supports DAP.

Interactive state-space exploration was pioneered by Will Schultz in Spectacle, and his work has been an inspiration for this implementation. Will also pioneered TLA+ animations several years ago, as demonstrated in his presentation at the TLA+ Community Event 2018. Spectacle remains unique as the only tool that runs entirely in the browser, providing an incredibly accessible way to explore and share TLA+ specifications with no installation required.

The TLA+ Debugger implementation builds on this concept while offering complementary capabilities:

• Step through individual formulas of your specification at the expression level
• Support for the largest fragment of TLA+ by virtue of being implemented on top of TLC
• Integration with the full debugging ecosystem (breakpoints, watch expressions, call stacks, etc.)

Both tools have their strengths, and I encourage you to explore both approaches!

Three screencasts demonstrate these new features in action:

1. [[https://www.youtube.com/watch?v=ZrzoIYjFeHE|Interactive State-Space Exploration & Graphical Debugging with Animations]]
1. [[https://www.youtube.com/watch?v=aTW87nTmAmQ|Breakpoint Conditions with Deadlock Detection]]
1. [[https://www.youtube.com/watch?v=cIXqCmEr_V4|Dynamic Trace Export and Advanced Watch Expressions]]

For those interested in implementation details, the last 39 commit messages up to and including this commit contain extensive context about these features, including:

• Support for conditional breakpoints on initial and next states
• Deterministic sorting of successor states by action location and state values
• Unified infrastructure for Watch and Debug expressions
• Step-in functionality using minimal Hamming distance to select "close" successor states
• Step-over functionality using maximal Hamming distance to select "far" successor states
• Preservation of finite stuttering in debugger traces for faithful behavior representation

I'd love to hear your thoughts on these new capabilities! Please feel free to provide feedback here on the mailing list or on GitHub.