Formal verification offers software's strongest correctness guarantee, but it's historically the hardest to obtain.

Teaching LLMs to prove their work correct is one of many critical steps towards making formal verification accessible and practically useful to all software engineers - our mission at Reasonable. This focus on practical application is why we’re proponents of a polyglot approach to software verification, and why we believe this is an essential capability for open-weight models.

Our focus includes program verifier Verus because it brings verification into the implementation in Rust, a language in which large scale systems and critical software are already built. TLA+ and temporal logic also feature heavily in our work, as these are widely used to model properties of complex distributed systems ranging from AWS to Azure, MongoDB to Kafka. For practical use performance, adaptability, speed, and cost matter greatly - making open-weight models attractive for domain- and task-specific specialization through fine-tuning.

Our latest work with NVIDIA brought all of these together: we developed a new training dataset (tlaverus-train), based on TLA+ translated to Verus, and a separate carefully selected evaluation dataset (tlaverus-60). We used it to fine-tune NVIDIA's latest open-weight model, the 120B parameter (12B active) - Nemotron™ 3.5 Super VL, testing its practical capabilities along the way.

Nemotron 3.5 Super VL is easy to fine-tune

• it is robust to learning rate and to hyperparameter choices

• fine-tuning significantly boosts pass-rate performance, in our application nearing that of Qwen 3.8-Flash-Next

• it forgets little and retains high performance on general knowledge and coding benchmarks

Nemotron 3.5 Super VL is fast

• 3.5 Super VL surpasses all models in its comparison class in terms of speed

• quantization improves inference efficiency even further without substantial loss in performance

Our temporal logic-based training datasets boosted generic verification skills

• our new dataset TLA-verus not only helps models prove properties of TLA+ specs, but teaches general verification skills that transfer to other unrelated Verus benchmarks

Section 1 explains how we created our datasets. Section 2 explains our fine-tuning process and results. Section 3 then compares tla-verus to other benchmarks. Finally, Section 4 tests for catastrophic forgetting.

TLA+ is a formal specification language used to design, model, and verify complex software and hardware systems. It is particularly useful for describing the behavior of concurrent and distributed systems. This provides a way to formally reason about the correctness of systems whose complex interactions are difficult to capture through testing alone. A TLA+ specification describes the system’s states, the actions that transition between them, and the properties that should hold over all possible behaviors. The properties we consider are:

• Safety: ensures that it executes safely following procedural constraints.

• Liveness: ensures that something good eventually happens.

• Invariance: ensures that a property holds in every reachable state.

• Type invariance: ensures that variables always have values of the expected type or domain.

Verus is a program verifier built on top of Rust. It allows developers to specify correctness and safety properties of their Rust code, and acts as an engine that checks if the Rust implementation satisfies those properties. Verus is an auto-active verifier, which means that some of the verification is generated automatically. However, complex problems require the developer to add proof annotations (invariants, lemmas, ghost code) that guide the underlying solver.

It is valuable to translate specifications from TLA+ to Verus, to move from reasoning about an abstract system model to creating machine-checkable proofs closely connected to executable code.

We translated TLA+ specs to Verus using our deterministic transpiler and our agentic translation pipeline, then decomposed them into (spec, property) pairs (Strelbytska et al, 2026). This resulted in a dataset with ~13k (spec, property) pairs on 2,676 specs. We then used various frontier models to verify these properties, applying standard techniques to prevent cheating. Some properties may not be provable, for example because the property declared in the source TLA+ was false in general. Therefore, we compiled our corpus from those (spec, property) pairs provable by at least one frontier-grade model using a generous test-time compute budget. Out of these, we selected 3,722 pairs with agentic traces from a frontier model. The details of obtaining agentic traces from these pairs is detailed later in section 2.

From these, we compiled a challenging benchmark, tlaverus-60, consisting of 60 tasks selected to be diverse across repositories and specifications. Of these, 40 pairs were chosen to be balanced across property types (safety, liveness, invariance, type invariance), and the remaining 20 were chosen for difficulty: among the tasks solved by only one of the frontier models, we selected those with the longest proofs

The selection process induces a distribution shift between training and evaluation: because tlaverus-60 was selected for diversity and difficulty, the benchmark tasks are, on average, harder and drawn from a broader set of repositories and specs than the fine-tuning data, so gains on the benchmark cannot be attributed to memorization of similar tasks.

Current Verus training datasets are mostly simple and tutorial-like (Di et al, 2026). As we move from simple to complex Verus tasks, such as verifying system properties, post-training approaches need to reflect this jump in complexity.

Such previous works focused on training mainly on problem-solution pairs, occasionally including thinking traces. We instead train on agentic trajectories. This enables models to learn more complex verification and proof repair tasks.

Generating agentic traces. We leverage our agentic pipeline we used for deciding which properties are provable. We selected an open-source frontier model and recorded its agentic traces on successful proofs. This resulted in a fine-tuning corpus consisting of 3,722 agentic proof sessions, covering 3,689 distinct theorems. Sequences average 43.2k tokens, and the corpus has a total of 160.8M tokens, out of which 46.7M are supervised (29%). The rest are user prompts or results of tool calls which the model should not learn to predict.

SFT settings. We use LoRA fine-tuning with rank 32 (α = 32, no dropout), applied to the attention projections, the Mamba input projections, and the MoE expert and latent projections, with learning rate 2e-4. Each training sequence is one agentic proof session of up to 65,536 tokens. We train with a global batch of 8 sequences (≈0.5M tokens per step) for one epoch (465 steps, 46.7M supervised tokens). We use AdamW (β = (0.9, 0.999), ε = 1e-8, weight decay 0.01) with gradient clipping at 1.0, a 50-step warmup followed by cosine decay to 1e-6 over the epoch, and bf16 training.

In our hyperparameter calibration sweeps, we found Nemotron 3.5 Super VL robust to minor changes in learning rate and rank. Hence we expect other settings to work well too.

LoRA rescaling. We found that rescaling the LoRA coefficient after fine-tuning boosts performance. A small grid search showed that simply halving the LoRA adapter's scale after SFT was a universally good choice across different runs.

We evaluate the models on three benchmarks: tlaverus-60, our main benchmark (Strelbytska et al, 2026), as well as 100 stratified-sampled tasks from VeruSAGE (Yang et al, 2025) and VerusBench (Yang et al, 2024). All models are evaluated in an agentic setting using the OpenCode harness, except Opus 5.5 which uses Claude Code. The agent can use the harness’s built-in tools to read the task file, write the output file, and invoke Verus iteratively, allowing it to inspect and refine its proofs until it stops or hits a predefined budget limit. The problems are evaluated with a single sample (pass@1) or with three independent trials (pass@3), and the final proof is checked with a strict anti-cheating gate.

We self-hosted all evaluated models except Opus 5.5. The self-hosted models are served with vLLM, with reasoning enabled and the appropriate reasoning parser for each model (e.g. ultra_v3 for Nemotron 3.5 Super VL and previously released Nemotron 3 Super). Where supported, we also enable MTP speculative decoding with 3 draft tokens. All Nemotron 3.5 Super models (base and fine-tunes) are used as language-only models. LoRA fine-tuning touches only the language layers, and at serving time the vision encoder is removed. We ran up to 20 problems concurrently on tlaverus-60, and 16 on other benchmarks.

The evaluation budget differs across benchmarks to account for their difficulty: tlaverus-60 allows up to 150 turns and 3 hours per problem, VeruSAGE-Bench up to 300 turns and 2 hours, and VerusBench up to 150 turns and 40 minutes.

Results.

Pass rate vs price per token

N.B. in this test, Qwen-3.8-Flash-Next benefits from a caching discount which Nemotron 3.5 Super does not receive, skewing price comparison in Qwen’s favour. There are indications that Nemotron 3.5 Super would perform better on a fair comparison basis but further work is required to disentangle.

Pass rate vs TPOT

Our evaluations of open-weight models on the tlaverus-60 benchmark dataset reveal that the Nemotron 3.5 Super VL base model even without fine-tuning outperforms Laguna S 2.1 and the 2x larger Inkling Small models in pass@1 rates of solving the tasks. Moreover, it already performs significantly better than Nemotron 3 Super - and its fine-tuned versions! Meanwhile the Opus 5.5 model in its own harness solves almost every benchmark task, even Qwen 3.8 Flash performs better than Nemotron 3.5 Super VL - so we asked whether we can improve the Verus proof writing capabilities of the latter via fine-tuning.

Fine-tuning on tlaverus-train improves the pass@1 performance of Nemotron 3.5 Super VL on tlaverus-60 by ~30 percentage points (pp) to 73.3%, approaching Qwen 3.8 Flash. This improvement is not specific to TLA-Verus: in the next section, we show that the gains translate to other Verus benchmarks as well. While fine-tuning improves Nemotron 3 Super’s performance by a similar absolute amount (approximately 30pp), it starts from a lower baseline value and underperforms Nemotron 3.5 Super VL.

In terms of speed, we measured the time per output token (TPOT), and found that Nemotron 3 Super, 3.5 Super VL, and their fine-tuned versions are the fastest among the compared models. Following the Nemotron 3 Super tech report, we also quantized our fine-tuned model, mostly to NVFP4, at 5.4 bits per weight. This maintains performance while further speeding up generation by ~20% and reducing model size from 230GB to 87GB fitting on a single NVIDIA Hopper GPU.

TLA-verus is a collection of new, novel verification tasks. But does it teach general verification capabilities beyond TLA+-style specifications? We looked into how fine-tuning on tla-verus transfers to open-source benchmarks VerusBench and VeruSAGE.

The creators of these benchmarks also compiled a training corpus, VeruSyn (Di et al, 2026), for efficiently teaching capabilities tested in these benchmarks. We wanted to assess the usefulness of tlaverus-train compared to training on VeruSyn, by looking at how much each training set’s effect transfers to the other benchmarks. However, the type of agentic traces the datasets contain are different. Our tlaverus-train dataset contains OpenCode traces with the model's reasoning and verbatim tool calls and outputs. VeruSyn's Part 2 subset consists of Copilot CLI terminal transcripts (Claude Sonnet 4.5) that were flattened into plain prose in order to fine-tune a non-reasoning target model, Qwen2.5-Coder-32B. As a result, there is no reasoning, and tool arguments and most observations other than Verus output are not recorded. This makes the dataset much less suitable for fine-tuning a reasoning model like 3.5 Super VL. To remove the format confounder, we created our own OpenCode agentic traces from VeruSyn problems. The number of supervised tokens were matched between tlaverus-train and VeruSyn.

Results. The table below shows that both training corpora improve over the base model’s performance on all benchmarks. However, on the challenging tlaverus-60, the VeruSyn-trained model gains ~13 pp, while training on tlaverus-train results in massive, ~30 pp increase. The model trained on tlaverus-train also matches or nearly matches the improvement of the VeruSyn-trained variant on the other two benchmarks. This is especially notable given the fact that VeruSyn is designed to be very similar to VerusBench, and surprising since tlaverus-train problems contain only minimal executable code.

We conclude that our tlaverus-train task set is useful for training general verification capabilities beyond temporal logic reasoning.

Supervised fine-tuning is prone to problems such as overfitting and catastrophic forgetting (see Luo et al, 2023). We tested our fine-tuned Nemotron 3.5 Super VL model on general knowledge and coding benchmarks.

• MMLU-Pro. Multiple-choice general knowledge questions (options A to J). We sample 500 questions from MMLU-Pro’s test set (12k questions).

• HumanEval. Short, textbook python functions. We evaluate all 164 problems.

• MBPP+. Entry-level Python tasks from Google's MBPP, 378 examples with hidden tests.

• LiveCodeBench. Competitive programming questions. We evaluate on 454 problems dated between Aug 2024 and April 2025. We have 110 easy, 141 medium, 203 hard problems.

Eval settings. We evaluate in prompt mode (non-agentic) with reasoning enabled. As the harness, we use NVIDIA NeMo™ open libraries for evaluation. We serve our models with vLLM, tensor parallel across 2 GPUs each. The evaluator keeps up to 256 problems in flight per server. All other settings, such as pass@k metrics and speculative decoding are identical to our tla-verus evaluations.

Results. The figure below confirms that there is essentially no forgetting after fine-tuning, with the fine-tuned model even improving on MBPP+. Nemotron 3.5 Super VL is therefore robust to retaining its existing capabilities during fine-tuning.

Caveat: Results reflect an early checkpoint of Nemotron 3.5 Super VL; numbers may shift by release

We believe the future of agentic software development involves widespread formal verification, as cost and complexity continue to be reduced significantly. Further, open models help accelerate practical application and Enterprise adoption - being amenable to domain- and task-specific fine-tuning, appealing to transparency and sovereignty requirements, and supporting speed+cost optimization.

By fine-tuning using our tlaverus-train dataset, and evaluating Nemotron 3.5 Super VL’s early checkpoints against our tlaverus-60 dataset, we demonstrated that the model is:

• Amenable to fine-tuning: easy and cost-efficient, generally very amenable to fine-tuning, with significant gains in task-specific performance

• Fast: among the similar sized models we tested in this program of work, 3.5 Super is the fastest (in TPOT)

Fine-tuning on synthetic data can significantly improve base-model performance.