Skip to content
NewsModel release

Mistral releases Leanstral 1.5, an open formal-verification model that solved 587 of 672 Putnam math problems

· by Pondero Newsdesk

The short version

Mistral AI released Leanstral 1.5 on July 2, a 119-billion-parameter open model for Lean 4 formal verification that saturated miniF2F, solved 587 of 672 PutnamBench problems, and found five previously unknown bugs in production code across 57 repositories.

Mistral releases Leanstral 1.5, an open formal-verification model that solved 587 of 672 Putnam math problems

Mistral AI released Leanstral 1.5 on July 2, a 119-billion-parameter mixture-of-experts model built specifically for Lean 4 formal verification. It found five previously unknown bugs in production code across 57 open-source repositories tested, a result that goes beyond synthetic benchmarks.

What

Leanstral 1.5 has 119B total parameters but only 6.5B active per token, keeping inference costs manageable for a model in this class. Per Mistral's release post, it saturates the miniF2F benchmark completely (100% on both validation and test sets), solves 587 of 672 problems on PutnamBench (graduate-level competition math), and sets a new state-of-the-art on FATE-H (87%) and FATE-X (34%), benchmarks covering abstract algebra at the graduate and PhD level.

The cost picture stands out. Mistral reports the model costs roughly $4 per Putnam problem at a 4-million-token budget, compared with an estimated $300 or more per problem for Seed-Prover 1.5 on its high setting. Leanstral also outscores Seed-Prover 1.5 by 7 problems on PutnamBench under that comparison.

Beyond math, Mistral tested the model on real code. Using an automated pipeline that translated Rust code to Lean 4 via the Aeneas tool, Leanstral attempted to prove or disprove inferred correctness properties. Across 57 repositories, it flagged 47 violated properties, 11 of which pointed to genuine bugs. Five of those 11 were previously unreported on GitHub. One confirmed bug was a silent integer overflow in the varinteger library's sign function: passing the maximum 64-bit unsigned integer caused a crash in debug mode and silent data corruption in release.

The model ships under an Apache 2.0 license with weights on Hugging Face and a free API endpoint accessible as leanstral-1-5. Mistral recommends running it inside Mistral Vibe with an optional Lean LSP MCP server for real-time compiler feedback.

Why it matters

Formal verification has long been expensive and tooling-dependent enough to stay confined to safety-critical hardware and cryptography projects. A model that runs agentically inside a standard Lean 4 development environment and finds real bugs in arbitrary Rust code changes that calculus. The Apache 2.0 license means teams can run it on private codebases without routing data through a vendor API, which removes the main compliance objection for regulated industries.

The cost comparison with Seed-Prover matters practically: at $4 per Putnam problem versus $300-plus, the gap is large enough that formal verification becomes plausible as a routine CI step rather than an occasional specialist engagement. Five new bugs in 57 repositories, found automatically without any manual specification of what to check, is the kind of result that gets security and reliability engineers to actually try a tool.

No comparable open-weights formal verification model exists at this scale, per Mistral's announcement. That claim is plausible given the benchmark comparisons: the models that score higher on PutnamBench either receive natural-language proof guidance (a different and harder-to-automate input) or cost an order of magnitude more to run.

What to watch next

Whether Lean 4 IDE plugins and CI/CD integrations adopt Leanstral as a default backend will determine how quickly the model moves from research artifact to production tool. The more concrete milestone is how Leanstral performs on FLTEval going forward: Mistral open-sourced that benchmark with this release, which should enable independent comparisons against models like DeepMind's AlphaProof that have not previously been measured on the same scale.

Sources