Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation Arslan Bisharat, Brian Ortiz, Eric Spencer, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad
arXiv:2606.05792v1 [cs.AI] 4 Jun 2026
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA {marslan,bortiz4,espencer2,kbhadauria,twang12,gthiruvathukal,klaufer,mabuhamad}@luc.edu
Keywords: Large Language Models, Temporal Logic of Actions, TLA+ , Formal Specification, Verification, Code Generation, Natural Language Processing Abstract: TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertise, which limits adoption. LLMs show promise, but no prior study measures whether they produce semantically correct TLA+ specifications from natural language. This paper presents the first systematic evaluation of LLM-based TLA+ specification synthesis from natural language. Our study evaluates 30 LLMs across eight families on a curated dataset of 205 TLA+ specifications: 25 open-weight models across four prompting strategies (2,600 runs) and 5 proprietary models under few-shot prompting (130 runs), all validated by the SANY parser and TLC model checker. LLMs achieve up to 26.6% syntactic correctness but only 8.6% semantic correctness, with successes exclusive to progressive prompting. Results show that model size does not predict quality, e.g., DeepSeek r1:8b outperforms its 70B variant across all strategies, which suggests the importance of reasoning alignment for formal languages. Code-specialized models consistently underperform due to negative transfer from mainstream language training. We identify five recurring hallucination categories, all traceable to specific training data biases. These results suggest that current LLMs do not generate reliable TLA+ specifications without expert oversight. We release the evaluation framework, code, and dataset to support reproducibility and future research.
1
Introduction
Formal specification is important to build reliable distributed and concurrent systems (Lamport, 2002). Writing correct formal system specifications from natural language remains difficult and time-consuming. Large language models (LLMs) have made progress in code generation, but their ability to produce semantically correct formal specifications from natural language has not been systematically evaluated. This work addresses TLA+ specification (synthesis) from natural language with LLMs. TLA+ is widely adopted in industry, e.g., Amazon Web Services has used it since 2011 to verify DynamoDB, S3, and EBS (Newcombe et al., 2015), and Microsoft Azure applied it to Cosmos DB (Cirstea et al., 2024). TLA+ combines tem-
poral logic, first-order logic, and set theory, which makes it technically difficult for LLMs to generate correct specifications. TLA+ is also a specialized formal language with a public corpus of only a few hundred modules, compared with millions of C, Python, and Java samples in standard LLM pre-training data. This data imbalance makes TLA+ syntax and semantics hard for LLMs to learn and leaves natural-language-to-TLA+ generation under-studied. To address this gap, we curate a benchmark of 205 TLA+ specifications from the TLA+ Foundation (TLA+ Community, 2025), each paired with natural-language comments and TLC configurations, with train, validation, and test splits. We then introduce a reproducible evaluation framework for LLM-based natural-language-to-TLA+ generation. We benchmark 30 models from eight
families, i.e., DeepSeek, LLaMA, Qwen, QwQ, GPT-OSS, code-specialized (e.g., CodeLLaMA and Granite), instruction-tuned (e.g., Mistral, Phi, Gemma, and Starling-LM), and proprietary APIs (e.g., OpenAI GPT and Anthropic Claude) on the curated dataset. The core evaluation uses 25 open-weight models across four prompt strategies (2,600 runs). We also evaluate five proprietary models with few-shot (k = 3) only (130 runs). All outputs from all runs are validated by the SANY parser and TLC checker. Key Findings. (1) LLMs achieve up to 26.6% syntactic correctness on TLA+ (SANY) but only 8.6% semantic correctness (TLC). Semantic success is exclusive to progressive prompts. (2) Model size does not predict quality. The 8Bparameter DeepSeek r1 outperforms its 70B sibling across all strategies. Reasoning-trace finetuning is a stronger predictor of quality than model size. (3) Code-specialized models consistently underperform general-purpose ones due to negative transfer (due to programming language bias) from mainstream programming logic and language training. (4) We identify five recurring hallucination categories: Unicode operator substitution, cross-language syntax injection, reasoning and formatting leakage, generation length miscalibration, and structural errors. These errors map to biases in current open-source training data (i.e., code, formal math, and reasoning samples) and point to two mitigation insights, e.g., obtaining high-quality datasets for specifications and grammar-constrained generation. Contributions. Our contributions are: ❶ We curate a dataset for natural-language-to-TLA+ specification synthesis, consisting of 205 TLA+ specifications paired with natural language comments and TLC configurations. ❷ We provide a systematic evaluation of LLM-based TLA+ specification generation/synthesis from natural language, testing 30 models from eight families across four prompting strategies with syntactic and semantic validation. ❸ We establish quantified baselines for TLA+ synthesis and highlight the gap between current LLM capabilities and reliable specification synthesis. We provide a taxonomy of five systematic hallucination categories in TLA+ generation/synthesis and offer directions for improvement. We release code, dataset, models, and results to support future work.
2
Background & Related Work
TLA+ and Formal Specification. Distributed and concurrent systems are difficult to design and verify. Small errors in the system’s logic can create bugs that appear only under rare timing conditions, so standard tests often cannot find them. Formal verification solves this problem by the application of mathematical reasoning to prove that a system behaves correctly in every possible scenario. TLA+ (Temporal Logic of Actions) (Lamport, 2002) was created to describe concurrent and distributed systems behavior through mathematical formulas that combine temporal logic, first-order logic and set theory. A TLA+ specification has several key components. The initial predicate Init defines all valid start states and the next-state relation Next describes how the system moves from one state to another through atomic actions. The expression Init ∧ [Next ]v defines the core behavior of the system. The symbol represents “always.” System properties are expressed as invariants (safety properties that hold in every reachable state) and liveness properties (behaviors that must eventually occur). The TLA+ toolchain provides two verification methods: the TLC model checker examines every reachable state in a finite version of a specification (Lamport, 2002), while TLAPS allows machine-checked deductive reasoning for infinite-state specifications (Cirstea et al., 2024). Although TLA+ is effective at the detection of design flaws, the creation of correct specifications requires specialized expertise. Engineers must translate informal descriptions with ambiguities and hidden assumptions into precise mathematical expressions that resolve questions about failure modes, concurrency and consistency. Small mistakes such as an incorrect quantifier bound or a missing fairness condition can make a specification compile but fail to capture intended behavior. This expertise barrier limits TLA+ adoption. LLM-based Generation. LLMs trained on large collections of source code can generate code from text. Models such as GPT4, Gemini, Claude and Code Llama can solve standard benchmarks like HumanEval (Austin et al., 2021). But LLMs still make many mistakes: they sometimes create APIs or library functions that do not exist, produce code that does not follow the rules in the specification and struggle with problems that require several steps of reasoning (Ye et al., 2023). The generation of formal specifications is even harder than code
creation. A normal program can be checked by execution, but a formal specification must follow strict mathematical rules. A TLA+ specification may be written correctly with proper operators and syntax but still describe the wrong system behavior by leaving out a fairness rule, defining a condition that is too weak, or leaving important variables undefined. These problems cannot be found by parsers or type checkers and show up only during formal verification or detailed expert review. LLM hallucination, where a model confidently produces incorrect output, has been classified for software tasks into task requirement conflicts, factual knowledge conflicts and project context conflicts (Zhang and Zhang, 2025). Package hallucination creates supply chain risks (Spracklen et al., 2025). For formal languages like TLA+ , hallucinated errors may only surface during verification. GenAI for TLA+ . The TLA+ Foundation launched the GenAI-accelerated TLA+ Challenge in 2025 to investigate generative AI applications for formal methods (TLA+ Foundation, 2025). Specula, the winner, generates TLA+ specifications from code that already exists The system converts (Cheng et al., 2025b). source code into intermediate TLA+ representations, fixes errors through Retrieval-Augmented Generation and iteratively corrects runtime errors identified by TLC. The creation of the Raft specification took about 1.5 hours of manual effort. The second-place entry tested whether LLMs can be guided to produce valid TLA+ syntax through token-level rules such as Greibach Backus-Naur Form and the Guidance framework (Helwer, 2025). This method focuses primarily on the production of syntactically correct specifications while semantic correctness is not addressed. Gregory Terzian studied the opposite approach: the use of completed TLA+ specifications to guide LLMs in the generation of Rust code (Terzian, 2025). SysMoBench (Cheng et al., 2025a) is the first benchmark for LLMs on complex distributed systems in TLA+ , but it compares generated specifications to source code implementations. Our work evaluates generation from natural language only. Previous specification synthesis work focused on invariant discovery from program traces: DistAI infers inductive invariants for distributed protocols (Yao et al., 2021) and SpecGen uses LLMs to generate function-level Java specifications through iterative verification feedback (Ma et al., 2025). Neither generates
Table 1: Summary of data availability across 205 TLA+ specifications in our dataset. Category
Count
Percentage
Both CFG & Comments CFG only Comments only Neither
92 14 95 4
44.9% 6.8% 46.3% 2.0%
Has CFG Has Comments
106 187
51.7% 91.2%
system-level specifications like TLA+ . Gap in Prior Work and Our Contribution. Existing GenAI research on TLA+ focuses on the creation of specifications from code, the enforcement of syntax through token constraints and the use of specifications to guide code generation. No systematic study has tested whether LLMs can produce full and semantically correct TLA+ specifications directly from natural language, what error patterns emerge across model architectures, or how prompting strategies affect generation quality. This work provides the first systematic evaluation of 30 LLMs across four prompting strategies to measure both syntactic and semantic correctness of TLA+ specifications generated from natural language. We use the TLA+ Examples repository, which contains both formal specifications and natural language comments, to test which model architectures and prompting approaches produce correct specifications and what types of errors and hallucinations occur.
3
Methods
Research Questions. This research addresses four questions. RQ1: Can LLMs generate TLA+ specifications that are both syntactically correct and semantically faithful? RQ2: What error types do different LLM backends produce? RQ3: How do quality metrics correlate with model architecture, size, and fine-tuning? RQ4: What failure modes and hallucinations recur in LLM-generated specifications? Formal validation (SANY and TLC) answers RQ1, RQ2, and RQ4. Textual similarity metrics answer RQ3. No public dataset supports systematic evaluation of LLMgenerated TLA+ specifications across these four dimensions. We curate a benchmark of 205 specifications to enable this evaluation. Dataset. We use the TLA+ Examples repository maintained by the TLA+ Foundation (TLA+ Community, 2025), the primary source of community-written formal specifications. The repository contains 205 TLA+ spec-
Table 2: Token usage by model family. R-Tok: reasoning tokens; T-Tok: total tokens; R%: reasoning percentage; Ctx: context window size. Family
Model
R-Tok
T-Tok
R%
Ctx
Proprietary Models GPT
gpt-5 gpt-4o
3.8K 338
24K 19K
15.8 1.8
128K 128K
Claude
sonnet-4-5 haiku-4-5 opus-4-1
338 338 338
28K 17K 31K
1.2 2.0 1.1
200K 200K 200K
DeepSeek
r1:70b r1:32b r1:14b r1:8b r1:7b r1:1.5b coder:6.7b coder:latest
364 338 338 390 364 390 390 286
12K 12K 9.5K 6.7K 25K 1141.7K 754K 289K
3.0 2.8 3.5 5.8 1.4 0.03 0.05 0.1
131K 131K 131K 131K 131K 131K 4K 128K
LLaMA
3.3:70b 3.3:latest 3.1:8b 3:latest 3.2:1b
338 338 416 338 390
20K 20K 17K 16K 771K
1.7 1.7 2.4 2.1 0.05
128K 128K 128K 8K 131K
Qwen
3:235b 3:30b 3:4b
520 520 390
18K 17K 4.1K
2.9 3.1 9.6
32K 32K
QwQ Phi Granite GPT-OSS
latest 4-mini:latest 3.3:latest 20b 120b latest latest 2b latest
390 416 390 520 390 416 390 520 364
110K 1.3K 42K 20K 19K 56K 61K 29K 38K
0.4 31.7 0.9 2.6 2.1 0.8 0.6 1.8 1.0
32K 128K 131K 128K 128K 16K 32K 8K 8K
Open-Weight Models
CodeLLaMA Mistral Gemma Starling-LM
ifications across 98 projects: distributed consensus protocols (Paxos, Raft, Byzantine agreement), concurrency problems (dining philosophers, readers-writers), and algorithmic puzzles (Towers of Hanoi, N-queens). Each specification includes a .tla file, extracted natural language comments used as LLM input, and an optional TLC configuration file. We split the dataset into training (143 specifications, 70%), validation (31 specifications, 15%), and test (31 specifications, 15%) sets stratified by project. The training set provides few-shot examples. The validation set is used for model hyperparameters and prompt tuning. The test set originally contains 31 specifications. Five were excluded because they lacked either natural language comments or a TLC configuration file, both required for evaluation. This yields 26 usable test specifications. Table 1 shows the distribution across splits. LLM Models. We test 30 LLMs from eight model families (Table 2). The core evaluation uses 25 open-weight models across all four strategies via the Ollama runtime (Contributors, 2024): ❶ DeepSeek (R1 series: 1.5B–70B; Coder) (Guo et al., 2025); ❷ LLaMA (3.x: 1B–70B) (Grattafiori et al., 2024); ❸ Codespecialized (CodeLLaMA, DeepSeek-Coder,
Granite); ❹ Reasoning-focused (QwQ, Qwen3 (Yang et al., 2025)); ❺ Instructiontuned (Mistral (Jiang et al., 2023), StarlingLM, Phi-4 (Abouelenin et al., 2025), Gemma 2b (Team et al., 2024)). We also test five proprietary models with few-shot (k = 3) prompting: GPT-5 (Singh et al., 2025), GPT-4o (OpenAI et al., 2024), Claude Opus 4.1 (Anthropic, 2023), Sonnet 4.5 (Anthropic, 2025), and Haiku 4.5. We focus the multi-strategy analysis on open-weight models for two reasons. First, open-weight models support full reproducibility. Second, formal specifications often describe sensitive system designs better suited to local generation. Prompting Strategies. We test four prompting strategies adapted from common LLM codegeneration settings for TLA+ specification generation/synthesis. Each approach tests different LLM capabilities. 1 Few-Shot Prompting: This strategy tests few-shot in-context learning with k = 3 examples from the training set. Each example pairs natural language comments with the corresponding complete TLA+ specification. The prompt consists of a system instruction, the few-shot examples, and the target comments. The LLM generates the full specification in one step. 2 Progressive Prompting: This strategy also uses k = 3 few-shot examples but adds instructional messages that guide the model through the specification structure. Each message focuses on a different aspect: module declaration, state variables, operators, and temporal properties. This structure prepares the model before it receives the target comments. 3 Fill-in-Middle: This code completion strategy splits the ground-truth specification into three parts: prefix (first 30%), middle (40%), and suffix (last 30%). The prompt provides the prefix and suffix with a <FILL> marker. The LLM generates the missing middle portion. No few-shot examples are used. The surrounding context provides sufficient syntactic and semantic information for the model. 4 Half Completion: This strategy provides the first 50% of the specification as a prefix along with comments and configuration. The LLM generates the remaining 50%. No few-shot examples are used. The prefix provides sufficient syntactic and semantic context for the model. Evaluation Metrics. We use two metric groups with different roles. Formal validation measures correctness of the generated specification as an
Table 3: Cross-method comparison of SANY, TLC and textual similarity results across four prompting strategies (25 open-weight models × 26 specifications = 650 runs per strategy). Only Progressive achieves TLC passes (8.6%). Per-model breakdowns appear in Table 5; per-specification breakdowns in Table 10. † TLC pass rates of 0% reflect failures (i.e., State Directory Conflicts and Module Not Found errors). FS
HC
Prog.
FIM
162 / 650 24.9 qwen3:235b (80.8) 0 / 26
92 / 650 14.2 qwq (38.5) 9 / 26
56 / 650 8.6 r1:8b (53.8) 1 / 26
0 / 650 0.0 N/A 26 / 26
N/A N/A N/A N/A
0.077±0.13 0.213±0.20 12.27±13.9 1 / 650
Syntax Validation (SANY) Passed / Total Pass Rate (%) Best Model (%) Specs at 0%
173 / 650 26.6 qwen3:30b (92.3) 0 / 26
Passed / Total Pass Rate (%) Best Model (%) Specs at 0%
0 / 650 0.0 N/A 26 / 26
80 / 650 12.2 qwq (34.6) 6 / 26
Model Checking (TLC) 0 / 650 0.0 N/A 26 / 26
Similarity to Ground Truth Avg BLEU Avg ROUGE-L Avg Line Accuracy (%) Exact Matches
N/A N/A N/A N/A
0.062±0.11 0.189±0.19 10.90±11.8 0 / 650
FS: Few Shot, HC: Half Completion, Prog.: Progressive, FIM: Fill-in-Middle
executable formal artifact. Textual similarity measures closeness to the reference sequence. Formal Validation: Each specification passes through two stages. ❶ SANY checks syntax with a 30-second timeout and passes if it reports “Parsing completed.” ❷ Specifications that pass SANY are submitted to TLC with their configuration file for model checking. Textual Similarity: For completion strategies (HC and FIM), a well-defined target region exists for direct comparison. We compute BLEU (Papineni et al., 2002), ROUGEL (Lin, 2004), edit distance, exact match, and line accuracy against the ground-truth segment.
4
Results
Table 3 summarizes results across all four prompting strategies. The headline finding is a persistent syntax–semantics gap: i.e., even the best strategy reaches only 26.6% SANY syntax validity. Only Progressive prompting produces any model-checking successes (8.6%). Within those successes, a single 8B reasoning model accounts for a quarter of all passing runs and outperforms every larger model tested.
4.1
RQ1: Synthesis Correctness
Syntax Validation: FS achieves the highest SANY pass rate at 26.6% (173/650) followed by Prog. at 24.9% (162/650). The two completion strategies lag behind: FIM passes 14.2% (92/650)
and HC passes 12.2% (80/650). Model Checking: The clearest result is the near-total failure of semantic validation. Three of the four strategies (FS, HC, and FIM) achieve 0% TLC pass rates across all 650 runs each. Prog. is the only exception with 56 of 650 runs (8.6%) passing TLC model checking (Table 4 details two categories of TLC failure: infrastructure failures, i.e., environment-level issues such as unresolved EXTENDS module paths that prevent TLC from loading the specification, and genuine semantic failures caused by invalid model-checking configuration in the LLM output). The 56 passes are concentrated in just three model families. DeepSeek r1:8b is the strongest performer with 14 out of 26 TLC passes (53.8%) under Prog., a result that accounts for 25% of all successful runs. Qwen3:235b and Qwen3:30b follow with 12 and 10 TLC passes, respectively, together contributing another 39% of all Prog. successes. GPT-OSS-20b achieves 6 and Phi-4-mini 4 TLC passes; every other model achieves 3 or fewer. The Qwen family’s TLC success under Prog. contrasts sharply with its 0 TLC passes under FS despite its highest FS syntax rates. We examine this pattern in RQ3. Best Models per Strategy: Table 5 shows two contrasting performance profiles. For full-generation strategies (FS and Prog.), large general-purpose models dominate: Qwen3:30b (23/26) and Qwen3:235b (22/26) lead FS SANY, while Qwen3:235b (21/26) and both LLaMA 3.3 variants (18/26) lead Prog. SANY. For completion strategies, the picture inverts: QwQ achieves only 3/26 on FS yet leads both HC (9/26) and FIM (10/26). Chain-of-thought reasoning appears to help context-sensitive completion, but hurts open-ended generation. Proprietary Models (FS k = 3 Only): In a companion experiment, we test five proprietary models with FS (k = 3) as the sole strategy. The detailed results are shown in Table 6. Among these, GPT-5 is the strongest overall: it passes SANY on all 26 specifications (100%) and achieves 7/26 TLC passes (26.9%), the highest TLC rate for any model under FS. Claude Sonnet 4.5 and Haiku 4.5 pass SANY at 92% (24/26) and 81% (21/26) respectively and each achieves 3/26 TLC passes (11.5%). Claude Opus 4.1 passes 23/26 SANY (88.5%) with 1 TLC pass. GPT-4o passes 20/26 SANY (77%) with 1 TLC pass. These proprietary models were not included in the multi-strategy analysis due to reproducibility constraints and because formal specifications often describe sensitive system designs. Even the
Table 4: TLC model checking infrastructure failure analysis across prompting strategies. Progressive shows 122 TLC failures plus 455 parsing errors (577 total failures, 56 passes, 8.6% pass rate). FS, HC and FIM each had 650 TLC failures (0% pass rate). The table decomposes TLC failures into infrastructure artifacts (Module Not Found) and genuine semantic failures (Config File Exception: 18 FS, 5 HC, 110 Prog., 5 FIM). Category
Type
Module Not Found Config File Exception
Infra. Genuine
FS
HC
Prog.
FIM
159 (24.5%) 18 (2.8%)
159 (24.5%) 5 (0.8%)
12 (9.8%) 110 (90.2%)
156 (24.0%) 5 (0.8%)
650 97.2%
650 99.2%
122 9.8%
650 99.2%
Total Infrastructure %
Table 5: Per-model SANY (S) and TLC (T) pass counts across all four prompting strategies (25 openweight models, 26 specifications each). Detailed permodel per-specification breakdowns are provided in supplementary materials. HC
Prog.
Model
S
FS T
S
T
S
T
S
T
r1:70b r1:32b r1:14b r1:8b r1:7b r1:1.5b coder:6.7b coder:latest
0 6 1 22 1 1 1 0
0 0 0 0 0 0 0 0
3 2 2 1 4 2 1 5
0 0 0 0 0 0 0 0
3 8 2 15 6 8 0 3
0 1 1 14 1 3 0 1
3 6 2 3 3 2 2 5
0 0 0 0 0 0 0 0
LLaMA
3.3:70b 3.3:latest 3.1:8b 3:latest 3.2:1b
11 11 6 3 2
0 0 0 0 0
2 1 3 3 2
0 0 0 0 0
18 18 3 2 12
0 0 0 0 0
6 5 4 5 4
0 0 0 0 0
Qwen
3:235b 3:30b 3:4b
22 23 5
0 0 0
3 3 3
0 0 0
21 11 1
12 10 1
5 5 2
0 0 0
QwQ
latest
3
0
9
0
2
0
10
0
Phi
4mini:latest
5
0
4
0
4
4
1
0
Granite
3.3:latest
3
0
5
0
2
0
2
0
GPT-OSS
120b 20b
17 18
0 0
4 3
0 0
6 9
1 6
3 5
0 0
CodeLLaMA
latest
3
0
5
0
2
0
3
0
Mistral
latest
3
0
2
0
3
0
3
0
Gemma
2b
6
0
4
0
2
1
2
0
Starling-LM
latest
0
0
2
0
1
0
1
0
3.71
0.00
Family
DeepSeek
Average
6.920.00
3.170.00
FIM
6.382.08
FS: Few Shot, HC: Half Completion, Prog.: Progressive, FIM: Fill-in-Middle
Table 6: SANY and TLC performance for five proprietary LLMs under Full-Generation (FS) prompting. GPT-5 achieves the highest TLC rate at 26.9%, confirming that the syntax–semantics gap persists even at frontier model scale. Model GPT-5 Claude Sonnet 4.5 Claude Haiku 4.5 Claude Opus 4.1 GPT-4o
SANY
TLC
Pass
%
Pass
%
26/26 24/26 21/26 23/26 20/26
100.0 92.3 80.8 88.5 76.9
7/26 3/26 3/26 1/26 1/26
26.9 11.5 11.5 3.8 3.8
best frontier model (GPT-5) achieves 26.9% TLC success under FS, comparable to the open-weight FS ceiling. Syntax–semantics gap persists at frontier scale under the same prompting conditions. Textual Similarity: For the completion strate-
Description Unresolved EXTENDS module paths Invalid .cfg for TLC
gies where ground-truth comparison is possible, similarity to the reference is low as shown in Tables 9 and 7. HC achieves a mean BLEU of 0.062 (±0.11) and ROUGE-L of 0.189 (±0.19) while FIM scores slightly higher with BLEU of 0.077 (±0.13) and ROUGE-L of 0.213 (±0.20). Line accuracy averages 10.90% for HC and 12.27% for FIM; exact matches are nearly absent (0/650 for HC, 1/650 for FIM). These low scores follow directly from the length miscalibration documented in RQ4: models that generate 3–9x the expected output length will diverge from ground-truth ngram patterns regardless of semantic quality. RQ1 Summary LLMs produce syntactically valid TLA+ in up to 26.6% of attempts, but semantic correctness is rare (8.6% TLC under Prog.). Only Prog. achieves any TLC passes, led by DeepSeek r1:8b (14/26) and Qwen3 models (10–12 TLC each). Completion strategies show low textual similarity (BLEU < 0.08 and ROUGE-L < 0.22).
4.2
RQ2: Synthesis Errors
Dominant Error Categories: Table 8 (PanelA) shows the distribution of SANY errors across the four strategies. The most common error category is Parse: Bad Module Body, which accounts for roughly half of all failures across every strategy (47.8% FS, 46.3% HC, 49.8% Prog., 52.0% FIM). This error arises when the parser encounters invalid syntax within the module body: malformed operator definitions, structurally broken expressions, or injected non-TLA+ syntax. This pattern remains constant across strategies, which indicates a core limitation in LLM understanding of TLA+ grammar rather than prompt design. Strategy-Specific Error Patterns: The second most common error type differs by strategy class. FS and Prog. produce relatively more Unexpected Token errors (17.2% and 13.3%), which arise when the parser encounters a token that violates the expected grammar. In contrast, HC and FIM produce more Parse: Other errors (39.8%
and 34.2%), which capture miscellaneous parse failures such as mismatched delimiters and incomplete expressions. Full-generation models must construct correct operator syntax from scratch and tend to fail with specific illegal tokens. Completion models receive valid syntactic context and fail with structural mismatches deeper in the file. Lexical Errors: Lexical errors account for less than 10% of SANY-detected failures but reveal systematic cross-language contamination. Unicode operator substitution (replacing TLA+ ASCII operators with LATEX/math equivalents) appears in 7.1% of FS and 8.8% of Prog. failures. Backtick errors from Markdown code-fence leakage appear in 5.9% of FS failures. Semicolons, absent from TLA+ but ubiquitous in C, Java, and Python, appear as SANY first errors in 3.8% of FS and 5.1% of Prog. failures. A broader file scan reveals higher ambient contamination rates of 7.5% for FS and 12.6% for Prog. These lexical hallucinations are discussed in full under RQ4. Error Location: Panel B of Table 8 shows where the first error occurs in the generated file, divided into early (first third), middle, and late (final third) segments. FS and Prog. exhibit earlyheavy error distributions: 50.3% and 45.1% of errors occur in the first third of the file. HC and FIM show the opposite pattern: errors concentrate in the middle and late portions (88.9% and 85.5% combined). Full-generation strategies must produce a valid TLA+ module header from scratch and fail immediately when the preamble is wrong. Completion strategies receive a correct prefix and only diverge further into the body. RQ2 Summary “Parse: Bad Module Body” accounts for roughly half of all failures across every strategy and points to a structural failure mode that future datasets should target. Full-generation strategies fail early with specific illegal tokens; completion strategies fail mid-to-late with structural mismatches. Lexical contamination from non-TLA+ languages (Unicode operators, backticks, semicolons) is systematic and strategyindependent. Grammar-constrained generation and deterministic post-processing offer concrete paths for future improvement.
4.3
RQ3: Model Impact
Model Family Analysis: The per-model results in Table 5 reveal that model family predicts which strategy a model excels at more than it predicts
Table 7: Per-model textual similarity metrics for Fillin-the-Middle (FIM) prompting (mean± SD across 26 specifications). Includes BLEU, ROUGE, edit distance, exact match and line accuracy. Family
Model
E
Acc (%)
Similarity
BLEU
ROUGE-L
r1:70b r1:32b r1:14b r1:8b r1:7b r1:1.5b coder:6.7b coder:latest
1 0 0 0 0 0 0 0
18.59±21.2 19.02±20.0 12.19±14.2 6.04±10.0 8.06±9.4 7.89±11.0 13.33±17.5 9.55±12.8
0.151±0.19 0.195±0.18 0.152±0.18 0.028±0.05 0.128±0.12 0.064±0.09 0.076±0.11 0.075±0.09
0.159±0.21 0.145±0.17 0.076±0.13 0.017±0.03 0.053±0.08 0.027±0.05 0.044±0.07 0.023±0.04
0.348±0.22 0.371±0.19 0.270±0.20 0.048±0.07 0.217±0.12 0.131±0.16 0.209±0.19 0.171±0.15
LLaMA
3.3:70b 3.3:latest 3.1:8b 3:latest 3.2:1b
0 0 0 0 0
22.39±17.1 21.70±18.4 9.55±11.9 10.68±11.3 3.82±6.0
0.194±0.16 0.185±0.17 0.132±0.13 0.142±0.14 0.075±0.09
0.204±0.19 0.195±0.19 0.121±0.15 0.091±0.13 0.026±0.05
0.377±0.17 0.367±0.18 0.278±0.16 0.285±0.15 0.135±0.14
Qwen
3:235b 3:30b 3:4b
0 0 0
9.62±13.1 5.37±6.8 8.27±11.7
0.054±0.09 0.033±0.06 0.149±0.16
0.054±0.08 0.013±0.02 0.021±0.04
0.087±0.14 0.049±0.08 0.191±0.16
QwQ
latest
0
14.66±19.5
0.030±0.05
0.020±0.04
0.070±0.08
Phi
4mini:latest
0
2.20±6.4
0.023±0.05
0.001±0.00
0.025±0.07
Granite
3.3:latest
0
14.45±13.5
0.130±0.13
0.103±0.14
0.285±0.17
GPT-OSS
120b 20b
0 0
24.16±21.0 8.46±12.7
0.240±0.24 0.065±0.10
0.212±0.25 0.033±0.06
0.392±0.25 0.089±0.15
CodeLLaMA
latest
0
16.84±17.5
0.052±0.09
0.063±0.12
0.191±0.19
Mistral
latest
0
16.41±16.3
0.109±0.11
0.113±0.14
0.285±0.17
Gemma
2b
0
10.09±10.6
0.090±0.10
0.038±0.07
0.219±0.14
Starling-LM
latest
0
15.88±15.8
0.093±0.10
0.062±0.09
0.242±0.16
0.04
12.37±13.83
0.107±0.119
0.077±0.102
0.213±0.154
DeepSeek
Average
Table 8: SANY error taxonomy across four prompting strategies. Panel A: distribution of error types among failed runs. Panel B: location of the first error in the generated file. Panel A: Error Type Distribution Error Type
Method
n
%
Parse: Bad Module Body
FS HC Prog. FIM
228 264 243 290
47.8 46.3 49.8 52.0
Parse: Other
FS HC Prog. FIM
72 227 70 191
15.1 39.8 14.3 34.2
Parse: Unexpected Token
FS HC Prog. FIM
82 29 65 17
17.2 5.1 13.3 3.0
Panel B: First Error Location Location
Method
n
%
Early (first third)
FS HC Prog. FIM
240 63 220 81
50.3 11.1 45.1 14.5
Mid (middle third)
FS HC Prog. FIM
196 261 209 310
41.1 45.8 42.8 55.6
Late (final third)
FS HC Prog. FIM
41 246 59 167
8.6 43.2 12.1 29.9
overall quality. The Qwen3 family dominates syntax generation under full-generation strategies but achieves no TLC passes under FS despite leading the SANY rankings. High syntactic fluency does not translate to semantic cor-
Table 9: Per-model textual similarity metrics for Half-Completion (HC) prompting (mean± SD across 26 specifications). Includes BLEU, ROUGE, edit distance, exact match and line accuracy. Family
Model
E
Acc (%)
Similarity
BLEU
ROUGE-L
r1:70b r1:32b r1:14b r1:8b r1:7b r1:1.5b coder:6.7b coder:latest
0 0 0 0 0 0 0 0
14.69±11.6 15.43±13.2 11.67±8.7 4.42±6.1 12.62±11.3 6.05±8.0 10.48±14.2 10.80±11.7
0.154±0.21 0.175±0.17 0.083±0.06 0.008±0.02 0.081±0.08 0.037±0.05 0.062±0.10 0.044±0.04
0.107±0.17 0.120±0.16 0.050±0.07 0.002±0.01 0.056±0.07 0.020±0.04 0.032±0.06 0.014±0.03
0.278±0.21 0.319±0.19 0.227±0.14 0.030±0.08 0.215±0.14 0.086±0.13 0.163±0.15 0.109±0.10
LLaMA
3.3:70b 3.3:latest 3.1:8b 3:latest 3.2:1b
0 0 0 0 0
17.67±13.9 17.51±13.5 9.05±10.7 12.07±9.9 6.72±8.7
0.181±0.17 0.166±0.17 0.106±0.11 0.115±0.12 0.053±0.07
0.158±0.18 0.161±0.18 0.083±0.11 0.064±0.09 0.043±0.08
0.366±0.20 0.361±0.20 0.232±0.16 0.265±0.16 0.140±0.14
Qwen
3:235b 3:30b 3:4b
0 0 0
5.18±10.3 3.58±4.8 8.24±9.2
0.061±0.14 0.041±0.15 0.127±0.15
0.014±0.05 0.023±0.08 0.067±0.15
0.093±0.19 0.058±0.21 0.217±0.21
QwQ
latest
0
6.06±9.2
0.037±0.05
0.018±0.02
0.066±0.04
Phi
4mini:latest
0
1.54±4.2
0.015±0.03
0.003±0.01
0.034±0.06
Granite
3.3:latest
0
15.30±12.6
0.071±0.07
0.055±0.10
0.192±0.15
GPT-OSS
120b 20b
0 0
18.39±14.1 11.12±12.9
0.195±0.17 0.098±0.13
0.151±0.18 0.052±0.10
0.362±0.22 0.197±0.22
CodeLLaMA
latest
0
8.84±11.2
0.057±0.11
0.038±0.09
0.121±0.16
Mistral
latest
0
14.15±12.3
0.068±0.06
0.084±0.11
0.213±0.17
Gemma
2b
0
15.23±11.5
0.073±0.06
0.067±0.09
0.194±0.11
Starling-LM
latest
0
15.73±12.3
0.083±0.09
0.070±0.12
0.188±0.13
Total
–
0
10.90±10.6
0.088±0.10
0.062±0.09
0.189±0.15
DeepSeek
rectness without the structured guidance of Prog. The DeepSeek R1 series presents the most striking result: the 8B parameter model achieves the best TLC result in the entire study (14/26 under Prog.) while the 70B variant fails to produce a single SANY pass under FS. This inversion of scale is not noise: it appears consistently across metrics and strategies (see Model Size below). The R1 training regime produces reasoning capabilities that transfer differently at different scales. The LLaMA 3.3 family performs reliably under Prog. for syntax (18/26 for both 70b and latest) but, like Qwen, achieves no TLC passes. Model Size: Larger models do not consistently outperform smaller ones, a finding that holds within three independent model families. Within DeepSeek R1, the 8B model achieves 14 TLC passes under Prog. while the 70B model achieves none. The 8B model also leads on SANY under FS (22/26 vs. 0/26). Within Qwen3, the 30B variant leads FS SANY (23/26) over the 235B model (22/26). Within LLaMA, the 1B model (3.2:1b) achieves the highest Prog. SANY of any LLaMA variant (12/26), ahead of LLaMA 3.1:8b (3/26) and LLaMA 3:latest (2/26). For TLA+ , a scarce-corpora formal language, reasoning alignment and instruction-following discipline matter more than raw parameter count. Code Specialization: Models designed or finetuned for code generation do not outperform general-purpose models on TLA+ . CodeL-
LaMA achieves 0–5 SANY passes per strategy, DeepSeek-Coder peaks at 5/26 (HC and FIM), and Granite reaches only 5/26 (HC). Generalpurpose models like Qwen3:30b (23/26 FS) and LLaMA 3.3:70b (18/26 Prog.) far exceed these code specialists. Models heavily fine-tuned on Python, C, and Java learn strong priors about those languages’ syntax that interfere with the stricter and more distinctive grammar of TLA+ . Per-Specification Difficulty: Table 10 shows that specification difficulty varies from 0% to 100% SANY pass rates and that the difficulty profile is strategy-specific. Simple statemachine specifications (e.g., YoYoNoPruning) achieve 100% SANY under both completion strategies, while complex distributed protocols (e.g., HDiskSynod, BinarySearch) score 0%. Under Prog. with TLC, MultiPaxos and VoucherCancel achieve the highest semantic pass rates (16% each). MCDieHarder achieves 0% TLC across every strategy. RQ3 Summary Standard assumptions about scale and specialization do not hold for TLA+ . Smaller reasoning models (DeepSeek r1:8b, LLaMA 3.2:1b) outperform larger siblings. Code-specialist models consistently underperform general-purpose ones due to negative transfer from mainstream language training. Model family determines strategy fit better than overall capability.
4.4
RQ4: Failure Modes
Beyond the error type distribution in RQ2, we identify five categories of hallucination that recur across models and strategies (Table 11). Unicode Operator Substitution: LLMs frequently replace the ASCII operators that TLA+ requires with their Unicode or LATEX equivalents. Common substitutions include ∨ (U+2228) for \/, ∧ (U+2227) for /\, ∈ (U+2208) for \in, and → (U+2192) for ->. These substitutions appear across all four strategies and all model families. SANY rejects all Unicode operators, which makes this a consistent source of lexical errors. Cross-Language Syntax Injection: Models inject syntax from mainstream languages into TLA+ output. Semicolons are the most common example: Prog. shows the highest contamination rate at 12.6% of files (82/650) followed by FS at 7.5% (49/650), while HC and FIM are lower at approximately 3.5% each. QwQ is the worst offender with 35% semicolon contamination in FS
Table 10: Specification-level SANY and TLC pass rates averaged across 25 open-weight models for each of the 26 test specifications. Per-specification similarity metrics and detailed breakdowns are provided in supplementary materials. Prog.
FIM
Specification
S
FS T
S
HC T
S
T
S
T
Alternate BinarySearch BufferedRandom AccessFile ClientCentric Consensus Environment Controller EWD687a_anim EWD998ChanID _export Hanoi HDiskSynod KVsnap Majority MajorityProof MCConsensus MCDieHarder MCEWD687a MultiPaxos MultiPaxos_MC nbacc_ray97 Relation SimpleRegular TLAPS TwoPhase VoucherCancel VoucherTransfer YoYoNoPruning
44.0 12.0
0.0 0.0
4.0 0.0
0.0 0.0
28.0 24.0
4.0 8.0
0.0 0.0
0.0 0.0
16.0 24.0 44.0
0.0 0.0 0.0
0.0 16.0 4.0
0.0 0.0 0.0
28.0 12.0 36.0
12.0 8.0 12.0
0.0 0.0 8.0
0.0 0.0 0.0
24.0 36.0
0.0 0.0
4.0 0.0
0.0 0.0
24.0 28.0
16.0 12.0
4.0 4.0
0.0 0.0
20.0 4.0 32.0 28.0 20.0 32.0 36.0 28.0 24.0 24.0 36.0 32.0 28.0 24.0 20.0 24.0 24.0 32.0 24.0
0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0
0.0 20.0 0.0 16.0 8.0 32.0 4.0 4.0 24.0 8.0 36.0 0.0 4.0 8.0 12.0 8.0 4.0 4.0 100.0
0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0
16.0 16.0 20.0 24.0 16.0 28.0 40.0 16.0 32.0 32.0 36.0 20.0 20.0 32.0 24.0 20.0 28.0 24.0 24.0
8.0 12.0 4.0 12.0 4.0 4.0 8.0 0.0 4.0 16.0 4.0 12.0 4.0 12.0 4.0 8.0 16.0 4.0 16.0
0.0 4.0 48.0 0.0 8.0 12.0 8.0 24.0 36.0 0.0 8.0 36.0 8.0 44.0 4.0 12.0 0.0 0.0 100.0
0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0
Average
26.6
0.0
12.2
0.0
24.9
8.6
14.2
0.0
and 27% in Prog. Granite and Mistral each reach 31% in Prog. Backtick injection from Markdown code fences is most common in FS (28 files), with DeepSeek r1:7b particularly prone (12 out of 26 files). Prog. also shows isolated instances of END keyword injection from Pascal/SQL syntax. Reasoning and Formatting Leakage: Models with chain-of-thought capabilities leak their internal reasoning into the generated specification. QwQ is the worst offender: it injects <think> blocks into 100% of its HC and FIM outputs (26/26 files each) and 46.2% of FS outputs DeepSeek R1 models (r1:14b and r1:32b) and Qwen3:235b show lower contamination rates (3.8–7.7%). The overall contamination rates are 2.3% for FS, 4.6% for HC, and 4.3% for FIM. Prog. is not affected because its multi-step pipeline structure handles reasoning differently. Beyond thinking blocks, Prog. outputs occasionally contain Markdown fences and natural language prose within the TLA+ module body.
Table 11: Hallucination taxonomy across prompting strategies (RQ4). Integer values = file counts; X = observed but count not isolated; 0 = not † observed; n/a = not applicable. FIM applies clean_llm_response() to strip markdown before validation. ‡ File scan (contains ≥1 semicolon). § SANY first-error count (FS: 18/477; HC: 11/570; Prog. : 25/488; FIM: 10/558). ¶ File scan shows higher rates (FS: 49/650 = 7.5%; HC: 23/650 = 3.5%; Prog. : 82/650 = 12.6%; FIM: 22/650 = 3.4%). Pattern
Source
Correct TLA+
FS
HC
Prog
FIM
\/ /\ \in ->
X X X X
X X X X
X X X X
X X X X
invalid invalid ====
18§ /49¶ 28 0
11§ /23¶ 10 0
25§ /82¶ 21 X
10§ /22¶ 13 0
CoT reasoning Output format Task confusion
invalid invalid invalid
15 0 0
30 0 0
n/a X X
28 0† 0
Missing ==== Missing MODULE
Incomplete gen No preamble
X 0
X 0
243+ X
X 0
Duplicate MODULE
Repeated start
==== - MODULE X single header
0
0
X
0
Unicode Operator Substitution (Lexical Error) ∨ (U+2228) ∧ (U+2227) ∈ (U+2208) → (U+2192)
LATEX/Math LATEX/Math LATEX/Math LATEX/Math
Cross-Language Syntax Injection Semicolons (;) Backticks (‘) END keyword
C/Java/Py Markdown Pascal/SQL
Reasoning/Formatting Leakage <think> blocks Markdown fences NL prose in body Structural Errors
RQ4 Summary Five systematic hallucination categories recur across all models: (1) Unicode operator substitution; (2) cross-language syntax injection (semicolons in 12.6% of files, backticks in 5.9%); (3) reasoning token leakage (<think> blocks in QwQ); (4) generation length miscalibration (0.00–9.84× ground truth); and (5) structural errors (243+ missing ==== terminators). Each category is traceable to a specific training data bias and addressable by better datasets, grammar-specific decoding/post-processing. Generation Length Miscalibration: Models exhibit poor calibration between output length and the expected ground-truth length On average, HC outputs are 3.46× the length of the ground-truth target segment and FIM outputs are 2.24×. The extremes are stark: DeepSeek coder:latest generates 9.15× the expected HC length, LLaMA 3.2:1b generates 9.84×, and QwQ generates 7.71× for HC and 7.75× for FIM. At the opposite extreme, Qwen3:30b produces near-empty output for HC (0.00×) and Qwen3:235b produces only 0.09× the expected length. Only a few models achieve nearperfect calibration: LLaMA 3.3:70b (1.16× HC and 1.03× FIM) and DeepSeek r1:7b (0.97× HC). Structural Errors: Prog. produces distinctive structural hallucinations due to its multistep generation process. The most common is the missing ==== terminator: over 243 Prog.-
generated files lack the four-equals-sign module terminator that TLA+ requires. Models also occasionally produce duplicate MODULE headers or omit the MODULE header entirely when the focus is on body content from a particular step. These structural errors are largely absent from the other strategies where generation occurs in one pass.
5
Discussion
This section discusses the results and practical implications for TLA+ LLM-based synthesis. The Syntax-Semantics Gap Is Structural, Not Incidental: The wide gap between syntactic validity (up to 26.6% SANY) and semantic correctness (8.6% TLC) persists across all four strategies and all model scales. It reflects a structural property: LLMs acquire surface-level token patterns of TLA+ syntax without internalizing the modal and set-theoretic semantics those tokens encode. A TLA+ module that parses is only a skeleton. Hahn et al. show that LLM performance degrades as target formalism complexity increases from regular expressions through firstorder logic to LTL (Hahn et al., 2022); TLA+ , combining TLA with set theory, sits at the harder end of that spectrum. Ferrari and Spoletini frame LLMs and formal methods as mutually reinforcing: LLMs accelerate specification drafting while formal tools provide correctness guarantees (Ferrari and Spoletini, 2025). Our results illustrate why both directions are needed. The Qwen3 family makes the gap most concrete: Qwen3:30b achieves the highest FS SANY rate (23/26) yet produces zero TLC passes under the same strategy. The results establish that closing the syntax-semantics gap is the primary challenge for future TLA+ work. Fine-tuning on the 205 TLA+ Foundation specifications could improve semantic understanding, and iterative refinement with TLC feedback could help toward valid synthesis. Progressive Prompting as Cognitive Scaffolding: Progressive prompting is the only strategy that achieves TLC passes (8.6%) and its SANY rate (24.9%) is competitive with FS (26.6%), making it the dominant choice overall. Its advantage lies in decomposing the generation task into sequential concerns: module structure, variable declarations, initial predicate, next-state relation, temporal property. This matches the insight behind chain-of-thought prompting, where externalis-
ing intermediate reasoning steps improves performance on tasks requiring multi-hop inference (Wei et al., 2022). Correct TLA+ synthesis must simultaneously satisfy module syntax, type consistency, behavioral semantics and temporal logic. Kogler et al. independently found that iterative LLM prompting with post-processing achieves syntactic validity in formal railway specifications (Kogler et al., 2024), and the Specula system’s architecture confirms that multicomponent pipelines substantially outperform single-pass generation (Cheng et al., 2025b). The cost of progressive prompting is a new class of structural errors (duplicate headers, missing terminators) that do not arise in single-pass strategies. This observation suggests that future systems should pair progressive decomposition with a lightweight global consistency check. The baseline 8.6% TLC success under progressive prompting sets a foundation that future work with finetuned models and improved datasets could substantially exceed through progressive decomposition and semantic feedback. Model Scale and the Scarce-corpora Formal Language Problem.: The inversion of scale, where DeepSeek r1:8b outperforms r1:70b and Qwen3:30b matches Qwen3:235b, recurs across families and strategies and is not noise. TLA+ is a scarce-corpora formal language: its entire public corpus amounts to hundreds of modules, dwarfed by billions of tokens of C, Python and Java. Larger models have proportionally more capacity devoted to high-resource languages, which manifests as stronger prior pulls toward mainstream syntax. Smaller reasoningdistilled models in the DeepSeek R1 series were trained with reinforcement learning on step-bystep symbolic reasoning traces (Guo et al., 2025); at 8B parameters the model reasons over TLA+ structure without the noise of the larger conflicting training pool. Mirzadeh et al. show that LLMs replicate reasoning steps from training data rather than performing genuine logical reasoning (Mirzadeh et al., 2025). A model whose reasoning depends on training distribution will be most affected when that distribution is sparse, as it is for TLA+ . For practitioners, this baseline guidance means that the largest available model is not necessarily the right choice: smaller, reasoning-oriented models may be more reliable and substantially cheaper. Negative Transfer from Code Specialization: Code-specialist models (CodeLLaMA, DeepSeek-Coder, Granite) consistently under-
perform general-purpose counterparts across all strategies. The mechanism is negative transfer: fine-tuning on C, Java and Python trains the model to associate token sequences (semicolons, curly braces, return) with correct code, and these associations are activated when generating TLA+ . This directly accounts for two of our five hallucination categories: semicolon injection and backtick fence insertion. Beg et al. identify the mismatch between target formal languages and pre-training distributions as a principal challenge for LLM-based formal requirements (Beg et al., 2025). When selecting a model for TLA+ generation, general-purpose reasoningoriented models retain the linguistic flexibility needed for TLA+ ’s unusual operator vocabulary and set-theoretic structure. Hallucinations Are Systematic and Mitigable: All five hallucination categories are traceable to specific training distributions rather than to the TLA+ generation task itself. Unicode operator substitution arises because documentation renders operators in mathematical Unicode (∈, ∧) while SANY requires ASCII (\in, /\). Semicolon and backtick injection arise from C-family and Markdown-dominated pre-training corpora. Reasoning token leakage is a side effect of chainof-thought fine-tuning. Generation length miscalibration (3.46× for HC, 2.24× for FIM, with outliers at 9.84×) directly explains the near-zero textual similarity scores. Phantom operator invention parallels the package hallucination phenomenon (Spracklen et al., 2025): models generate identifiers statistically consistent with context that do not exist in the target environment. The systematic and predictable nature of these errors is itself an opportunity: grammarconstrained decoding (Helwer, 2025) can enforce TLA+ syntax at the token level, deterministic post-processing (Unicode normalization, semicolon stripping, fence removal) can eliminate a large fraction of SANY failures before the parser is invoked, and retrieval-augmented generation over verified TLA+ specifications can ground operator usage in concrete examples. Implications for Practice: Progressive prompting achieves semantically valid specifications. Reasoning-oriented is favored over general-purpose models and code specialists. Deterministic post-processing (with augmented retrieval) before SANY could help with TLA+ synthesis, e.g., Unicode normalization, fence removal, and reasoning token stripping to eliminate the majority of preventable syntax failures
at zero cost. SANY pass rate can be only a base, as semantic validity requires model checking. Limitations: We run each model-specification pair once per strategy, so stochastic variation is not fully captured; we address this through scale (650 runs per strategy, 2,600 core runs total) with temperature and sampling parameters held constant across all models. Our 26 test specifications cover distributed protocols, concurrency problems, and algorithmic puzzles from the TLA+ community repository, but may not represent the full range of industrial use cases, as proprietary specifications from organizations such as Amazon and Microsoft are not publicly available. This study focuses on TLA+ , and the results may not transfer directly to other formal languages. Finally, the natural language inputs vary in comment density across specifications, and TLC validation is bounded to finite-state instances, so errors that appear only with larger parameter values remain undetected.
6
Conclusion
We present the first systematic evaluation of LLM-based TLA+ specification synthesis from natural language. Across 30 models, eight families, 26 test specifications, and more than 2,700 runs, results show a clear syntax-semantics gap. LLMs reach 26.6% SANY validity, yet only 8.6% pass TLC, and only under progressive prompting. DeepSeek r1:8b outperforms its 70B counterpart. Code-specialized models also trail generalpurpose models. Through our experiments, we identify five recurring hallucination categories: Unicode operator substitution, cross-language syntax injection, reasoning leakage, length miscalibration, and structural errors. These results show that current LLMs do not yet produce reliable TLA+ specifications rigorous review by a human. Future work should target three challenges in this area: (1) iterative repair/feedback loop with SANY and TLC to address the syntaxsemantics gap; (2) multi-step prompting with global consistency checks to mitigate lexical and structural errors in progressive generation; and (3) fine-tuning on TLA+ data with grammarconstrained decoding to reduce negative transfer and systematic hallucinations.
REFERENCES Abouelenin, A. et al. (2025). Phi-4-mini technical report: Compact yet powerful multimodal language models via mixture-of-loras. arXiv:2503.01743.
Anthropic (2023). Introducing claude: A nextgeneration ai assistant. Anthropic Blog. Anthropic (2025). Introducing claude sonnet 4.5. Anthropic Blog. Austin, J. et al. (2021). Program synthesis with large language models. arXiv:2108.07732. Beg, A., O’Donoghue, D., and Monahan, R. (2025). Leveraging llms for formal software requirements—challenges and prospects. arXiv:2507.14330. Cheng, Q. et al. (2025a). Sysmobench: Evaluating ai on formally modeling complex real-world systems. arXiv:2509.23130. Cheng, Q., Xu, T., and Huang, Y. (2025b). Specula: First place, genai-accelerated TLA+ challenge (code → spec). TLA+ Foundation. Cirstea, H., Kuppe, M. A., Loillier, B., and Merz, S. (2024). Validating traces of distributed programs against TLA+ specifications. arXiv:2404.16075. Contributors, O. (2024). Ollama: Open source runtime for local large language models. https://github.com/ollama/ollama. Ferrari, A. and Spoletini, P. (2025). Formal requirements engineering and large language models: A two-way roadmap. Information and Software Technology, 181:107697. Grattafiori, A. et al. (2024). The llama 3 herd of models. arXiv:2407.21783. Guo, D. et al. (2025). Deepseek-r1 incentivizes reasoning in llms through reinforcement learning. Nature, 645:633–638. Hahn, C. et al. (2022). Formal specifications from natural language. arXiv:2206.01962. Helwer, A. (2025). Second place, genai-accelerated TLA+ challenge. TLA+ Foundation. Jiang, A. Q. et al. (2023). Mistral 7b. arXiv:2310.06825. Kogler, P., Falkner, A., and Sperl, S. (2024). Reliable generation of formal specifications using large language models. In SE 2024 - Companion, pages 141–153. Gesellschaft für Informatik. Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. Lin, C.-Y. (2004). Rouge: A package for automatic evaluation of summaries. In Text Summarization Branches Out, pages 74–81. Association for Computational Linguistics.
Ma, L., Liu, S., Li, Y., Xie, X., and Bu, L. (2025). Specgen: Automated generation of formal program specifications via large language models. arXiv:2401.08807. Mirzadeh, I. et al. (2025). Gsm-symbolic: Understanding the limitations of mathematical reasoning in large language models. arXiv:2410.05229. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., and Deardeuff, M. (2015). How amazon web services uses formal methods. Commun. ACM, 58(4). OpenAI et al. (2024). Gpt-4 technical report. arXiv:2303.08774. Papineni, K., Roukos, S., Ward, T., and Zhu, W.-J. (2002). Bleu: a method for automatic evaluation of machine translation. In Proc. of the 40th Annual Meeting of the Association for Computational Linguistics, pages 311–318. Singh, A. et al. (2025). Openai gpt-5 system card. arXiv:2601.03267. Spracklen, J. et al. (2025). We have a package for you! a comprehensive analysis of package hallucinations by code generating llms. In Proc. 34th USENIX Security Symposium. Team, G., Mesnard, T., Hardin, C., Dadashi, R., Bhupatiraju, S., et al. (2024). Gemma: Open models based on gemini research and technology. arXiv:2403.08295. Terzian, G. (2025). Third place, genai-accelerated TLA+ challenge. TLA+ Foundation. + TLA Community (2025). TLA+ examples: A collection of TLA+ specifications and models. https://github.com/tlaplus/examples. TLA+ Foundation (2025). Genai-accelerated TLA+ challenge announcement. TLA+ Foundation. Wei, J. et al. (2022). Chain-of-thought prompting elicits reasoning in large language models. arXiv:2201.11903. Yang, A. et al. (2025). Qwen3 technical report. arXiv:2505.09388. Yao, J. et al. (2021). Distai: Data-driven automated invariant learning for distributed protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). Ye, H., Liu, T., Zhang, A., Hua, W., and Jia, W. (2023). Cognitive mirage: A review of hallucinations in large language models. Zhang, W. and Zhang, J. (2025). Hallucination mitigation for retrieval-augmented large language models: A review. Mathematics, 13(5):856.