Mistral launches Leanstral 1.5 with major performance upgrade in formal verification

Mistral has released Leanstral 1.5, a major update to its open-source code agent designed for Lean 4 users seeking improved formal verification tools. Leanstral 1.5 is distributed under the Apache-2.0 license and features a model with 119 billion total parameters, of which 6 billion are active. This upgrade delivers a notable performance boost in formal code verification, intended to make rigorous proof engineering more attainable.

Building on these technical foundations, Leanstral 1.5 achieves new state-of-the-art results in several popular proof benchmarks: it solves 587 of 672 PutnamBench problems, saturates miniF2F, and reaches 87% on FATE-H and 34% on FATE-X. Beyond numerical benchmarks, the model has proven its effectiveness by verifying complex code properties and identifying previously unknown bugs in open-source repositories.

Following its advanced training pipeline, which includes mid-training, supervised fine-tuning, and reinforcement learning with the CISPO method, the agent demonstrates strong capabilities in agentic proof engineering. During testing, it uncovered five previously unknown bugs across 57 repositories. While the training focus was primarily mathematical, Leanstral 1.5 also exhibits strong code verification skills.

To encourage broader adoption, Leanstral 1.5 is fully open-sourced and available for download on Hugging Face. Users can also access it via a free API for practical Lean 4 proof engineering.