Mistral open-sources Leanstral 1.5, a formal-verification model that saturates miniF2F

Mistral has released Leanstral 1.5, a free Apache-2.0 licensed model built specifically for formal verification and proof engineering in Lean 4, and it has effectively maxed out one of the field's standard benchmarks.

What's new

Leanstral 1.5 has 119B total parameters with only 6B active at inference, and Mistral is shipping it both as open weights on Hugging Face and as a free API endpoint. On results, Mistral says the model "delivers a major performance upgrade in formal verification": it saturates miniF2F (both validation and test sets), solves 587 of 672 problems on PutnamBench, and posts state-of-the-art scores of 87% on FATE-H and 34% on FATE-X. On FLTEval it reaches Pass@1 of 28.9% and Pass@8 of 43.2%.

The model was trained in three stages — mid-training, supervised fine-tuning, and reinforcement learning using CISPO — across two distinct environments: a multiturn setting where it iteratively proves theorems using compiler feedback, and a code-agent setting where it edits files, runs bash commands, and talks to a language server directly. Mistral highlights that design choice as central to the model's behavior: "Leanstral keeps reasoning, editing files, and revising across millions of tokens, turning that budget directly into solved problems."

Beyond benchmark scores, Mistral ran the model's bug-discovery pipeline against 57 real open-source repositories and says it turned up five previously unknown bugs, including a critical integer overflow in the zigzag-decoding function of the datrs/varinteger library — the kind of finding Mistral frames as proof the approach works outside synthetic benchmarks: it "uncovers previously unknown bugs in open-source repositories — proving that rigorous formal methods can be both effective and practical for real-world use."

Context

Formal verification — mathematically proving code or theorems correct rather than testing them empirically — has historically required specialist expertise and slow, manual proof-writing in languages like Lean. Model-assisted theorem proving has been an active research target for the major labs for several years (Google DeepMind's AlphaProof and various Lean-focused fine-tunes among them), but most efforts have targeted competition math benchmarks rather than paired code-agent behavior. Leanstral 1.5 combines both: strong formal-proof benchmark numbers and an agentic mode that behaves like a coding assistant with a compiler and language server in the loop, rather than a narrow theorem-proving tool.

Why it matters

Saturating miniF2F is a signal the benchmark itself is nearing the end of its useful life as a difficulty ceiling for this class of model — expect FATE-H/FATE-X and harder Putnam-style sets to become the new yardsticks. More practically, releasing this as a free, open-weight Apache-2.0 model rather than a closed research demo lowers the barrier for teams to try formal methods on their own codebases, and the five real bugs found in ordinary repositories are a concrete argument that formal verification tooling is approaching practical, not just academic, usefulness for everyday software.