Mistral AI Releases Leanstral 1.5 for Formal Verification
Original: Leanstral 1.5: Proof abundance for all
Why This Matters
Leanstral 1.5 advances open-source formal verification AI, bridging mathematical proofs and real-world software reliability.
Mistral AI released Leanstral 1.5 on July 2, 2026, an Apache-2.0 licensed model with 119B total and 6B active parameters. It achieves 87% on FATE-H, 34% on FATE-X, solves 587/672 PutnamBench problems, and discovered 5 previously unknown bugs across 57 open-source repositories.
Mistral AI announced Leanstral 1.5, the latest version of its formal verification model targeting Lean 4 proof engineering. The model carries 119B total parameters but only 6B active parameters, and is released under the permissive Apache-2.0 license, available via Hugging Face and a free API.
On benchmarks, Leanstral 1.5 saturates miniF2F, solves 587 out of 672 PutnamBench problems, and achieves state-of-the-art results of 87% on FATE-H and 34% on FATE-X. Training followed a three-stage pipeline: mid-training, supervised fine-tuning (SFT), and reinforcement learning using CISPO. Two RL environments were used — a multiturn environment where the model proves or disproves theorem statements and receives Lean compiler feedback, and an additional agentic setting for complex proof engineering tasks.
Beyond mathematical benchmarks, the model was applied to real-world code verification, testing 57 open-source repositories and uncovering 5 previously unknown bugs. Mistral AI positions this as evidence that formal verification methods can be both rigorous and practical for production software.