Skip to main content
Back to top
Ctrl
+
K
GitHub
Pages
About
Team
Funding
Get Involved
Research Papers
All Papers
Can LLMs Write Correct TLA+ Specifications?
ChatTLA+: Using LLMs for TLA+ Formal Specification Generation and Verification
Large Language Models (LLM) and Temporal Logic of Actions (TLA): How Effective are LLMs for Verification Systems
Automating TLA+ Model Synthesis with Large Language Models and Formal Verification Pipelines
TLA+ for All: Running Model Checking in a Python Notebook
Research Updates
All Posts
Our Paper on LLM-Based TLA+ Specification Generation Has Been Accepted
Eric Spencer Presents ChatTLA+ at Loyola University Chicago
Brian Ortiz Presents Poster at Graduate School Interdisciplinary Research Symposium 2026
Can LLMs Write Correct TLA+ Specifications? Our New Evaluation Study
Brian Ortiz Presents Poster at GCASR 2025
Eric Spencer Awarded Mulcahy Scholar Stipend
TLA+ for All: Running Model Checking in a Python Notebook
Index
