Mistral AI has released Leanstral 1.5, a new open-source code agent model built for Lean 4 formal proof engineering, automated theorem proving, and autoformalization. The model is available as labs-leanstral-1-5 through Mistral’s Labs API, in Mistral Vibe, and as downloadable weights on Hugging Face under an Apache-2.0 license.
The release targets researchers, proof engineers, developers working with formal methods, and teams exploring verified software. Mistral’s documentation lists Leanstral 1.5 with 119B total parameters, 6.5B active parameters, a 256k context window, text and image input, text output, and $0 pricing in Labs. The Labs listing also notes that the model is scheduled for retirement on September 30, 2026, indicating a limited-window experimental deployment rather than a permanent production endpoint.
Despite being primarily trained on math, Leanstral demonstrates impressive code verification capabilities, discovering previously unknown bugs in open-source repositories.
— Mert Ünsal (@mertunsal2020) July 3, 2026
We built an automated pipeline where Aeneas translates Rust code to Lean and Leanstral infers the user…
Mistral states that Leanstral 1.5 raises the ceiling for machine-checked reasoning in Lean 4. The company reports that the model fully saturates miniF2F, solves 587 of 672 PutnamBench problems, reaches 87% on FATE-H and 34% on FATE-X, and lifts FLTEval pass@8 from 31.9 to 43.2. Mistral also mentions that the model can continue working on very long proof attempts, citing a case where Leanstral processed more than 2.7 million tokens across 22 context compactions while proving AVL-tree time-complexity guarantees.
The system was trained through mid-training, supervised fine-tuning, and reinforcement learning with CISPO. In one training environment, Leanstral receives theorem statements, submits proofs, reads Lean compiler feedback, and revises until the proof compiles or the attempt budget ends. In another, it acts like a developer inside a raw filesystem, editing files, running bash commands, using the Lean language server, building helper lemmas, and completing partial proofs inside real repositories.
Mistral is also positioning the model beyond academic math. In a Rust verification pipeline using Aeneas and Lean, the company says Leanstral generated correctness properties, tried to prove them, then attempted to prove their negation when proofs failed. Across 57 repositories, Mistral claims that this process flagged 47 violations, 11 genuine bugs, and 5 bugs that had not previously been reported on GitHub.
This move builds on the first Leanstral release from March 2026, which Mistral described as its first open-source code agent for Lean 4 proof engineering. The older labs-leanstral-2603 model is listed as retired on June 30, 2026, and replaced by Leanstral 1.5. Early developer response is already forming around the tooling layer, with the maintainer of OpenATP stating that the package would be updated to point at Leanstral 1.5.
For Mistral, the release aligns with its broader push to offer full-stack AI systems spanning frontier models, developer tools, applications, and compute. The company frames Leanstral as part of its open model strategy and as a technical bet on AI agents that not only generate code but can also prove properties about code and mathematics through formal verification.
