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.

翻译：TLA+中的模型检验虽能提供强有力的正确性保证，但实践者仍面临解释反例、理解大规模状态转移图以及修复错误模型等重大挑战。这些困难源于原始模型检验器输出的可解释性有限，以及将违规行为追溯至源规约所需的大量人工工作。尽管TLA+工具箱包含状态图查看器，但其仅提供静态、完全展开且无折叠、颜色高亮或语义解释的图，这限制了其可扩展性与可解释性。我们提出ModelWisdom，一个利用可视化与大型语言模型的交互式环境，旨在提升TLA+模型检验的可解释性与可操作性。ModelWisdom提供：（i）模型可视化，包括违规状态颜色高亮、从转移边到TLA+代码的可点击链接，以及违规状态与违反属性之间的映射；（ii）图优化，包含基于树的结构化与节点/边折叠以管理大型模型；（iii）模型摘要，通过大型语言模型（LLMs）总结和解释子图，并执行预处理与部分解释；（iv）模型修复，提取错误信息并支持迭代调试。这些功能共同将原始模型检验器输出转化为交互式、可解释的工作流，从而提升对复杂TLA+规约的理解并减少调试工作量。ModelWisdom的网站地址为：https://model-wisdom.pages.dev。演示视频可在 https://www.youtube.com/watch?v=plyZo30VShA 查看。