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. 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.