{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,22]],"date-time":"2026-05-22T04:08:36Z","timestamp":1779422916423,"version":"3.53.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T00:00:00Z","timestamp":1779753600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2133516"],"award-info":[{"award-number":["2133516"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,5,26]]},"DOI":"10.1145\/3786335.3813159","type":"proceedings-article","created":{"date-parts":[[2026,5,22]],"date-time":"2026-05-22T03:16:22Z","timestamp":1779419782000},"page":"181-196","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7459-7080","authenticated-orcid":false,"given":"Shuren","family":"Xia","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, Rutgers University, New Brunswick, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4013-4097","authenticated-orcid":false,"given":"Qiwei","family":"Li","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Rutgers University, New Brunswick, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1300-5379","authenticated-orcid":false,"given":"Taqiya","family":"Ehsan","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Rutgers University, New Brunswick, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3325-1298","authenticated-orcid":false,"given":"Jorge","family":"Ortiz","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Rutgers University, New Brunswick, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,5,26]]},"reference":[{"key":"e_1_3_3_1_2_2","unstructured":"Rajeev Alur Mukund Raghothaman Christos Stergiou Stavros Tripakis and Abhishek Udupa. 2015. Automatic Completion of Distributed Protocols with Symmetry. arxiv:https:\/\/arXiv.org\/abs\/1505.04409\u00a0[cs.FL] https:\/\/arxiv.org\/abs\/1505.04409"},{"key":"e_1_3_3_1_3_2","unstructured":"Yuntao Bai Saurav Kadavath Sandipan Kundu et\u00a0al. 2022. Constitutional AI: Harmlessness from AI Feedback. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2212.08073 (2022). arxiv:https:\/\/arXiv.org\/abs\/2212.08073\u00a0[cs.CL]"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Laura Bocchi Tzu-Chun Chen Romain Demangeon Kohei Honda and Nobuko Yoshida. 2017. Monitoring Networks through Multiparty Session Types. Theoretical Computer Science 669 (2017) 33\u201358. 10.1016\/j.tcs.2017.02.009","DOI":"10.1016\/j.tcs.2017.02.009"},{"key":"e_1_3_3_1_5_2","unstructured":"Mert Cemri Melissa\u00a0Z. Pan Shuyi Yang Lakshya\u00a0A. Agrawal Bhavya Chopra Rishabh Tiwari Kurt Keutzer Aditya Parameswaran Dan Klein Kannan Ramchandran Matei Zaharia Joseph\u00a0E. Gonzalez and Ion Stoica. 2025. Why Do Multi-Agent LLM Systems Fail? arxiv:https:\/\/arXiv.org\/abs\/2503.13657\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2503.13657"},{"key":"e_1_3_3_1_6_2","unstructured":"Harrison Chase. 2022. LangChain. https:\/\/github.com\/langchain-ai\/langchain. Accessed: 2026-02-16."},{"key":"e_1_3_3_1_7_2","unstructured":"Lingjiao Chen Jared\u00a0Quincy Davis Boris Hanin Peter Bailis Matei Zaharia James Zou and Ion Stoica. 2025. Optimizing model selection for compound ai systems. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2502.14815 (2025)."},{"key":"e_1_3_3_1_8_2","unstructured":"Zhiyong Chen Jialun Cao Chang Xu and Shing-Chi Cheung. 2026. ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization Digest and Repair. arxiv:https:\/\/arXiv.org\/abs\/2602.12058\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2602.12058"},{"key":"e_1_3_3_1_9_2","unstructured":"Zhaorun Chen Mintong Kang and Bo Li. 2025. ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning. arxiv:https:\/\/arXiv.org\/abs\/2503.22738\u00a0[cs.LG] https:\/\/arxiv.org\/abs\/2503.22738"},{"key":"e_1_3_3_1_10_2","unstructured":"Qian Cheng Ruize Tang Emilie Ma Finn Hackett Peiyang He Yiming Su Ivan Beschastnikh Yu Huang Xiaoxing Ma and Tianyin Xu. 2025. SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems. arxiv:https:\/\/arXiv.org\/abs\/2509.23130\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2509.23130"},{"key":"e_1_3_3_1_11_2","volume-title":"Model Checking","author":"Clarke Edmund\u00a0M.","year":"1999","unstructured":"Edmund\u00a0M. Clarke, Orna Grumberg, and Doron\u00a0A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_3_1_12_2","unstructured":"Inc. CrewAI and contributors. 2026. CrewAI. GitHub repository. https:\/\/github.com\/crewAIInc\/crewAI Accessed: 2026-02-16."},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Edsger\u00a0W. Dijkstra. 1971. Hierarchical Ordering of Sequential Processes. Acta Informatica 1 2 (1971) 115\u2013138. 10.1007\/BF00289519","DOI":"10.1007\/BF00289519"},{"key":"e_1_3_3_1_14_2","unstructured":"Marius-Constantin Dinu Claudiu Leoveanu-Condrei Markus Holzleitner Werner Zellinger and Sepp Hochreiter. 2024. SymbolicAI: A framework for logic-based approaches combining generative models and solvers. arxiv:https:\/\/arXiv.org\/abs\/2402.00854\u00a0[cs.LG] https:\/\/arxiv.org\/abs\/2402.00854"},{"key":"e_1_3_3_1_15_2","unstructured":"Derek Egolf William Schultz and Stavros Tripakis. 2024. Efficient Synthesis of Symbolic Distributed Protocols by Sketching. arxiv:https:\/\/arXiv.org\/abs\/2405.07807\u00a0[cs.LO] https:\/\/arxiv.org\/abs\/2405.07807"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Alessio Ferrari and Paola Spoletini. 2025. Formal requirements engineering and large language models: A two-way roadmap. Information and Software Technology (2025). 10.1016\/j.infsof.2025.107697","DOI":"10.1016\/j.infsof.2025.107697"},{"key":"e_1_3_3_1_17_2","unstructured":"Yannai\u00a0A. Gonczarowski. 2012. Timely Coordination in a Multi-Agent System. The Hebrew University of Jerusalem. https:\/\/yannai.gonch.name\/scientific\/papers\/2012-timely-coordination-huji.pdf Undergraduate thesis."},{"key":"e_1_3_3_1_18_2","unstructured":"Google and contributors. 2026. ADK (Agent Development Kit) for Python. GitHub repository. https:\/\/github.com\/google\/adk-python Accessed: 2026-02-16."},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_3_1_20_2","unstructured":"Omar Khattab Arnav Singhvi Paridhi Maheshwari Zhiyuan Zhang Keshav Santhanam Sri Vardhamanan Saiful Haq Ashutosh Sharma Thomas\u00a0T. Joshi Hanna Moazam Heather Miller Matei Zaharia and Christopher Potts. 2024. DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines. The Twelfth International Conference on Learning Representations."},{"key":"e_1_3_3_1_21_2","unstructured":"Roham Koohestani. 2025. AgentGuard: Runtime Verification of AI Agents. arxiv:https:\/\/arXiv.org\/abs\/2509.23864\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2509.23864"},{"key":"e_1_3_3_1_22_2","unstructured":"Saul\u00a0A Kripke. 1963. Semantical considerations on modal logic. Acta philosophica fennica 16 (1963)."},{"key":"e_1_3_3_1_23_2","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston, MA, USA."},{"key":"e_1_3_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"e_1_3_3_1_25_2","doi-asserted-by":"crossref","unstructured":"Leslie Lamport Robert Shostak and Marshall Pease. 1982. The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems 4 3 (1982) 382\u2013401.","DOI":"10.1145\/357172.357176"},{"key":"e_1_3_3_1_26_2","unstructured":"Inc. LangChain and contributors. 2026. LangGraph. GitHub repository. https:\/\/github.com\/langchain-ai\/langgraph Accessed: 2026-02-16."},{"key":"e_1_3_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Martin Leucker and Christian Schallhart. 2009. A Brief Account of Runtime Verification. Journal of Logic and Algebraic Programming 78 5 (2009) 293\u2013303. 10.1016\/j.jlap.2008.08.004","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_3_3_1_28_2","unstructured":"Shuang Li Jing Yang et\u00a0al. 2023. TaskMatrix.AI: Completing Tasks by Connecting Foundation Models with Millions of APIs. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2303.16434 (2023). arxiv:https:\/\/arXiv.org\/abs\/2303.16434\u00a0[cs.AI]"},{"key":"e_1_3_3_1_29_2","doi-asserted-by":"crossref","unstructured":"Yujia Li David Choi Junyoung Chung et\u00a0al. 2022. Competition-Level Code Generation with AlphaCode. Science 378 6624 (2022) 1092\u20131097.","DOI":"10.1126\/science.abq1158"},{"key":"e_1_3_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Chris Newcombe Tim Rath Fan Zhang Bogdan Munteanu Marc Brooker and Michael Deardeuff. 2015. How Amazon Web Services Uses Formal Methods. Commun. ACM 58 4 (2015) 66\u201373. 10.1145\/26994172699417\"\/>","DOI":"10.1145\/2699417"},{"key":"e_1_3_3_1_31_2","unstructured":"Ansong Ni Srinivasan Iyer and Dragomir Radev. 2023. LEVER: Learning to Verify Language-to-Code Generation with Execution. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2302.08468 (2023). arxiv:https:\/\/arXiv.org\/abs\/2302.08468\u00a0[cs.CL]"},{"key":"e_1_3_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_3_1_33_2","unstructured":"Dhananjay Raju Suda Bharadwaj and Ufuk Topcu. 2019. Online Synthesis for Runtime Enforcement of Safety in Multi-Agent Systems. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/1910.10380 (2019). arxiv:https:\/\/arXiv.org\/abs\/1910.10380\u00a0[cs.SY]"},{"key":"e_1_3_3_1_34_2","unstructured":"Keshav Ramani Vali Tawosi Salwa Alamir and Daniel Borrajo. 2025. Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification. arxiv:https:\/\/arXiv.org\/abs\/2510.03469\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2510.03469"},{"key":"e_1_3_3_1_35_2","first-page":"431","volume-title":"Proceedings of the 2023 conference on empirical methods in natural language processing: system demonstrations","author":"Rebedea Traian","year":"2023","unstructured":"Traian Rebedea, Razvan Dinu, Makesh\u00a0Narsimhan Sreedhar, Christopher Parisien, and Jonathan Cohen. 2023. NeMo Guardrails: A Toolkit for Controllable and Safe LLM Applications with Programmable Rails. In Proceedings of the 2023 conference on empirical methods in natural language processing: system demonstrations. 431\u2013445."},{"key":"e_1_3_3_1_36_2","unstructured":"Vikash Singh Darion Cassel Nathaniel Weir Nick Feng and Sam Bayless. 2026. VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning. arxiv:https:\/\/arXiv.org\/abs\/2601.20055\u00a0[cs.CL] https:\/\/arxiv.org\/abs\/2601.20055"},{"key":"e_1_3_3_1_37_2","unstructured":"Chuyue Sun Ying Sheng Oded Padon and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. arxiv:https:\/\/arXiv.org\/abs\/2310.17807\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2310.17807"},{"key":"e_1_3_3_1_38_2","unstructured":"Haoyu Wang Christopher\u00a0M. Poskitt Jun Sun and Jiali Wei. 2025. Pro2Guard: Proactive Runtime Enforcement of LLM Agent Safety via Probabilistic Model Checking. arxiv:https:\/\/arXiv.org\/abs\/2508.00500\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2508.00500"},{"key":"e_1_3_3_1_39_2","first-page":"24824","volume-title":"Advances in Neural Information Processing Systems","volume":"35","author":"Wei Jason","year":"2022","unstructured":"Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc\u00a0V Le, and Denny Zhou. 2022. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. In Advances in Neural Information Processing Systems, S.\u00a0Koyejo, S.\u00a0Mohamed, A.\u00a0Agarwal, D.\u00a0Belgrave, K.\u00a0Cho, and A.\u00a0Oh (Eds.), Vol.\u00a035. Curran Associates, Inc., 24824\u201324837. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/9d5609613524ecf4f15af0f7b31abca4-Paper-Conference.pdf"},{"key":"e_1_3_3_1_40_2","unstructured":"will62794 and contributors. 2026. TLA+ Web Explorer (tla-web). GitHub repository. https:\/\/github.com\/will62794\/tla-web Accessed: 2026-02-21."},{"key":"e_1_3_3_1_41_2","unstructured":"Qingyun Wu Gagan Bansal Jieyu Zhang Yiran Wu Beibin Li Erkang Zhu Li Jiang Xiaoyun Zhang Shaokun Zhang Jiale Liu Ahmed\u00a0Hassan Awadallah Ryen\u00a0W. White Doug Burger and Chi Wang. 2023. AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation. arxiv:https:\/\/arXiv.org\/abs\/2308.08155\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2308.08155"},{"key":"e_1_3_3_1_42_2","volume-title":"The eleventh international conference on learning representations","author":"Yao Shunyu","year":"2022","unstructured":"Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik\u00a0R Narasimhan, and Yuan Cao. 2022. React: Synergizing reasoning and acting in language models. In The eleventh international conference on learning representations."},{"key":"e_1_3_3_1_43_2","unstructured":"Yedi Zhang Yufan Cai Xinyue Zuo Xiaokun Luan Kailong Wang Zhe Hou Yifan Zhang Zhiyuan Wei Meng Sun Jun Sun Jing Sun and Jin\u00a0Song Dong. 2024. The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap. arxiv:https:\/\/arXiv.org\/abs\/2412.06512\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2412.06512"},{"key":"e_1_3_3_1_44_2","unstructured":"Yedi Zhang Sun\u00a0Yi Emma Annabelle Lee\u00a0Jia En and Jin\u00a0Song Dong. 2025. RvLLM: LLM Runtime Verification with Domain Knowledge. arxiv:https:\/\/arXiv.org\/abs\/2505.18585\u00a0[cs.AI] https:\/\/arxiv.org\/abs\/2505.18585"},{"key":"e_1_3_3_1_45_2","unstructured":"Kunlun Zhu Hongyi Du Zhaochen Hong Xiaocheng Yang Shuyi Guo Zhe Wang Zhenhailong Wang Cheng Qian Xiangru Tang Heng Ji and Jiaxuan You. 2025. MultiAgentBench: Evaluating the Collaboration and Competition of LLM agents. arxiv:https:\/\/arXiv.org\/abs\/2503.01935\u00a0[cs.MA] https:\/\/arxiv.org\/abs\/2503.01935"}],"event":{"name":"CAIS '26: ACM Conference on AI and Agentic Systems","location":"San Jose CA USA","acronym":"CAIS '26"},"container-title":["Proceedings of the ACM Conference on AI and Agentic Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3786335.3813159","content-type":"text\/html","content-version":"vor","intended-application":"syndication"}],"deposited":{"date-parts":[[2026,5,22]],"date-time":"2026-05-22T03:36:41Z","timestamp":1779421001000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3786335.3813159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,26]]},"references-count":44,"alternative-id":["10.1145\/3786335.3813159","10.1145\/3786335"],"URL":"https:\/\/doi.org\/10.1145\/3786335.3813159","relation":{},"subject":[],"published":{"date-parts":[[2026,5,26]]},"assertion":[{"value":"2026-05-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}