Towards Language Model Guided $$\text {TLA}^{+}$$ Proof Automation
Yuhao Zhou, Stavros Tripakis · Lecture notes in computer science · 2026
Abstract Formal theorem proving with $$\texttt {TLA}^{+}$$ TLA + provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language models have shown promise in automating proofs for tactic-based theorem provers like Lean, applying these approaches directly to $$\texttt {TLA}^{+}$$ TLA + faces significant challenges due to the hierarchical proof structure of the $$\texttt {TLA}^{+}$$ TLA + proof system. We present a prompt-based approach that leverages LLMs to guide hierarchical decomposition of complex proof obligations into simpler sub-claims, while relying on symbolic provers for verification. Our key insight is to constrain LLMs to generate normalized claim decompositions rather than complete proofs, significantly reducing syntax errors. We also introduce a benchmark suite of 119 theorems adapted from (1) established mathematical collections and (2) inductive proofs of distributed protocols. Our approach consistently outperforms baseline methods across the benchmark suite.