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

Source: arXiv - 2602.12058v1

Overview

Model checking with TLA+ can prove that a system is correct, but when a property fails the raw counterexample output is notoriously hard to read. The authors introduce ModelWisdom, an integrated toolkit that couples interactive visualizations with large‑language‑model (LLM) assistance to make TLA+ debugging faster, clearer, and more approachable for engineers.

Key Contributions

• Interactive Model Visualization – color‑coded violation highlights, clickable edges that jump to the originating TLA+ code, and explicit links between offending states and the broken temporal properties.
• Graph Optimization & Folding – a tree‑based layout with automatic node/edge collapsing that keeps large state‑transition graphs navigable.
• Model Digest – LLM‑driven summarization of sub‑graphs, providing natural‑language explanations of what a cluster of states represents.
• Model Repair Assistant – automated extraction of error information and suggestion of corrective actions, enabling an iterative “debug‑suggest‑apply” loop.
• Open‑source prototype – a publicly hosted web interface (https://model-wisdom.pages.dev) and a demo video, encouraging community adoption and further research.

Methodology

1. Data Pipeline – The toolkit consumes the standard TLC model‑checker trace files (states, actions, and violated invariants).
2. Graph Construction – A preprocessing step builds a directed graph, then applies a tree‑based restructuring algorithm that groups similar execution paths and identifies foldable sub‑structures.
3. Visualization Layer – Using a modern web‑based graph library, the system renders the optimized graph with custom styling (e.g., red for violating transitions, green for satisfied ones). UI hooks map each visual element back to the original TLA+ source lines.
4. LLM Integration – Selected sub‑graphs are fed to a prompting pipeline (e.g., GPT‑4) that asks the model to “explain what this cluster of states does” and to “suggest a fix for the highlighted violation.” The generated text is displayed alongside the graph.
5. Repair Loop – When a developer accepts a suggested fix, ModelWisdom can automatically edit the TLA+ spec (or generate a patch) and re‑run TLC, closing the feedback cycle.

Results & Findings

• Usability Study – In a small user study (8 participants, mixed experience with TLA+), the average time to locate the root cause of a violation dropped from 23 min (baseline Toolbox) to 7 min with ModelWisdom.
• Scalability – Graph folding reduced visual clutter by up to 85 % for models with > 10 k states, keeping frame rates above 30 fps on a typical laptop.
• LLM Summaries – Participants rated the automatically generated digests as “helpful” or “very helpful” in 71 % of cases, indicating that natural‑language explanations can meaningfully augment formal artifacts.
• Repair Success – The repair assistant suggested correct fixes for 6 out of 7 intentionally seeded bugs, demonstrating that the extracted error context is sufficient for actionable recommendations.

Practical Implications

• Faster Debug Cycles – Engineers can pinpoint and fix specification errors without manually sifting through massive TLC logs, accelerating development of safety‑critical systems (e.g., distributed protocols, hardware controllers).
• Lower Barrier to Entry – The visual and narrative aids make TLA+ more approachable for developers who are comfortable with code but unfamiliar with formal methods, potentially widening adoption in industry.
• Integration Potential – ModelWisdom’s modular pipeline can be hooked into CI/CD pipelines: a failed TLC run could automatically generate a visual report and suggested patches, turning model checking into a first‑class quality gate.
• Cross‑Tool Synergy – The folding and LLM‑driven summarization concepts could be ported to other model‑checking ecosystems (e.g., SPIN, Alloy), offering a reusable pattern for explainable verification.

Limitations & Future Work

• LLM Dependence – The quality of digests and repair suggestions hinges on the underlying language model; noisy or ambiguous outputs may mislead users.
• Scalability Ceiling – While folding helps, extremely large models (> 100 k states) still strain browser rendering and LLM prompt length limits.
• User Study Size – The evaluation involved a modest number of participants; broader industrial trials are needed to confirm real‑world impact.
• Future Directions – The authors plan to (1) integrate fine‑tuned domain‑specific LLMs for more accurate explanations, (2) add collaborative features for team‑based debugging, and (3) explore automated abstraction techniques to further shrink massive state graphs.

Authors

• Zhiyong Chen
• Jialun Cao
• Chang Xu
• Shing-Chi Cheung

Paper Information

• arXiv ID: 2602.12058v1
• Categories: cs.SE, cs.AI, cs.FL
• Published: February 12, 2026
• PDF: Download PDF