ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
作者: Zhiyong Chen, Jialun Cao, Chang Xu, Shing-Chi Cheung
分类: cs.SE, cs.AI, cs.FL
发布日期: 2026-02-12
备注: Accepted by FM 2026 Research Track (Tool)
💡 一句话要点
ModelWisdom：集成TLA+模型可视化、理解与修复工具，提升模型检查效率。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: TLA+ 模型检查 形式化方法 可视化 大型语言模型 模型调试 软件验证 状态空间搜索
📋 核心要点
- TLA+模型检查虽强大，但反例解释、状态图理解和模型修复面临挑战，现有工具可解释性不足。
- ModelWisdom利用可视化和大型语言模型，提供交互式环境，增强TLA+模型检查的可解释性和可操作性。
- ModelWisdom集成了模型可视化、图优化、模型摘要和模型修复等功能，简化调试流程，提升理解效率。
📝 摘要（中文）
TLA+中的模型检查提供了强大的正确性保证，但从业者在解释反例、理解大型状态转换图以及修复错误模型方面仍然面临重大挑战。这些困难源于原始模型检查器输出的可解释性有限，以及需要大量手动工作才能将违规追溯到源规范。尽管TLA+工具箱包含状态图查看器，但它仅提供静态的、完全展开的图，没有折叠、颜色突出显示或语义解释，这限制了其可扩展性和可解释性。我们提出了ModelWisdom，这是一个交互式环境，它使用可视化和大型语言模型，使TLA+模型检查更具可解释性和可操作性。ModelWisdom提供：（i）模型可视化，具有彩色违规突出显示，从转换到TLA+代码的点击链接，以及违规状态和损坏属性之间的映射；（ii）图优化，包括基于树的结构和节点/边缘折叠，以管理大型模型；（iii）模型摘要，通过大型语言模型（LLM）总结和解释子图，并执行预处理和部分解释；（iv）模型修复，提取错误信息并支持迭代调试。总之，这些功能将原始模型检查器输出转换为交互式的、可解释的工作流程，从而提高对重要TLA+规范的理解并减少调试工作。
🔬 方法详解
问题定义：TLA+模型检查虽然能提供高置信度的正确性保证，但在实际应用中，开发者难以理解模型检查器输出的反例、难以理解庞大的状态转移图，以及难以定位和修复模型中的错误。现有的TLA+ Toolbox提供的状态图查看器功能有限，缺乏必要的交互性和可解释性，难以应对复杂模型。
核心思路：ModelWisdom的核心思路是利用可视化技术和大型语言模型（LLM）来增强TLA+模型检查的可解释性和可操作性。通过可视化，开发者可以更直观地理解模型的状态和状态转移过程。通过LLM，可以自动生成模型摘要和错误解释，帮助开发者快速定位和修复错误。
技术框架：ModelWisdom包含四个主要模块：模型可视化、图优化、模型摘要和模型修复。模型可视化模块提供彩色违规突出显示和代码链接，方便开发者定位错误。图优化模块通过树结构和节点/边缘折叠来管理大型模型。模型摘要模块使用LLM来总结和解释子图。模型修复模块提取错误信息并支持迭代调试。
关键创新：ModelWisdom的关键创新在于将可视化技术和大型语言模型相结合，为TLA+模型检查提供了一个交互式的、可解释的工作流程。这种集成使得开发者能够更有效地理解和调试TLA+规范，从而提高开发效率和软件质量。
关键设计：ModelWisdom的关键设计包括：(1) 使用颜色编码来突出显示违规状态和转换；(2) 提供从状态转换到TLA+代码的点击链接；(3) 使用树结构和节点/边缘折叠来简化大型状态图；(4) 使用LLM来生成模型摘要和错误解释，具体LLM的选择和prompt设计未知；(5) 提供迭代调试支持，允许开发者逐步修复模型中的错误。
🖼️ 关键图片
📊 实验亮点
论文展示了ModelWisdom在TLA+模型检查中的应用，通过可视化、摘要和修复等功能，显著提升了开发者理解和调试模型的能力。虽然论文中没有提供具体的性能数据或与其他基线的定量比较，但通过演示视频和案例研究，展示了ModelWisdom在提高TLA+模型检查效率方面的潜力。具体提升幅度未知。
🎯 应用场景
ModelWisdom可应用于形式化方法验证、并发程序设计、分布式系统建模等领域。通过提高TLA+模型检查的可解释性和易用性，该工具能够帮助开发者更有效地验证和调试复杂系统，从而提高软件的可靠性和安全性。未来，该工具可以集成到更广泛的软件开发流程中，促进形式化方法的普及。
📄 摘要（原文）
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.