{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T19:11:17Z","timestamp":1782846677613,"version":"3.54.5"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T00:00:00Z","timestamp":1782777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>Building software that is correct by construction is a long-standing goal in software engineering, as it ensures reliability during design and development rather than after deployment. Formal methods realize this vision by enabling the expression of system behavior and requirements in mathematics, thereby guaranteeing correctness through formal verification, including theorem proving and model checking. However, the steep learning curve and demand for mathematical expertise hinder the widespread adoption of formal methods. Large language models (LLMs) have recently shown promise in bridging this gap through autoformalization. However, existing LLM-based approaches are largely limited to isolated tasks, such as theorem proving without formalization or model synthesis with insufficient verification. While valuable, these efforts do not fully exploit the potential of a more comprehensive framework in which models and proofs evolve together, a process that closely reflects real-world development practice. To address this gap, we propose Event-B Agent, a novel framework inspired by the interleaved nature of software design. Given natural language requirements, Event-B Agent constructs an initial model and iteratively repairs and refines it using formal verification feedback. Refinement simplifies proof discharge, while repair of models and proofs ensures the soundness of each refinement step. Together, these two components reinforce each other to progressively improve the model quality. Evaluation across systems of varying complexity demonstrates that Event-B Agent substantially outperforms baselines in end-to-end formal model synthesis and repair, while maintaining reasonable efficiency. These results suggest that Event-B Agent is a promising step toward correct-by-construction formal model synthesis and repair.<\/jats:p>","DOI":"10.1145\/3808218","type":"journal-article","created":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T17:06:14Z","timestamp":1782839174000},"page":"4804-4826","source":"Crossref","is-referenced-by-count":0,"title":["Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair"],"prefix":"10.1145","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-0198-148X","authenticated-orcid":false,"given":"Hongshu","family":"Wang","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4411-3054","authenticated-orcid":false,"given":"Xinyue","family":"Zuo","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9132-5349","authenticated-orcid":false,"given":"Yuhan","family":"Sun","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7476-4079","authenticated-orcid":false,"given":"Qin","family":"Li","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4582-9712","authenticated-orcid":false,"given":"Yamine","family":"Ait Ameur","sequence":"additional","affiliation":[{"name":"IRIT - National Polytechnic Institute of Toulouse, Toulouse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6512-8326","authenticated-orcid":false,"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2303.08774"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.06.002"},{"key":"e_1_2_1_5_1","volume-title":"Cursor: The AI Code Editor","author":"Anysphere","year":"2025","unstructured":"Anysphere, Inc. 2025. Cursor: The AI Code Editor. https:\/\/cursor.com\/ Accessed: 2025-09-11."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-019-00264-4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3536430"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSEET66350.2025.00009"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3663529.3663814"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000049"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2501.13712"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3448270"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09580-x"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2404.04662"},{"key":"e_1_2_1_22_1","volume-title":"The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23","author":"Gloeckle Fabian","year":"2023","unstructured":"Fabian Gloeckle, Baptiste Roziere, Amaury Hayat, and Gabriel Synnaeve. 2023. Temperature-scaled large language models for Lean proofstep prediction. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23. https: \/\/openreview.net\/forum?id=sSgdyY0YJR"},{"key":"e_1_2_1_23_1","volume-title":"Group for Software Engineering and Programming Languages","author":"Heinrich Heine University D\u00fcsseldorf","year":"2025","unstructured":"Heinrich Heine University D\u00fcsseldorf, Group for Software Engineering and Programming Languages. 2025. ProB Animator and Model Checker. https:\/\/prob.hhu.de\/ Accessed: 2025-09-11."},{"key":"e_1_2_1_24_1","volume-title":"Group for Software Engineering and Programming Languages","author":"Heinrich Heine University D\u00fcsseldorf","year":"2025","unstructured":"Heinrich Heine University D\u00fcsseldorf, Group for Software Engineering and Programming Languages. 2025. Rodin User's Handbook v.2.8. https:\/\/stups.hhu-hosting.de\/handbook\/rodin\/current\/html\/introduction.html Accessed: 2025-09-11."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2502.15441"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3695988"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747588"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-96-0617-7_2"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2407.10040"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3691620"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-016-0514-4"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2069216.2069252"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2303.04488"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238210"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_32"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2503.02143"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0381-2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2025.103279"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2307.10434"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.52202\/079017-2753"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2310.04870"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2503.05042"},{"key":"e_1_2_1_47_1","first-page":"21573","volume-title":"Levine (Eds.)","volume":"36","author":"Yang Kaiyu","year":"2023","unstructured":"Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems, A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine (Eds.), Vol. 36. Curran Associates, Inc., 21573-21612. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2023\/file\/ 4441469427094f8873d0fecb0c4e1cee-Paper-Datasets_and_Benchmarks.pdf"},{"key":"e_1_2_1_48_1","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 Song Dong. 2025. Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods. In Forty-second International Conference on Machine Learning Position Paper Track. https:\/\/openreview.net\/forum?id=wkisIZbntD"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2509.23675"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T18:30:37Z","timestamp":1782844237000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,30]]},"references-count":49,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3808218"],"URL":"https:\/\/doi.org\/10.1145\/3808218","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,30]]}}}