ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair

TL;DR

The paper addresses the interpretability gap in TLA+ model checking, where large counterexamples and state-transition graphs are hard to understand. It proposes ModelWisdom, an LLM-assisted, interactive environment that unifies Model Visualizer, Model Digest, and Model Repair to turn verification artifacts into actionable insights. Key contributions include: (1) colorized violation highlighting and source-code navigation for precise traceability, (2) scalable graph optimization with tree-based layouts and folding, (3) Model Digest for automated, context-rich explanations of partial graphs, and (4) iterative Model Repair with an interactive history to support systematic debugging. The approach aims to reduce debugging effort and broaden practical adoption of formal verification by making visualization, summarization, and repair more accessible and explainable.

Abstract

Model checking in TLA+ provides strong correctness guarantees, yet practitioners continue to face significant challenges in interpreting counterexamples, understanding large state-transition graphs, and repairing faulty models. These difficulties stem from the limited explainability of raw model-checker output and the substantial manual effort required to trace violations back to source specifications. Although the TLA+ Toolbox includes a state diagram viewer, it offers only a static, fully expanded graph without folding, color highlighting, or semantic explanations, which limits its scalability and interpretability. We present ModelWisdom, an interactive environment that uses visualization and large language models to make TLA+ model checking more interpretable and actionable. ModelWisdom offers: (i) Model Visualization, with colorized violation highlighting, click-through links from transitions to TLA+ code, and mapping between violating states and broken properties; (ii) Graph Optimization, including tree-based structuring and node/edge folding to manage large models; (iii) Model Digest, which summarizes and explains subgraphs via large language models (LLMs) and performs preprocessing and partial explanations; and (iv) Model Repair, which extracts error information and supports iterative debugging. Together, these capabilities turn raw model-checker output into an interactive, explainable workflow, improving understanding and reducing debugging effort for nontrivial TLA+ specifications. The website to ModelWisdom is available: https://model-wisdom.pages.dev. A demonstrative video can be found at https://www.youtube.com/watch?v=plyZo30VShA.

Figures (3)

• Figure 1: Interface of ModelWisdom with Highlight Features
• Figure 2: Interface of ModelWisdom with node folding
• Figure 3: Interface of ModelWisdom with highlighting violated properties, ModelRepair, and ModelDigest