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