{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T19:11:57Z","timestamp":1783019517846,"version":"3.54.6"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    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\n                    <jats:sc>ModelWisdom<\/jats:sc>\n                    , an interactive environment that uses visualization and large language models to make TLA+ model checking more interpretable and actionable.\n                    <jats:sc>ModelWisdom<\/jats:sc>\n                    \u00a0offers: (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. This tool is available:\n                    <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"https:\/\/github.com\/ModelWisdom\/ModelWisdom\" ext-link-type=\"uri\">https:\/\/github.com\/ModelWisdom\/ModelWisdom<\/jats:ext-link>\n                    . A demonstrative video can be found at\n                    <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"https:\/\/www.youtube.com\/watch?v=plyZo30VShA\" ext-link-type=\"uri\">https:\/\/www.youtube.com\/watch?v=plyZo30VShA<\/jats:ext-link>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_11","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:24Z","timestamp":1779033084000},"page":"211-219","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ModelWisdom: An Integrated Toolkit for\u00a0TLA$$^{+}$$ Model Visualization, Digest and\u00a0Repair (Short Tool Paper)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2555-5728","authenticated-orcid":false,"given":"Zhiyong","family":"Chen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4892-6294","authenticated-orcid":false,"given":"Jialun","family":"Cao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6299-4704","authenticated-orcid":false,"given":"Chang","family":"Xu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3508-7172","authenticated-orcid":false,"given":"Shing-Chi","family":"Cheung","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"issue":"5","key":"11_CR1","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10664-025-10687-1","volume":"30","author":"M Alhanahnah","year":"2025","unstructured":"Alhanahnah, M., Rashedul Hasan, M., Xu, L., Bagheri, H.: An empirical evaluation of pre-trained large language models for repairing declarative formal specifications. Empir. Softw. Eng. 30(5), 149 (2025)","journal-title":"Empir. Softw. Eng."},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized verification with automatically computed inductive assertions? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_19"},{"key":"11_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"11_CR5","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal 4.0. Department of computer science, Aalborg University 1(1), 1\u201348 (2006)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: QEST, vol.\u00a06, pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Cao, J., et al.: From informal to formal \u2013 incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs. In: Che, W., Nabende, J., Shutova, E., Pilehvar, M.T. (eds.) Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 26984\u201327003. Association for Computational Linguistics, Vienna, Austria, July 2025. https:\/\/doi.org\/10.18653\/v1\/2025.acl-long.1310. https:\/\/aclanthology.org\/2025.acl-long.1310\/","DOI":"10.18653\/v1\/2025.acl-long.1310"},{"key":"11_CR8","unstructured":"Chen, X., Gopalakrishnan, G.: A general compositional approach to verifying hierarchical cache coherence protocols. Technical report, Technical Report. UUCS-06-014, School of Computing, University of Utah (2006)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_27"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 54\u201356. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0058022"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp. 135\u2013143. IEEE (2001)","DOI":"10.1109\/ASE.2001.989799"},{"issue":"5","key":"11_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: 2013 Formal Methods in Computer-Aided Design, pp. 201\u2013209. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"11_CR14","unstructured":"Kogler, P., Falkner, A., Sperl, S.: Reliable generation of formal specifications using large language models. In: SE 2024-Companion, pp. 141\u2013153. Gesellschaft f\u00fcr Informatik eV (2024)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Kuppe, M.A.: The TLA+ debugger. In: International Conference on Software Engineering and Formal Methods, pp. 174\u2013180. Springer (2022)","DOI":"10.1007\/978-3-031-26236-4_15"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. arXiv preprint arXiv:1912.10633 (2019)","DOI":"10.4204\/EPTCS.310.6"},{"key":"11_CR17","unstructured":"Lamport, L.: Specifying concurrent systems with TLA+. Calculational System Design, pp. 183\u2013247 (1999)"},{"key":"11_CR18","unstructured":"Lamport, L.: Specifying systems (2002)"},{"issue":"1","key":"11_CR19","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: SpecGen: automated generation of formal program specifications via large language models. In: 2025 IEEE\/ACM 47th International Conference on Software Engineering (ICSE), pp. 16\u201328. IEEE (2025)","DOI":"10.1109\/ICSE55347.2025.00129"},{"key":"11_CR21","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-74107-7_8","volume-title":"Logics of Specification Languages","author":"S Merz","year":"2008","unstructured":"Merz, S.: The specification language TLA+. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of Specification Languages. MTCSAES, pp. 401\u2013451. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74107-7_8"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Qu, Y., Zhang, T., Garg, N., Kumar, A.: Recursive introspection: teaching language model agents how to self-improve. In: Advances in Neural Information Processing Systems, vol. 37, pp. 55249\u201355285 (2024)","DOI":"10.52202\/079017-1754"},{"key":"11_CR23","unstructured":"Song, P., Yang, K., Anandkumar, A.: Towards large language models as copilots for theorem proving in lean. In: The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS\u201923 (2023)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: International Conference on Computer Aided Verification, pp. 302\u2013328. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Yang, K., et al.: LeanDojo: theorem proving with retrieval-augmented language models. In: Advances in Neural Information Processing Systems, vol. 36, pp. 21573\u201321612 (2023)","DOI":"10.52202\/075280-0944"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Zhao, M., Tao, R., Huang, Y., Shi, J., Qin, S., Yang, Y.: NL2CTL: automatic generation of formal requirements specifications via large language models. In: International Conference on Formal Engineering Methods, pp. 1\u201317. Springer (2024)","DOI":"10.1007\/978-981-96-0617-7_1"},{"issue":"3\u20134","key":"11_CR27","first-page":"139","volume":"30","author":"L Zuck","year":"2004","unstructured":"Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3\u20134), 139\u2013169 (2004)","journal-title":"Comput. Lang. Syst. Struct."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:58:06Z","timestamp":1783015086000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}