Towards Language Model Guided TLA+ Proof Automation

1. Problem Statement

Formal verification using TLA+ (Temporal Logic of Actions) is critical for ensuring the correctness of complex distributed systems (e.g., used by Amazon, Microsoft, Intel). However, constructing formal proofs in TLA+ is a significant bottleneck due to:

• High Expertise Requirement: It requires deep mathematical insight and familiarity with the TLA+ Proof System (TLAPS).
• Hierarchical Structure: Unlike tactic-based provers (like Lean or Coq) that transform proof states sequentially via commands, TLA+ proofs are hierarchical trees. A complex claim must be broken down into intermediate sub-claims (lemmas) that collectively establish the parent goal.
• LLM Limitations: While Large Language Models (LLMs) have shown success in tactic-based provers by generating sequences of tactics, applying them directly to TLA+ fails because:
  • LLMs struggle with the syntax of TLA+ proofs, frequently generating invalid code.
  • LLMs fail at monolithic generation; generating a full proof in one go leads to errors that propagate, and without incremental verification, the model cannot self-correct.
  • There is a lack of large-scale TLA+ datasets for fine-tuning compared to Lean/Coq.

Goal: To automate the generation of complete, machine-verifiable TLA+ proofs for unproved claims (proof obligations) by leveraging LLMs for reasoning while mitigating their syntactic and structural weaknesses.

2. Methodology: Language Model Guided Proof Automation (LMGPA)

The authors propose LMGPA, a hybrid system that combines the reasoning capabilities of LLMs with the rigorous verification of symbolic provers (TLAPS). The core insight is to constrain LLMs to generate normalized claim decompositions rather than complete proofs.

Key Components:

1. Recursive Decomposition Strategy:

   • Instead of asking an LLM to write a full proof, the system asks it to break a complex goal into a set of simpler sub-claims.
   • The system recursively applies this process: if a sub-claim is still too complex, it is decomposed again until the claims are simple enough for backend provers.

2. Normalized Claim Structure:

   • To address syntax errors, the LLM is prompted to output sub-claims in a strict, normalized format (ASCII-based, specific logical operators like \A, \E, /\, =>).
   • The system parses this normalized output and programmatically converts it into valid TLA+ ASSUME-PROVE blocks. This eliminates the need for the LLM to generate complex TLA+ syntax directly, drastically reducing syntax errors.

3. Symbolic Auto-Proof Generation:

   • For simple claims, the system uses a heuristic symbolic method (without LLMs) to generate "auto proofs" using TLA+ directives like OBVIOUS or BY DEF (unfolding definitions).
   • This handles trivial cases efficiently and reduces the load on the LLM.

4. Verification Feedback Loop:

   • Decomposition Verification: Before recursing, the system uses TLAPS to verify that the set of generated sub-claims logically implies the parent claim. If the implication fails, the feedback is sent back to the LLM to regenerate the decomposition.
   • Recursive Proof: Once a valid decomposition is found, the system recursively attempts to prove each sub-claim. If any sub-claim fails to be proved, the entire attempt for that branch fails, and the system backtracks or retries.

Algorithm Flow:

1. Input: A proof obligation (Context + Goal).
2. Attempt Auto-Proof: Try to prove directly using TLAPS (OBVIOUS/BY DEF). If successful, return.
3. Decompose: If auto-proof fails, prompt the LLM to generate a list of sub-claims in normalized format.
4. Verify Decomposition: Use TLAPS to check if (Sub-claims $\land$ Context) $\Rightarrow$ Goal.
   • If valid, proceed to step 5.
   • If invalid, provide error feedback to LLM and retry (up to a limit).
5. Recurse: For each valid sub-claim, recursively call the proof generator.
6. Construct: Assemble the hierarchical proof tree.

3. Key Contributions

• Novel Approach for Hierarchical Proofs: The paper introduces the first framework specifically designed to automate TLA+ proofs by leveraging LLMs for decomposition rather than tactic generation, respecting the unique tree-structure of TLA+.
• Normalization Technique: A critical contribution is the "normalized claim structure" prompt strategy. By forcing LLMs to output structured data (assumptions and goals) rather than raw code, the system achieves high syntactic validity, solving a major failure mode of direct LLM generation.
• Benchmark Suite: The authors created a new benchmark suite of 119 theorems:
  • 93 mathematical theorems adapted from miniF2F and ProofNet.
  • 26 inductive proofs of distributed protocols (inductive invariants).
  • Note: These were manually translated into TLA+ to ensure correctness, as automated translation from other formalisms proved unreliable.
• System Implementation: A fully functional Python-based system integrating TLAPS, Tree-sitter (for parsing), and various LLM APIs (Claude, Gemini, GPT-5, o3-mini, DeepSeek).

4. Experimental Results

The system was evaluated against three baselines:

1. TLAPS OBVIOUS: Direct symbolic attempt (no LLM).
2. Symbolic Auto Proof Generation (SAPG): Heuristic symbolic generation.
3. Direct LLM Proof Generation (DLPG): Asking LLMs to write full proofs (with feedback).

Key Findings:

• Success Rate: LMGPA consistently outperformed all baselines across all tested models.
  • On Distributed Protocol benchmarks: LMGPA achieved 42.3% – 50.0% success rates (depending on the model), compared to 0% for DLPG and ~38% for SAPG.
  • On Mathematical benchmarks: LMGPA achieved 53.8% – 59.1% success rates, compared to ~29% for the best DLPG and ~49% for SAPG.
• Syntactic Validity: This was the most significant improvement.
  • DLPG had very low syntactic validity (e.g., 0.2% for o3-mini-high, ~20% for Claude).
  • LMGPA achieved high syntactic validity for its decompositions (e.g., 74.8% – 86.8%), proving that the normalization strategy effectively isolates and fixes LLM errors.
• Efficiency: While LMGPA requires more LLM queries than a single-shot attempt, it is significantly more efficient than DLPG because it avoids generating massive, invalid proof trees. It successfully proves theorems that symbolic methods alone cannot.

5. Significance and Future Work

• Lowering the Barrier: This work significantly lowers the barrier to entry for formal verification in TLA+, making it more accessible to engineers who may not be expert theorem provers.
• Paradigm Shift: It demonstrates that for hierarchical proof systems, "divide and conquer" (decomposition) is a more effective LLM application strategy than "sequence generation" (tactics).
• Future Directions:
  • Fine-tuning: The authors suggest fine-tuning LLMs specifically on TLA+ proof corpora to improve decomposition quality and reduce remaining syntax errors.
  • Prover-Aware LLMs: Training models to understand the specific capabilities and timeouts of backend provers (Z3, Zenon, Isabelle) to generate decompositions that are not just mathematically valid but also verifiable within time limits.
  • Benchmark Expansion: Creating larger, leakage-free benchmarks to better evaluate generalization.

In conclusion, the paper presents a robust, hybrid architecture that successfully bridges the gap between the reasoning power of modern LLMs and the rigid verification requirements of the TLA+ ecosystem, achieving state-of-the-art results in automated TLA+ proof generation.