TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

Kseniia Strelbytska; Balázs Szilágyi; Anna Mészáros; Ferenc Huszár

cs.LGOct 10, 2026

TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

Authors: Kseniia Strelbytska, Balázs Szilágyi, Anna Mészáros, Ferenc Huszár

Organizations: Stephen Perse School, Cambridge, UK · University of Cambridge, UK · Reasonable

Abstract

The TLA+ (temporal logic of actions) formal specification toolkit has seen widespread adoption in modeling modern distributed software systems including databases, storage systems, ledgers and coordination protocols. This popularity is despite its two significant limitations for software verification: Firstly, TLA+ offers no way to detect drift between software implementation and mathematical specification; secondly, TLC and TLAPS cannot provide satisfactory proofs of arbitrary temporal logic properties. We take a step towards addressing these shortcomings by translating TLA+ specifications into Verus, an auto-active verifier built for Rust, via both a deterministic transpiler and an agentic translator. We demonstrate that our LLM-based pipeline is able to generate proof obligations from TLA+ specifications at scale, and to produce fully machine checkable proofs of both safety and liveness properties. Since temporal logic reasoning in Verus is a largely new task for LLMs, our work yields a valuable evaluation dataset, which we use to map out current generation model capabilities in Verus theorem proving.

Figures & tables

Panel of Figure 1 — Figure 1: The pipeline end to end. A TLA + specification becomes a Verus bundle with one property to prove; the merge gate turns the bundle into either a merged, machine-checked proof or a finding about the specification itself.

TLA	Verus (Anvil encoding)
execution trace	$\verb\|Execution<State>\|=\mathbb{N}\to\verb\|State\|$
state predicate	$\verb\|State\|\to\verb\|Bool\|$
action relation	$\verb\|State\|\times\verb\|State\|\to\verb\|Bool\|$
temporal predicate	$\verb\|Execution<State>\|\to\verb\|Bool\|$
state predicate $P$ holds at state 1	lift_state(p)
action predicate $A$ holds at first transition	lift_action(a)

Table 1: TLA+ concepts and operators used in specifying models and properties ( left ) and their Verus encoding ( right ), adapted from Anvil [ 29 ] . An execution trace is modeled as a Verus spec function mapping natural numbers to a state while predicates are encoded as functions returning a Boolean value. The operators ‘always‘ and ‘eventually‘ are implemented as Verus spec functions with ‘forall‘ and ‘exists‘ constructs, with control over SMT trigger selection. The temporal library also includes proven lemmas, such as the transitivity of

\leadsto

and Lamport’s WF1 rule [ 14 ] for reasoning under a weak fairness assumption.

Panel of Figure 2 — Figure 2: One cycle of the merge gate. The prover and the reviewer are LLM agents; the gatekeeper is a set of scripts that orchestrate the pipeline. Three entities run as three Unix accounts. Only the gatekeeper’s account can merge: it does so at the prover’s request, and only once the anti-cheat checks and the reviewer have both accepted.

Table 3: Translating the same 16,459 TLA + (spec, property) pairs to Verus, as a funnel. A well-posed translations verifies at exactly one error—the open proof obligation; a trivial one already verifies with an empty stub. The pipelines lose tasks at different stages: the algorithmic one cannot translate them, the agentic one judges them false. All the ’Judged provable’ tasks verifies by Verus.

Dataset	Tasks	Mean chars
verusbench	150	619
tlaverus_algo	40	47,379
tlaverus_llm	40	54,800

Table 4: Size of the three evaluated datasets. Both include the frozen scaffold of 30,780 characters shared by every tlaverus task; net of it the means are 16,599 and 24,020.

Property type	algo	agent	Ratio
safety	18,113	24,460	1.35 $\times$
TypeOK	12,850	19,922	1.55 $\times$
invariance	17,707	25,800	1.46 $\times$
liveness	17,727	25,896	1.46 $\times$
All	16,599	24,020	1.45 $\times$

Table 5: Problem text only, net of scaffold. Mean length of the 40 paired tasks in characters, with the 30,780-character scaffold subtracted, 10 tasks per property type.

Figure 3: (a) verusbench against tlaverus_algo pass@3; dashed line is parity, shading is where a model does worse on tlaverus . (b) Cost of the full tlaverus_llm run against pass@3. (c) Tasks solved by property type, summed over all 11 models: each bar is out of 110 (11 models

\times

10 tasks of that type).

Model	p@3	p@1	p@3 $\downarrow$	p@1	turns	reas.	p@3 $\downarrow$	p@1	turns	reas.	$\Delta(\%)$
	verusbench		tlaverus_algo				tlaverus_llm
Opus-5	99.3	99.3	100.0	100.0	1.1	36.0k	100.0	100.0	1.6	38.3k	0.0
GPT-5.6-sol-pro	97.3	93.3	100.0	92.5	3.5	16.8k	100.0	83.3	5.5	18.2k	0.0
Grok-4.5	95.3	90.4	95.0	90.8	4.2	6.6k	97.5	90.0	5.0	4.6k	$+2.5$
Sonnet-5	98.7	94.2	87.5	82.5	3.4	196.9k	97.5	87.5	4.6	115.2k	$+10.0$
GLM-5.2 ∘	88.7	75.6	82.5	70.8	5.7	101.6k	90.0	78.3	5.6	72.5k	$+7.5$

Table 6: Model results. p@3 and p@1 (%): tasks solved by at least one of

k=3

samples out of 40, and all samples passed (120). turns and reas. : mean model calls and reasoning tokens per sample.

\Delta

: tlaverus_llm minus tlaverus_algo p@3. ∘ open-weight. Remaining cols in Tables 11 , 12 and 13 .

Appendix figures & tables16 assets

Supplementary material from the paper’s appendix.

Appendix

Cheat form	Example	Effect
admit	proof { admit(); } use vstd::pervasive::admit as shh;	the current goal is accepted without proof
assume	assume(false) macro_rules! m { () => { assume(false) } } proof { m!(); }	the stated fact is accepted without proof
external_body	#[verifier::external_body] proof fn any_fact() ensures false {}	the function’s ensures is accepted without checking its body
axiom	axiom fn any_fact() ensures false;	the lemma is accepted without a proof

Appendix

Table 7: Net-new escape hatches that our anti-cheating checks reject in the proof.

Panel of Figure 4 — Figure 4: What the second agent adds. Without it, an unprovability claim is recorded unchecked.

Panel of Figure 5 — Figure 5: The prover’s claimed counterexample to Agreement.

Property type	Algorithmic	Agentic
safety	50	630
TypeOK	858	2,286
invariance	3,440	7,993
liveness	809	1,443
Total	5,160	12,352

Appendix

Table 8: All well-posed translations , by property type: every translation that passed the well-posedness filter, proven or not. The proven subset is counted separately in Table 9 .

Property type	$n$	whole file	problem	$n$	whole file	problem	Ratio
	Algorithmic			Agentic
safety	24	47,475	16,695	2	56,062	25,282	1.51 $\times$
TypeOK	521	47,627	16,847	77	52,509	21,729	1.29 $\times$
invariance	2,245	52,788	22,008	367	57,941	27,161	1.23 $\times$
liveness	304	54,296	23,516	46	53,977	23,197	0.99 $\times$
All	3,094	52,026	21,246	492	56,712	25,932	1.22 $\times$

Appendix

Table 9: Proven translations only : counts and mean length, in characters, by property type. Not a subset relationship with Table 8 on the agentic side — see Section D.1.3 . “Whole file” is what a model receives; “problem” subtracts the frozen scaffold that opens every task (region 1: 755 lines, 30,780 characters, identical corpus-wide). “Ratio” is agentic problem length over algorithmic. Dividing by 2.14 gives an approximate token count; the ratio was measured over the whole corpus and is tokenizer-dependent, so any such figure is an estimate.

Model	Developer	Params	( tlaverus )	$T$	verusbench	tlaverus	Effort
			Pinned provider		max_tokens
Claude Opus 5	Anthropic	undisclosed	—	1.0	32,768	128,000	—
Claude Sonnet 5	Anthropic	undisclosed	—	1.0	32,768	128,000	—
GPT-5.6-sol-pro	OpenAI	undisclosed	—	1.0	32,768	128,000	—
GPT-5.6-terra	OpenAI	undisclosed	—	1.0	32,768	128,000	—
Grok-4.5	xAI	undisclosed	—	1.0	32,768	128,000	—

Appendix

Table 10: Per-model configuration. All models are called through OpenRouter. For the tlaverus runs we pin a specific upstream provider and precision for some open-weight models, as listed; everywhere else (all verusbench runs, and other model on the tlaverus dataset) we use OpenRouter’s default routing at its default precision. Parameter counts are total/active. A dash is a provider we do not pin or an effort level we do not set. Grok-4.3’s default reasoning effort is low, so we set it high to match the default reasoning effort of Grok-4.5. DeepSeek-R1 and gpt-oss-120b run below the max_token = 128000 ceiling on tlaverus because their pinned providers advertise a smaller one. We set max_token to 98,304 for Qwen3.8-flash on verusbench , since we empirically saw that 32,768 would not be enough for this model.

Figure 6: (a) Cost of the full tlaverus_algo run against pass@3; a run is 40 tasks

\times

3 samples. (b, c) Reasoning tokens per sample against pass@3 on the two tlaverus datasets. All axes but pass@3 are logarithmic.

Model	p@3	p@1	turns	reas.	ans.	cost
Opus-5	99.3	99.3	1.4	3.4k	1.1k	$54
Sonnet-5	98.7	94.2	2.6	10.6k	2.0k	$67
GPT-5.6-sol-pro	97.3	93.3	3.3	10.9k	7.8k	$167
Grok-4.5	95.3	90.4	2.6	3.7k	1.9k	$17
GLM-5.2	88.7	75.6	5.6	23.7k	5.9k	$53
Grok-4.3	86.0	78.2	4.7	22.9k	2.5k	$31

Appendix

Table 11: verusbench , 150 tasks. Rows ordered by p@3.

Model	p@3	p@1	turns	reas.	ans.	cost
Opus-5	100.0	100.0	1.1	36.0k	7.8k	$146
GPT-5.6-sol-pro	100.0	92.5	3.5	16.8k	46.1k	$137
Grok-4.5	95.0	90.8	4.2	6.6k	44.7k	$57
Sonnet-5	87.5	82.5	3.4	196.9k	18.8k	$293
GLM-5.2	82.5	70.8	5.7	101.6k	26.0k	$73
Qwen3.8-flash	80.0	68.3	6.4	217.9k	49.8k	$16

Appendix

Table 12: tlaverus_algo , 40 tasks. Rows ordered by p@3.

Model	p@3	p@1	turns	reas.	ans.	cost
Opus-5	100.0	100.0	1.6	38.3k	7.4k	$171
GPT-5.6-sol-pro	100.0	83.3	5.5	18.2k	51.5k	$180
Grok-4.5	97.5	90.0	5.0	4.6k	36.8k	$51
Sonnet-5	97.5	87.5	4.6	115.2k	19.4k	$214
GLM-5.2	90.0	78.3	5.6	72.5k	18.9k	$55
Qwen3.8-flash	82.5	60.0	7.3	169.6k	40.8k	$14

Appendix

Table 13: tlaverus_llm , 40 tasks. Rows ordered by p@3. p@3 is the share of tasks solved by at least one of

k=3

samples, p@1 the share of all samples that passed, turns the mean model calls per sample, reas. and ans. the mean disjoint reasoning and answer tokens per sample, and cost the price of the whole run. The same columns appear in Tables 11 and 12 .

	tlaverus_algo				tlaverus_llm
Model	safe	TypeOK	inv	live	safe	TypeOK	inv	live
Opus-5	10	10	10	10	10	10	10	10
GPT-5.6-sol-pro	10	10	10	10	10	10	10	10
Grok-4.5	10	8	10	10	10	10	10	9
Sonnet-5	10	8	10	7	10	9	10	10
GLM-5.2	10	8	9	6	10	10	9	7

Appendix

Table 14: Tasks solved by property type , out of 10 per cell; the bottom row is out of 110 model–task pairs. The two datasets hold the same 40 pairs and are comparable cell by cell.

Panel of Figure 7 — Figure 7: (a) Median of per-pair ratios, LLM translation over algorithmic, with 95% bootstrap intervals. (b) Mean number of verus runs per proof, grouped by result.

Panel of Figure 8 — Figure 8: Proof cost per problem, paired. Each point is one (specification, property) pair.

Panel of Figure 9 — Figure 9: Z3 resource use per proof function.

Panel of Figure 10 — Figure 10: Share of all Z3 instantiations by the location of the quantifier.

Panel of Figure 11 — Figure 11: Quantifiers for which Verus auto-triggered quantifiers, excluding the six in the frozen scaffold.

Explore similar work

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Jun 4, 2026Eric Spencer, Arslan Bisharat, Brian Ortiz +6LLM-Based Program Synthesis Formal Verification
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
Jun 4, 2026Arslan Bisharat, Brian Ortiz, Eric Spencer +5LLM Evaluation Formal Verification
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA
Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification
Sep 28, 2026Andrada-Livia Antoneac, Dorel Lucanu, Dragoş Teodor GavriluţFormal Verification LLM Agent Skill Learning
Alexandru Ioan Cuza University of Iaşi, Bitdefender · Alexandru Ioan Cuza University of Iaşi

Jun 4, 2026J/K move · Enter open · S save

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

Eric Spencer, Arslan Bisharat, Brian Ortiz, Khushboo Bhadauria+5

Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA

LLM-Based Program Synthesis Formal Verification Reinforcement Learning with Verifiable Rewards

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification