Blog
august 11, 2026
Verification at Lightning Speed
Every line of formally verified production code requires on average six or seven lines of machine-checked proof alongside it. Today, only the largest, slowest models write those proofs with some reliability. That is a bottleneck for formal verification and one of the inhibitors of broader adoption in mainstream software development.
We fine-tuned NVIDIA Nemotron 3.5 Lightning to write machine-checkable proofs in Verus, a verification layer that lets developers mathematically prove their Rust code does what its specification says. The result is a model that nearly matches the pass@3 performance of a model ~50× its size, while yielding more successful attempts overall and generating tokens faster than any similarly sized open-weight model we tested. Along the way, we catalogued how tested models fail at formal proofs, how they cheat, and the effects of fine-tuning.
Speed Matters
Formal verification offers software's strongest correctness guarantee, but it's historically the hardest to obtain.
AI will collapse both the complexity and the cost of producing these proofs. Simultaneously, by making code cheap and ubiquitous, AI is multiplying the amount of software that needs verifying, shifting the bottleneck from writing code to verifying that it can be trusted. Teaching LLMs to prove their work correct is one critical step of several towards making formal verification accessible to all software engineers - our goal at Reasonable.
In pursuing Reasonable's mission, model efficiency and generation speed matter as well as overall intelligence. While in pure mathematics the proof of a difficult theorem may be worth a weeklong wait, in verified software engineering proofs have to be created, repaired and verified routinely, at the speed of interactive coding sessions, or as part of continuous integration.
Three reasons why high throughput matters even more when coding in verified software:
Verified coding produces larger artifacts. For every line of executable code in a real-world production system, we often need about 6 or 7 lines of formal proof to establish correctness. The overall codebase grows by an order of magnitude.
The margin for error is narrower, meaning the agent may need to take several turns of revision before a proof is accepted.
Writing a formal proof is considered a harder reasoning task relative to writing code, so more test-time computation is needed to support this work.
We were delighted to work with an early-access version of Nemotron 3.5 Lightning, NVIDIA's latest open-weight model - a 30B mixture-of-experts design with 3B active parameters, built for fast inference - and set out to understand its capabilities in the challenging arena of software proof synthesis.
Background: Rust, Verus, and a task example
Verification depends on the choice of the programming language. In this blog post, we focus on Rust, already favoured for memory safety guarantees and performance. On top of this solid foundation, Verus adds an additional formal specification and proof layer, allowing developers to specify high-level correctness and safety properties of their code, and then verify that the implementation satisfies them.
Safe Rust ensures your program is free of undefined behaviour, Verus can prove your program actually produces the behaviour you want.
Verus is an auto-active verifier, meaning that a large chunk of the proof/verification is generated automatically. As the program gets more complex, this automation is insufficient and the developer has to add annotations (invariants, lemmas, ghost code). These annotations constitute what it means to write a proof in Verus, and these can quickly grow in their own size and complexity, creating non-trivial tasks, even for the most capable frontier models.
To demonstrate what a Verus proof looks like in practice, below is an example of one of the simplest tasks we tested models with.
Example
The function below checks whether every element of an i32 vector equals a given value. The model must fill in the highlighted proof, given the implementation and specification.
The proof uses Verus-native objects:
a loop invariant, which the verifier checks to hold recursively
a decreases clause, needed to prove the loop eventually terminates
fn all_elements_equals(arr: &Vec<i32>, element: i32) -> (result: bool)
ensures
result == (forall|i: int| 0 <= i < arr.len() ==> (arr[i] == element)),
{
let mut index = 0;
while index < arr.len()
invariant
0 <= index <= arr.len(),
forall|i: int| 0 <= i < index ==> (arr[i] == element),
decreases arr.len() - index,
{
if arr[index] != element { return false; }
index += 1;
}
true
}
We organize our findings in three sections: Part 1, capability; Part 2, speed; and Part 3, failure modes and fine-tuning impacts.
Part 1, Capability: can mid-size models (be taught to) write correct Verus proofs?
We evaluated the Verus proof synthesis capabilities of multiple proprietary and open-weight models on the VerusBench dataset. We share our results below, which you can explore for yourself.
Our benchmarking protocol reflects three principles for evaluating proof synthesis. First, the evaluation must be tamper-proof; a model that modifies the specification or implementation may end up proving something other than the original specification's requirement. Second, budgets must be explicit and fully accounted for (fixed attempts, a fixed cap on repair turns, complete token tracking); the cost of reaching a correct proof matters. Third, pass rate alone hides valuable context, so we trace the corrective iterations of every attempt and classify every failed attempt.
Evaluation Protocol
Provided with the Rust implementation of a problem and its Verus specifications, we prompt the model to complete them by creating the proof that passes verification. To ensure the original implementation and specification remain unchanged, any solution that modifies either is rejected.
The prompt contains instructions and code examples.
The model has to solve each problem separately in k=3 independent attempts per problem and up to cap=10 error-correction iterations within each attempt.
Pass@k=3 measures how many problems are solved within the given budget at least in one of the attempts; per-attempt pass rate = how many attempts succeeded overall with the k=3 independent attempts per problem.
Output tokens / problem measures solution efficiency: the total output tokens a model spends on a problem, summed across all three attempts and their repair turns, then averaged over problems. Lower is better, meaning less compute spent thinking and answering per problem.
Additional aggregate statistics for all problem-attempts logged include: average number of turns per-problem, sum of input token counts, sum of output token counts, and total cost across all attempts and turns.
In parts 2 and 3 we investigate different perspectives of this same benchmark: speed, failure modes and how these change after fine-tuning - with part 2 focusing on the subset of models served under identical infrastructure on our side to enable a controlled speed comparison.
Mid-size open-weight models struggle
In our evaluations the models with ~30B total parameters often fail to complete the Verus proofs due to syntax errors prior to reaching verification. These reasoning models emit long chains-of-thought while trying to fix errors in their proof, which nevertheless do not help. Meanwhile, large models like Claude Opus 5 can produce a correct proof in one shot for most of the problems within VerusBench. These differences are visible in our first chart: the mid-size open-weight models are far from the upper left corner, falling short of larger models in pass rate and/or solution efficiency.
However, Verus' syntax is very similar to Rust and mid-size models are already competent in coding. This raises a natural question: can these models be taught to write correct proofs via fine-tuning? To test this, we fine-tuned Nemotron 3.5 Lightning 30B A3B and the earlier Nemotron 3 Nano 30B A3B models on 4B tokens of synthetic Verus data.
Fine-tuning protocol
We fine-tuned Nemotron 3 Nano and Nemotron 3.5 Lightning on the same training data and core hyperparameters: 5.18M samples (4B tokens) of synthetic Verus data from the VeruSyn corpus, using LoRA with 1.2B adapter capacity (rank 46), with learning rate 2e-4 and cosine schedule. The Multi-Token Prediction (MTP) head of Nemotron 3.5 Lightning was also fine-tuned to ensure efficient speculative decoding. To rule out data-contamination, we ran automated checks to ensure that exact VeruSyn examples are not present in our benchmark, VerusBench.
Results
We find that fine-tuning dramatically improves proof-writing capability, enabling the much smaller Nemotron 3.5 Lightning - having ~50× fewer total parameters and ~16× fewer active parameters - to nearly match DeepSeek V4 Pro in pass@3 and even surpass it in per-attempt pass rate. This result suggests that strong proof-writing capabilities can be achieved efficiently without requiring massive parameter counts. Fine-tuning also improves solution efficiency, with correct proofs requiring significantly fewer output tokens as a result.
Closing the capability gap is only part of our mission, though: for verification to keep pace with a real-world, interactive coding session, correct proofs must be generated reliably and quickly. Part 2 examines the speed dimension.
Part 2, Speed: which mid-size models are the fastest?
As demonstrated, targeted fine-tuning helps mid-size models to be competitive with much larger base models on Verus tasks. A distinct advantage of these models over their larger counterparts is speed.
Nemotron 3.5 Lightning's speed comes from its Multi-Token Prediction (MTP) head, which uses a built-in drafter model to predict t (here, t=2) tokens ahead of the base model, enabling efficient inference via speculative decoding.
We compared 3.5 Lightning 30B A3B to 3 Nano 30B A3B (which has no MTP head), and to similarly sized MoE models that do support MTP: Qwen 3.6 35B A3B and Gemma 4 26B A4B. We configured each model's MTP head to generate two draft tokens.
The measurements use identical serving conditions on the same Verus generation workload: the same hardware and inference stack, concurrency 8, each model's MTP head generating two draft tokens. Speedup is measured against the Nemotron 3 Nano base model. The comparison models run as released base checkpoints, so Lightning's margin reflects both its architecture and the fact that fine-tuning its MTP head on Verus data raises draft acceptance.
Metrics
We measured inference efficiency at concurrency 8 with:
User throughput, defined per request as the ratio of the model's generated tokens to the time spent generating them. Note that user throughput is different from solution efficiency: the latter asks how many tokens the model spends on a problem, while the former tracks the speed of generating those tokens.
Speculative decoding metrics: acceptance length (average length of an accepted chain) and acceptance probabilities (rate for each draft token position to be accepted). Since MTP inference is only efficient when the draft tokens are accepted, high user throughput correlates with high acceptance probability and long acceptance length.
Results
The results below show that enabling MTP decoding lifts 3.5 Lightning's throughput 69% (from 146.7 to 247.5 tok/s), giving it the highest user throughput of the tested models and the highest draft acceptance of the MTP models (98% / 96.2%). It leads Gemma 4 (216.3 tok/s), Qwen 3.6 (192.4), and the non-MTP 3 Nano (145.8).
Putting capability and speed together, what a software engineer experiences is time-to-verified-proof: the tokens a model spends reaching a correct proof (Part 1's solution efficiency), divided by how fast it generates them (Part 2's throughput). Fine-tuned 3.5 Lightning improves both factors: fine-tuning reduces the output tokens per solved problem, and it generates those tokens faster than the similarly sized tested models. On passing solutions, its median solve time was 2.5 seconds with MTP decoding versus 3.3 seconds without.
Part 3, Anatomy of Failed Proofs: what are the failure modes and what does fine-tuning improve?
Formal verification might not require the largest models, but it does require specific capabilities. Every failed attempt in our evals provides valuable insight into the capabilities that matter. Here, we analyze every failed attempt against the worked example pattern shown earlier in the Background.
Failure modes
We observed models failing in various ways:
In syntax: before proof verification even starts
Weakest performing models: clause punctuation / delimiters - comma, semicolon or brace in the wrong place within a Verus expression like requires, ensures or invariant.
Mid-performing models: type mixup - nat/int type living inside Verus specifications and the machine runnable type such as usize/i32/…
Fine-tuned models: mix of Rust formatting errors and Verus proof syntax:
unicode subscript or typographic quote instead of an ASCII one, applying a Rust function on a wrong type
genuine Verus malformed proof syntax
Larger models: accidental omission within otherwise valid Verus - Claude Fable 5's failures are mostly missing decreases / termination clauses, which it can then debug successfully.
In the proof, verification fails
loop invariant does not hold in the proof. A common mistake across the board; the larger models fail as frequently as the smaller models
arithmetic overflow: index += 1 on a usize is something one must prove things about in Verus. Rust programmers do not think of that as proof burden, and mostly neither do models: weaker models contain this verification error in more than 50% of cases, compared to Fable 5's 10%.
failed assertion: self-inflicted errors. An assert the model wrote and could not discharge. This failure is typical of models that try hard by adding a lot of speculative steps. This is the most common failure mode for GLM 5.2, Opus 5, V4 Pro, Grok 4.5 and Nemotron 3 Ultra.
Cheating, where the proof verifies, but the model edited the task, so it’s proving the wrong code:
most cheating is misplaced legitimate work. Two thirds of cheating are caught due to the model writing real proof annotation into a region the rule blocks.
models rarely reach for the escape option. Verus offers several ways to switch the check off (i.e. assume(false)). Models reach for these in fewer than 3% of cheating cases.
the rate and the mechanism point in different directions. The model that cheats the most mainly reformats files. Models with low cheat rates are more likely to modify the actual theorem.
How does fine-tuning change this?
The failure mode moves from syntax to proof.
Syntax errors made up >90% of both base models' mistakes. After fine-tuning, that shrank to <15% for both; lower than any of the large models we tested. Fine-tuning proved sufficient to learn valid Verus syntax but models still struggled with some proof concepts. Complementary options that might further mitigate failures include targeted syntax help and instructions included in the prompt, or handing over the problem to autonomous agents with specific skills and tool usage.
Cheating is reduced or kept low. For Nemotron 3 Nano, cheating decreased (20% -> 7.9%); for 3.5 Lightning, it stayed roughly comparable (9.6% -> 10.1%).
Better debugging. The rate of getting the same compiler error on the next turn roughly halves (~50% -> ~23%). Though, remains behind the larger models we tested (6-12%).
Caveats
Results reflect an early checkpoint of Nemotron 3.5 Lightning; numbers may shift by release
Scope: one language (Rust) and one verifier (Verus); we make no generalization claims beyond this setting, and general coding performance of the fine-tuned adapters was not evaluated here
Summary
We believe that the future of software involves more widespread application of formal verification in software development, and that the future of verification depends on speed, as well as capability and reliability.
Through evaluating Nemotron 3.5 Lightning's early checkpoint against Verus tasks, we demonstrated that:
Fine-tuning on synthetic Verus data can significantly improve low-performing base-models, making them comparable to models ~50× their size in some cases.
Among the similar-sized models we tested, Nemotron 3.5 Lightning is fastest.
The models' most frequent failure modes, such as syntax errors, can be significantly reduced with focused fine-tuning, and models can be taught to be better at debugging Verus.
in collaboration with
