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
- Archive / PDF:
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 published ICSOFT 2026 paper. The archival record uses the title ChatTLA+ - Can LLMs Write Correct TLA+ Specifications?.
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.