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

arXiv: https://arxiv.org/abs/2602.12058 · HTML: https://mlsanity.com/paper/2602.12058/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 26 references that are in the map.
- First posted on arXiv 12 Feb 2026.

## Builds on (most cited first, 7 of 7)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Recursive Introspection: Teaching Language Model Agents How to Self-Improve](https://mlsanity.com/paper/2407.18219/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications](https://mlsanity.com/paper/2404.11050/) (2024)
- [The TLA+ Toolbox](https://mlsanity.com/paper/1912.10633/) (2019)

## Built on by (most cited first, 1 of 1)

- [TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples](https://mlsanity.com/paper/2605.07935/) (2026)

## Abstract (arXiv)

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.