{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:07:50Z","timestamp":1779034070489,"version":"3.51.4"},"publisher-location":"Cham","reference-count":74,"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                    Formal theorem proving with\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt {TLA}^{+}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mi>TLA<\/mml:mi>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language models have shown promise in automating proofs for tactic-based theorem provers like Lean, applying these approaches directly to\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt {TLA}^{+}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mi>TLA<\/mml:mi>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    faces significant challenges due to the hierarchical proof structure of the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt {TLA}^{+}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mi>TLA<\/mml:mi>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    proof system. We present a prompt-based approach that leverages LLMs to guide hierarchical decomposition of complex proof obligations into simpler sub-claims, while relying on symbolic provers for verification. Our key insight is to constrain LLMs to generate normalized claim decompositions rather than complete proofs, significantly reducing syntax errors. We also introduce a benchmark suite of 119 theorems adapted from (1) established mathematical collections and (2) inductive proofs of distributed protocols. Our approach consistently outperforms baseline methods across the benchmark suite.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_32","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:59Z","timestamp":1779033059000},"page":"619-640","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Language Model Guided $$\\text {TLA}^{+}$$ Proof Automation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6895-6308","authenticated-orcid":false,"given":"Yuhao","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1777-493X","authenticated-orcid":false,"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"32_CR1","unstructured":"TLA+ Proof System documentation: Tactics. https:\/\/proofs.tlapl.us\/doc\/web\/content\/Documentation\/Tutorial\/Tactics.html"},{"key":"32_CR2","unstructured":"Anthropic: Claude 3.7 Sonnet (2025). https:\/\/www.anthropic.com\/news\/claude-3-7-sonnet"},{"key":"32_CR3","unstructured":"Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E.W., Radev, D., Avigad, J.: ProofNet: autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433 (2023)"},{"key":"32_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking, MIT Press (2008)"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Beers, R.: Pre-RTL formal verification: an Intel experience. In: Proceedings of the 45th ACM\/IEEE Design Automation Conference, pp. 806\u2013811 (2008)","DOI":"10.1145\/1391469.1391675"},{"key":"32_CR6","doi-asserted-by":"publisher","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151\u2013165. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_13","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty, S.: Ranking LLM-generated loop invariants for program verification. arXiv preprint arXiv:2310.09342 (2023)","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"32_CR8","doi-asserted-by":"publisher","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA\u2009+\u2009 proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 142\u2013148. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_12","DOI":"10.1007\/978-3-642-14203-1_12"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: transforming natural languages to temporal logics using large language models. arXiv preprint arXiv:2305.07766 (2023)","DOI":"10.18653\/v1\/2023.emnlp-main.985"},{"issue":"2","key":"32_CR10","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345\u2013363 (1936)","journal-title":"Am. J. Math."},{"key":"32_CR11","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking, MIT Press (2000)"},{"key":"32_CR12","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Handbook of Model Checking. Presented at the (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"32_CR13","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: NL2SPEC: interactively translating unstructured natural language to temporal logics with large language models. In: International Conference on Computer Aided Verification, pp. 383\u2013396. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"32_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"32_CR15","unstructured":"DeepSeek-AI: Introducing DeepSeek-V3.2-Exp (2025). https:\/\/api-docs.deepseek.com\/news\/news250929"},{"key":"32_CR16","unstructured":"Dong, Q.: A survey on in-context learning. arXiv preprint arXiv:2301.00234 (2022)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: Whole-proof generation and repair with large language models. In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1229\u20131241 (2023)","DOI":"10.1145\/3611643.3616243"},{"key":"32_CR18","unstructured":"Google DeepMind: Gemini 2.0 flash: a powerful workhorse model with low latency and enhanced performance (2025). https:\/\/cloud.google.com\/vertex-ai\/generative-ai\/docs\/models\/gemini\/2-0-flash"},{"key":"32_CR19","unstructured":"Google DeepMind: Gemini 2.5 flash (2025). https:\/\/cloud.google.com\/vertex-ai\/generative-ai\/docs\/models\/gemini\/2-5-flash"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Hackett, F., Rowe, J., Kuppe, M.A.: Understanding inconsistency in azure cosmos DB with TLA. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), pp. 1\u201312. IEEE (2023)","DOI":"10.1109\/ICSE-SEIP58684.2023.00006"},{"key":"32_CR21","unstructured":"Ho, N., Schmid, L., Yun, S.Y.: Large language models are reasoning teachers. arXiv preprint arXiv:2212.10071 (2022)"},{"key":"32_CR22","unstructured":"Jiang, A.Q.: Draft, sketch, and prove: guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283 (2022)"},{"key":"32_CR23","unstructured":"Kasibatla, S.R., Agarwal, A., Brun, Y., Lerner, S., Ringer, T., First, E.: Cobblestone: a divide-and-conquer approach for automating formal verification. arXiv preprint arXiv:2410.19940 (2024)"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Klein, G.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"32_CR25","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kuppe, M., Merz, S.: Specification and verification with the TLA+ trifecta: TLC, Apalache, and TLAPS. In: International Symposium on Leveraging Applications of Formal Methods, pp. 88\u2013105. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_6","DOI":"10.1007\/978-3-031-19849-6_6"},{"key":"32_CR26","unstructured":"Lamport, L.: Specifying systems: the TLA+ language and tools for hardware and software engineers (2002)"},{"key":"32_CR27","unstructured":"LangChain-AI: LangChain (2022). https:\/\/github.com\/langchain-ai\/langchain"},{"key":"32_CR28","unstructured":"Lewis, P.: Retrieval-augmented generation for knowledge-intensive NLP tasks. In: Advances in Neural Information Processing Systems, vol. 33, pp. 9459\u20139474 (2020)"},{"key":"32_CR29","unstructured":"Liang, Z.: Towards solving more challenging IMO problems via decoupled reasoning and proving. arXiv preprint arXiv:2507.06804 (2025)"},{"key":"32_CR30","unstructured":"Loughridge, C.: DafnyBench: a benchmark for formal software verification. arXiv preprint arXiv:2406.08467 (2024)"},{"key":"32_CR31","unstructured":"Megill, N., Wheeler, D.A.: Metamath: a computer language for mathematical proofs. Lulu. com, (2019)"},{"key":"32_CR32","unstructured":"Mirzadeh, I., Alizadeh, K., Shahrokhi, H., Tuzel, O., Bengio, S., Farajtabar, M.: GSM-symbolic: understanding the limitations of mathematical reasoning in large language models. arXiv preprint arXiv:2410.05229 (2024)"},{"key":"32_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"issue":"OOPSLA1","key":"32_CR34","doi-asserted-by":"publisher","first-page":"1519","DOI":"10.1145\/3720499","volume":"9","author":"E Mugnier","year":"2025","unstructured":"Mugnier, E., Gonzalez, E.A., Polikarpova, N., Jhala, R., Yuanyuan, Z.: Laurel: unblocking automated verification with large language models. Proc. ACM Program. Lang. 9(OOPSLA1), 1519\u20131545 (2025)","journal-title":"Proc. ACM Program. Lang."},{"key":"32_CR35","doi-asserted-by":"publisher","unstructured":"Newcombe, C.: Why amazon chose TLA+. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 25\u201339. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_3","DOI":"10.1007\/978-3-662-43652-3_3"},{"issue":"4","key":"32_CR36","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015). https:\/\/doi.org\/10.1145\/2699417","journal-title":"Commun. ACM"},{"key":"32_CR37","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9_5","DOI":"10.1007\/3-540-45949-9_5"},{"key":"32_CR38","unstructured":"OpenAI: OpenAI GPT-5 system card (2025). https:\/\/openai.com\/index\/gpt-5-system-card\/"},{"key":"32_CR39","unstructured":"OpenAI: OpenAI o3-mini system card (2025). https:\/\/cdn.openai.com\/o3-mini-system-card-feb10.pdf"},{"key":"32_CR40","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0030558","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. Springer (1994). https:\/\/doi.org\/10.1007\/bfb0030558","journal-title":"Springer"},{"key":"32_CR41","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 (2020)"},{"key":"32_CR42","unstructured":"Ren, Z.: DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801 (2025)"},{"key":"32_CR43","doi-asserted-by":"crossref","unstructured":"Rubin, O., Herzig, J., Berant, J.: Learning to retrieve prompts for in-context learning. arXiv preprint arXiv:2112.08633 (2021)","DOI":"10.18653\/v1\/2022.naacl-main.191"},{"key":"32_CR44","unstructured":"Schultz, W.: GitHub repository for plain and simple inductive invariant inference for distributed protocols in TLA+. https:\/\/github.com\/will62794\/endive"},{"key":"32_CR45","doi-asserted-by":"publisher","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Formal verification of a distributed dynamic reconfiguration protocol. In: CPP 2022, Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 143\u2013152. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503688","DOI":"10.1145\/3497775.3503688"},{"key":"32_CR46","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Plain and simple inductive invariant inference for distributed protocols in TLA. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 273\u2013283. IEEE (2022)"},{"key":"32_CR47","doi-asserted-by":"publisher","unstructured":"Schultz, W., Zhou, S., Dardik, I., Tripakis, S.: Design and analysis of a logless dynamic reconfiguration protocol. In: Bramas, Q., Gramoli, V., Milani, A. (eds.) 25th International Conference on Principles of Distributed Systems (OPODIS 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 217, pp. 26:1\u201326:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2021.26, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2022\/15801","DOI":"10.4230\/LIPIcs.OPODIS.2021.26"},{"key":"32_CR48","doi-asserted-by":"crossref","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: closed-loop verifiable code generation. arXiv preprint arXiv:2310.17807 (2023)","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"32_CR49","doi-asserted-by":"publisher","unstructured":"Tahat, A., Hardin, D., Petz, A., Alexander, P.: Proof repair utilizing large language models: a case study on the copland remote attestation proofbase. In: International Conference on Bridging the Gap between AI and Reality, pp. 145\u2013166. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_10","DOI":"10.1007\/978-3-031-75434-0_10"},{"key":"32_CR50","unstructured":"Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., Chaudhuri, S.: An in-context learning agent for formal theorem-proving. In: First Conference on Language Modeling (2023)"},{"key":"32_CR51","unstructured":"The Rocq Development Team: The Rocq reference manual - release 8.19.0 (2025). https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman"},{"key":"32_CR52","doi-asserted-by":"publisher","unstructured":"Thompson, K., et al.: Rango: adaptive retrieval-augmented proving for automated software verification. In: 47th IEEE\/ACM International Conference on Software Engineering, ICSE 2025, Ottawa, ON, Canada, April 26 - May 6, 2025, pp. 347\u2013359. IEEE (2025). https:\/\/doi.org\/10.1109\/ICSE55347.2025.00161","DOI":"10.1109\/ICSE55347.2025.00161"},{"key":"32_CR53","unstructured":"TLA+ Community: tree-sitter-tlaplus: TLA+ grammar for tree-sitter (2023). https:\/\/github.com\/tlaplus-community\/tree-sitter-tlaplus"},{"key":"32_CR54","unstructured":"TLA+ Foundation: Examples of TLA+ specifications (2025). https:\/\/github.com\/tlaplus\/Examples"},{"key":"32_CR55","unstructured":"TLA+ Foundation: The TLA+ proof system (2025). https:\/\/github.com\/tlaplus\/tlapm"},{"issue":"345\u2013363","key":"32_CR56","first-page":"5","volume":"58","author":"AM Turing","year":"1936","unstructured":"Turing, A.M., et al.: On computable numbers, with an application to the Entscheidungsproblem. J. Math 58(345\u2013363), 5 (1936)","journal-title":"J. Math"},{"key":"32_CR57","unstructured":"Varambally, S., Voice, T., Sun, Y., Chen, Z., Yu, R., Ye, K.: Hilbert: recursively building formal proofs with informal reasoning. arXiv preprint arXiv:2509.22819 (2025)"},{"key":"32_CR58","doi-asserted-by":"crossref","unstructured":"Wang, H.: Proving theorems recursively. In: Advances in Neural Information Processing Systems, vol. 37, pp. 86720\u201386748 (2024)","DOI":"10.52202\/079017-2753"},{"key":"32_CR59","unstructured":"Wang, H.: LEGO-prover: neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656 (2023)"},{"key":"32_CR60","doi-asserted-by":"crossref","unstructured":"Wang, R.: TheoremLlama: transforming general-purpose LLMs into Lean4 experts. arXiv preprint arXiv:2407.03203 (2024)","DOI":"10.18653\/v1\/2024.emnlp-main.667"},{"key":"32_CR61","doi-asserted-by":"crossref","unstructured":"Wei, J.: Chain-of-Thought prompting elicits reasoning in large language models. In: Advances in Neural Information Processing Systems, vol. 35, pp. 24824\u201324837 (2022)","DOI":"10.52202\/068431-1800"},{"key":"32_CR62","doi-asserted-by":"publisher","unstructured":"Wen, C.: 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). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"32_CR63","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: integrating large language models in automated program verification. arXiv preprint arXiv:2310.04870 (2023)"},{"key":"32_CR64","unstructured":"Xin, H.: DeepSeek-Prover-V1.5: harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. arXiv preprint arXiv:2408.08152 (2024)"},{"key":"32_CR65","unstructured":"Yang, K.: LeanDojo: theorem proving with retrieval-augmented language models. In: Advances in Neural Information Processing Systems, vol. 36 (2024)"},{"key":"32_CR66","unstructured":"Yao, S.: Tree of thoughts: deliberate problem solving with large language models. In: Advances in Neural Information Processing Systems, vol. 36 (2024)"},{"key":"32_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"},{"key":"32_CR68","doi-asserted-by":"crossref","unstructured":"Zhang, L., Lu, S., Duan, N.: Selene: pioneering automated proof in software verification. arXiv preprint arXiv:2401.07663 (2024)","DOI":"10.18653\/v1\/2024.acl-long.98"},{"key":"32_CR69","unstructured":"Zhang, S.D., Ringer, T., First, E.: Getting more out of large language models for proofs. arXiv preprint arXiv:2305.04369 (2023)"},{"key":"32_CR70","unstructured":"Zhang, Y.: LLM as a mastermind: a survey of strategic reasoning with large language models. arXiv preprint arXiv:2404.01230 (2024)"},{"key":"32_CR71","unstructured":"Zheng, K., Han, J.M., Polu, S.: MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110 (2021)"},{"key":"32_CR72","unstructured":"Zhou, Y.: GitHub repository for language-model guided TLA+ proof automation (2026). https:\/\/github.com\/YUH-Z\/lmgpa"},{"key":"32_CR73","unstructured":"Zhou, Y., Tripakis, S.: Towards language model guided TLA+ proof automation. arXiv:2512.09758 (2025)"},{"key":"32_CR74","doi-asserted-by":"publisher","unstructured":"Zhou, Y., Tripakis, S.: Artifact for paper: language-model guided TLA+ proof automation (2026). https:\/\/doi.org\/10.5281\/zenodo.18637323","DOI":"10.5281\/zenodo.18637323"}],"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_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:08Z","timestamp":1779033068000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_32","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"}}]}}