Skip to main content
Back to top
Ctrl
+
K
GitHub
Pages
About
Team
Funding
Get Involved
Research Papers
All Papers
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
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
TLA-Prover Paper Accepted to ICSOFT 2026
Our Paper on LLM-Based TLA+ Specification Generation Has Been Accepted
New Paper: TLA-Prover — Fine-Tuning LLMs for Verifiable TLA+ Specification Synthesis
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
