Automating TLA+ Model Synthesis with Large Language Models and Formal Verification Pipelines ============================================================================================ *Work in Progress* :Status: Presented :Venue: GCASR 2025 - 12th Greater Chicago Area Systems Research Workshop, May 8, 2025, Loyola University Chicago :Authors: Brian Ortiz, Mohammed Abuhamad, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer :Institution: Loyola University Chicago :DOI / Poster: `10.6084/m9.figshare.31896151 `__ Abstract -------- This work-in-progress presents a pipeline for automating TLA+ model synthesis using large language models, coupled with formal verification via the SANY parser and TLC model checker. The system takes natural language descriptions of concurrent or distributed systems and attempts to generate syntactically and semantically correct TLA+ specifications, evaluated through automated verification pipelines. Why This Matters ---------------- TLA+ specification writing requires significant expertise, limiting adoption in industry and academia. Automating synthesis with LLMs - while ensuring correctness through formal verification - could make TLA+ accessible to a much broader audience of engineers and researchers. Citation -------- Brian Ortiz, Mohammed Abuhamad, TaiNing Wang, George K. Thiruvathukal, and Konstantin Läufer, *Automating TLA+ Model Synthesis with Large Language Models and Formal Verification Pipelines (WIP)*, GCASR 2025, May 8, 2025. https://doi.org/10.6084/m9.figshare.31896151