{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:17Z","timestamp":1784793797036,"version":"3.55.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","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,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"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                    The TLA\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$^+$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow\/>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    language has been widely used, both in academia and industry, to specify and reason about distributed systems. This paper presents\n                    <jats:sc>Apalache<\/jats:sc>\n                    , an efficient and flexible symbolic model checker for TLA\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$^+$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow\/>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    .\n                    <jats:sc>Apalache<\/jats:sc>\n                    \u2019s engine is based on bounded model checking, with symbolic transitions being extracted from TLA\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$^+$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow\/>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    specifications and verification conditions suitable for satisfiability modulo theories (SMT) solvers being generated from them. Reasoning can be done in terms of safety and liveness properties, with liveness checking realised via a liveness-to-safety reduction.\n                    <jats:sc>Apalache<\/jats:sc>\n                    \u2019s flexibility lies in its three complementary functionalities: bounded exhaustive verification, for bounded guarantees, randomised symbolic execution, for prototyping and bug detection, and inductiveness checking, for unbounded guarantees. The paper describes\n                    <jats:sc>Apalache<\/jats:sc>\n                    \u2019s architecture and features, including its support for PlusCal and Quint, two languages that share the same semantic foundation as TLA\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$^+$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow\/>\n                            <mml:mo>+<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . Industrial usage of\n                    <jats:sc>Apalache<\/jats:sc>\n                    is also presented, together with a case study which illustrates how\n                    <jats:sc>Apalache<\/jats:sc>\n                    can be used to verify the agreement property of a consensus protocol.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_8","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:10Z","timestamp":1784791090000},"page":"151-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The TLA+ Model Checker Apalache"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1097-2367","authenticated-orcid":false,"given":"Rodrigo","family":"Otoni","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3976-3457","authenticated-orcid":false,"given":"Shon","family":"Feder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1094-773X","authenticated-orcid":false,"given":"Jure","family":"Kukovec","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2952-2800","authenticated-orcid":false,"given":"Andrey","family":"Kupriyanov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0275-5717","authenticated-orcid":false,"given":"Gabriela","family":"Moreira","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8477-2849","authenticated-orcid":false,"given":"Philip","family":"Offtermatt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4434-0248","authenticated-orcid":false,"given":"Thomas","family":"Pani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2260-6877","authenticated-orcid":false,"given":"Thanh-Hai","family":"Tran","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6629-3377","authenticated-orcid":false,"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Ben-Or, M.: Another advantage of free choice (extended abstract): completely asynchronous agreement protocols. In: Proceedings of the 2nd ACM Symposium on Principles of Distributed Computing (PODC 1983), pp. 27\u201330 (1983). https:\/\/doi.org\/10.1145\/800221.806707","DOI":"10.1145\/800221.806707"},{"issue":"5","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1\u201363 (2006). https:\/\/doi.org\/10.2168\/LMCS-2(5:5)2006","journal-title":"Log. Methods Comput. Sci."},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Split transition power abstraction for unbounded safety. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD 2022), pp. 349\u2013358 (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_42","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_42"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). LNCS, vol. 13243, pp. 524\u2013542. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Braithwaite, S., et al.: Tendermint blockchain synchronization: formal specification and model checking. In: Proceedings of the 11th International Symposium On Leveraging Applications of Formal Methods (ISoLA 2020). LNCS, vol. 12476, pp. 471\u2013488. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_27","DOI":"10.1007\/978-3-030-61362-4_27"},{"issue":"6","key":"8_CR7","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/3729175","volume":"68","author":"M Brooker","year":"2025","unstructured":"Brooker, M., Desai, A.: Systems correctness practices at amazon web services. Commun. ACM 68(6), 38\u201342 (2025). https:\/\/doi.org\/10.1145\/3729175","journal-title":"Commun. ACM"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA+ proof system: building a heterogeneous verification platform. In: Proceedings of the 7th International Colloquium on the Theoretical Aspects of Computing (ICTAC 2010). LNCS, vol. 6255, pp. 44\u201344. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14808-8_3","DOI":"10.1007\/978-3-642-14808-8_3"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"8_CR10","unstructured":"Commonware Inc.: Minimmit Formal Specification (2025). https:\/\/github.com\/commonwarexyz\/monorepo\/tree\/main\/pipeline\/minimmit\/quint"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Dardik, I., Kang, E.: Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning (2025). https:\/\/doi.org\/10.48550\/arXiv.2509.06250","DOI":"10.48550\/arXiv.2509.06250"},{"issue":"6","key":"8_CR12","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/2499370.2462184","volume":"48","author":"A Desai","year":"2013","unstructured":"Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., Zufferey, D.: P: safe asynchronous event-driven programming. ACM SIGPLAN Not. 48(6), 321\u2013332 (2013). https:\/\/doi.org\/10.1145\/2499370.2462184","journal-title":"ACM SIGPLAN Not."},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Desai, A., Phanishayee, A., Qadeer, S., Seshia, S.A.: Compositional programming and testing of dynamic distributed systems. Proc. ACM Program. Lang. 2(OOPSLA), 1\u201330 (2018). https:\/\/doi.org\/10.1145\/3276529","DOI":"10.1145\/3276529"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Fran\u00e7a, B., Kolegov, D., Konnov, I., Prusak, G.: ChonkyBFT: Consensus Protocol of ZKsync (2025). https:\/\/doi.org\/10.48550\/arXiv.2503.15380","DOI":"10.48550\/arXiv.2503.15380"},{"key":"8_CR15","unstructured":"Gr\u00e9goire, J.C., Jefferson, D., Yu, Y.: SANY Syntactic Analyzer. https:\/\/lamport.azurewebsites.net\/tla\/tools.html"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Hackett, F., Rowe, J., Kuppe, M.A.: Understanding inconsistency in azure cosmos DB with TLA+. In: Proceedings of the 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP 2023), pp. 1\u201312 (2023). https:\/\/doi.org\/10.1109\/ICSE-SEIP58684.2023.00006","DOI":"10.1109\/ICSE-SEIP58684.2023.00006"},{"key":"8_CR17","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: it\u2019s a small (enough) world after all. In: Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2021), pp. 115\u2013131 (2021). https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: Proceedings of the 9th International Conference on Integrated Formal Methods (IFM 2012). LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3","DOI":"10.1007\/978-3-642-30729-4_3"},{"issue":"9","key":"8_CR19","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019). https:\/\/doi.org\/10.1145\/3338843","journal-title":"Commun. ACM"},{"key":"8_CR20","unstructured":"Kolegov, D., Konnov, I.: ZKsync Governance\u2019s Quint Specification (2024). https:\/\/github.com\/zksync-association\/zk-governance\/tree\/master\/spec"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kukovec, J., Pani, T., Saltini, R., Tran, T.H.: Exploring Automatic Model-Checking of the Ethereum Specification (2025). https:\/\/doi.org\/10.48550\/arXiv.2501.07958","DOI":"10.48550\/arXiv.2501.07958"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kukovec, J., Tran, T.H.: TLA+ model checking made symbolic. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3360549","DOI":"10.1145\/3360549"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kuppe, M., Merz, S.: Specification and verification with the TLA+ trifecta: TLC, Apalache, and TLAPS. In: Proceedings of the 11th International Symposium On Leveraging Applications of Formal Methods (ISoLA 2022), pp. 88\u2013105 (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_6","DOI":"10.1007\/978-3-031-19849-6_6"},{"key":"8_CR24","unstructured":"Konnov, I., Pani, T.: Aztec Governance Formal Specification and Verification (2025). https:\/\/github.com\/konnov\/aztec-governance-formal-verification-2025q3"},{"key":"8_CR25","unstructured":"Kukovec, J., Konnov, I.: Type inference for TLA+ in Apalache. In: Summaries of the 2020 TLA+ Community Event (2020). https:\/\/conf.tlapl.us\/2020\/07-Kukovec_and_Konnov-Type_Inference_for_TLA_+_in_Apalache.pdf"},{"key":"8_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102361","volume":"187","author":"J Kukovec","year":"2020","unstructured":"Kukovec, J., Tran, T.H., Konnov, I.: Extracting symbolic transitions from TLA+ specifications. Sci. Comput. Program. 187, 102361 (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102361","journal-title":"Sci. Comput. Program."},{"key":"8_CR27","unstructured":"Kulagin, D.: Validation Test Suite for TLA+ (2025). https:\/\/github.com\/tlaplus\/ValidationTestSuite"},{"key":"8_CR28","unstructured":"Kupriyanov, A., Konnov, I.: Model-based testing with TLA+ and apalache. In: Summaries of the 2020 TLA+ Community Event (2020). https:\/\/conf.tlapl.us\/2020\/09-Kuprianov_and_Konnov-Model-based_testing_with_TLA_+_and_Apalache.pdf"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Kushwah, S., Desai, A., Subramanyan, P., Seshia, S.A.: PSec: programming secure distributed systems using enclaves. In: Proceedings of the 16th ACM Asia Conference on Computer and Communications Security (ASIA CCS 2021), pp. 802\u2013816 (2021). https:\/\/doi.org\/10.1145\/3433210.3453113","DOI":"10.1145\/3433210.3453113"},{"issue":"3","key":"8_CR30","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR31","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional (2002). https:\/\/lamport.azurewebsites.net\/tla\/book.html"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Lamport, L.: The PlusCal algorithm language. In: Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC 2009). LNCS, vol. 5684, pp. 36\u201360. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03466-4_2","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Proceedings of the 12th International Symposium of Formal Methods Europe (FME 2003). LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"8_CR34","unstructured":"Losa, G., Merz, S.: Distributed Termination Detection - Verified with Apalache, Isabelle\/HOL, and TLAPS (2022). https:\/\/github.com\/nano-o\/distributed-termination-detection"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: Proceedings of the 25th International Static Analysis Symposium (SAS 2018). LNCS, vol. 11002, pp. 43\u201355. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_4","DOI":"10.1007\/978-3-319-99725-4_4"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Proceedings of the 32nd International Conference on Computer Aided Verification (CAV 2020). LNCS, vol. 12225, pp. 190\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Moreira, G., Vasconcellos, C., Kniess, J.: Fully-tested code generation from TLA+ specifications. In: Proceedings of the 7th Brazilian Symposium on Systematic and Automated Software Testing (SAST 2022), pp. 19\u201328 (2022). https:\/\/doi.org\/10.1145\/3559744.3559747","DOI":"10.1145\/3559744.3559747"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Proceedings of the 28th International Conference on Automated Deduction (CADE 2021). LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"issue":"4","key":"8_CR40","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":"8_CR41","unstructured":"Offtermatt, P., Kukovec, J., Konnov, I.: Extending apalache to symbolically reason about temporal properties of TLA+. In: Summaries of the 2022 TLA+ Conference (2022). https:\/\/conf.tlapl.us\/2022\/sub3.pdf"},{"issue":"4","key":"8_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3716505","volume":"37","author":"R Otoni","year":"2025","unstructured":"Otoni, R., Blicha, M., Eugster, P., Sharygina, N.: Validation of CHC satisfiability with ATHENA. Formal Aspects Comput. 37(4), 1\u201320 (2025). https:\/\/doi.org\/10.1145\/3716505","journal-title":"Formal Aspects Comput."},{"key":"8_CR43","doi-asserted-by":"publisher","unstructured":"Otoni, R., Blicha, M., Rivera, M.B., Eugster, P., Kofro\u0148, J., Sharygina, N.: Unsatisfiability proofs for horn solving. In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), pp. 67\u201387 (2025). https:\/\/doi.org\/10.1007\/978-3-031-90653-4_4","DOI":"10.1007\/978-3-031-90653-4_4"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"Otoni, R., Konnov, I., Kukovec, J., Eugster, P., Sharygina, N.: Symbolic model checking for TLA+ made faster. In: Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), pp. 126\u2013144 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_7","DOI":"10.1007\/978-3-031-30823-9_7"},{"key":"8_CR45","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2(POPL), 1\u201333 (2017). https:\/\/doi.org\/10.1145\/3158114","DOI":"10.1145\/3158114"},{"key":"8_CR46","doi-asserted-by":"publisher","unstructured":"P\u00eerlea, G., Gladshtein, V., Kinsbruner, E., Zhao, Q., Sergey, I.: Veil: a framework for automated and interactive verification of transition systems. In: Proceedings of the 37th International Conference on Computer Aided Verification (CAV 2025), pp. 26\u201341 (2025). https:\/\/doi.org\/10.1007\/978-3-031-98682-6_2","DOI":"10.1007\/978-3-031-98682-6_2"},{"key":"8_CR47","doi-asserted-by":"publisher","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Plain and simple inductive invariant inference for distributed protocols in TLA+. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, pp. 273\u2013283 (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_34","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_34"},{"key":"8_CR48","doi-asserted-by":"publisher","unstructured":"Schultz, W., Demirbas, M.: Design and modular verification of distributed transactions in MongoDB. Proc. VLDB Endow. 18(12), 5045\u20135058 (2025). https:\/\/doi.org\/10.14778\/3750601.3750626","DOI":"10.14778\/3750601.3750626"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"Tran, T.-H., Konnov, I., Widder, J.: A case study on parametric verification of failure detectors. In: Proceedings of the 41st International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2021). LNCS, vol. 12719, pp. 138\u2013156. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_8","DOI":"10.1007\/978-3-030-78089-0_8"},{"key":"8_CR50","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: fast, automated inference of inductive invariants for verifying distributed protocols. In: Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022), pp. 485\u2013501 (2022). https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Yu, Q., Losa, G., Wang, X.: TetraBFT: reducing latency of unauthenticated, responsive BFT consensus. In: Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing (PODC 2024), pp. 257\u2013267 (2024). https:\/\/doi.org\/10.1145\/3662158.3662783","DOI":"10.1145\/3662158.3662783"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing (CHARME 1999). LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:13Z","timestamp":1784791093000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_8","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":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}