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, currently under submission.
Presentation#
Citation#
Eric Spencer, ChatTLA+: Using LLMs for TLA+ Formal Specification Generation and Verification, Undergraduate Research and Engagement Symposium, Loyola University Chicago, April 17, 2026.