ChatTLA+: Using LLMs for TLA+ Formal Specification Generation and Verification
===============================================================================

:Status: Presented
:Venue: Undergraduate Research and Engagement Symposium, Loyola University Chicago, April 17, 2026
:Authors: Eric Spencer
:Institution: Loyola University Chicago


Abstract
--------

A presentation exploring the use of large language models for generating and verifying
TLA+ formal specifications. The talk examines how LLMs can assist in the synthesis of
formal specifications from natural language, discussing both the promise and the
limitations of current models on rigorous specification tasks.

This work builds on the group's systematic evaluation of LLMs on TLA+ specification
synthesis, extending the discussion to practical generation and verification pipelines.


Based On
--------

This presentation builds on the paper `Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation <../llm-tla-evaluation/>`__, currently under submission.


Presentation
------------

`View the presentation (PDF) <../_static/ChatTLA-presentation-2026.pdf>`__


Citation
--------

Eric Spencer,
*ChatTLA+: Using LLMs for TLA+ Formal Specification Generation and Verification*,
Undergraduate Research and Engagement Symposium, Loyola University Chicago, April 17, 2026.