AI Insight
TLA-Prover is a 20-billion-parameter language model designed to generate verified TLA+ formal specifications for distributed systems and safety-critical protocols. The model achieves a 30% success rate (pass@1) on both syntactic correctness and semantic verification tests, representing approximately 3.5 times improvement over previous best baselines of 8.6%. Training combines supervised fine-tuning on verified examples with group-relative policy optimization, where the model learns to repair its own rejected specifications using feedback from the TLC model checker.
Why it matters
This advance could accelerate the development and verification of distributed systems and safety-critical software by automating formal specification writing, a traditionally time-consuming expert task. The tiered verification system, particularly the "Diamond" tier that tests for non-trivial correctness properties, helps prevent models from generating specifications that are technically correct but functionally meaningless.
Understand the Science
-cross
Abstract: TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fail the TLC model checker for semantic reasons. Across 25 LLMs, the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check. We present TLA-Prover, a 20-billion-parameter model for TLA+ specification synthesis. Training combines supervised fine-tuning (SFT) on verified examples with repair-based group-relative policy optimization (GRPO). In the GRPO stage, the model learns to fix its own rejected specifications. We also train a direct preference optimization (DPO) variant from the same SFT checkpoint as an ablation. TLC provides the reward signal directly, with no learned reward model. Four tiers grade each output: Bronze (parses), Silver (no warnings), Gold (passes TLC), and Diamond. To reach Diamond, the model’s correctness property is automatically altered in a small way; TLC must then detect a violation. If TLC still passes, the property was always-true and contributes nothing; the output fails Diamond. TLA-Prover reaches 9/30 (i.e. pass@1 = 30%) at both Gold and Diamond on a held-out 30-problem benchmark. This is roughly 3.5x the 8.6% untuned baseline. The DPO variant reaches 20% at Diamond. Gold and Diamond coincide at every checkpoint; this prevents the trivial-property failure mode.
Source: TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation