Towards Language Model Guided TLA+ Proof Automation

TL;DR

This paper introduces a prompt-based method leveraging large language models to assist in automating TLA+ proofs by guiding hierarchical decomposition, combined with symbolic verification, and demonstrates superior performance on a new benchmark suite.

Contribution

It presents a novel LLM-guided hierarchical proof decomposition approach for TLA+ and introduces a benchmark suite for evaluating proof automation methods.

Findings

Outperforms baseline methods on the benchmark suite

Effectively reduces syntax errors by constraining LLM outputs

Successfully automates complex TLA+ proofs with high accuracy

Abstract

Formal theorem proving with 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 TLA+ faces significant challenges due to the hierarchical proof structure of the 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.