Post-training Nemotron 3.5 Super VL for verified software development. By Szilvia Ujváry, Anna Mészáros, Balázs Szilágyi, Pál Czanik, Beatrix Benkő, Craig Hughes, and Ferenc Huszár Formal verification of complex software systems requires more than generating isolated proofs. Models need to interact with verification tools, diagnose failures, and iteratively repair their work. Reasonable built tlaverus-train, a new dataset of agentic proof trajectories derived from TLA+ specifications translated into Verus, alongside tlaverus-60, a challenging evaluation benchmark. In collaboration with NVIDIA, Reasonable used these datasets to fine-tune and evaluate Nemotron(TM) 3.5 Super VL, improving its pass@1 performance by around 30 percentage points to 73.3%. The gains also transfer to unrelated Verus benchmarks, while preserving general knowledge and coding capabilities. Combined with fast inference, its results demonstrate the potential of specialized open-weight models for practical software verification.