Last updated: July 15, 2026
Leanstral 1.5 is Mistral’s Apache-2.0 open-weight code agent for Lean 4 proof engineering. It generates and edits Lean proofs inside Mistral Vibe, the company’s general code-agent interface, while Lean and a verifier called SafeVerify perform the mechanical checks. Mistral reports strong results on formal-mathematics benchmarks. It is not a turnkey verifier for arbitrary software, and its free hosted endpoint is an experimental Labs service listed for retirement on September 30, 2026.
The decision in one sentence: evaluate it if your team already works in Lean 4 and owns the surrounding specification, translation, and review workflow; otherwise, skip it.
- Lean and Mathlib maintainers and formal-methods researchers
- Teams already maintaining a Lean codebase
- High-assurance groups that write formal specifications and can work within the supported translation path
- Teams wanting a general coding assistant
- Verifying arbitrary production software without Lean and a translation path
- Anyone needing a stable, supported production endpoint
- Sending sensitive code to the hosted endpoint without a data-governance review
| Model role | Specialized Lean 4 proof-engineering code agent (Mistral AI) |
| Architecture | 119B total, 6.5B active per token, mixture-of-experts (128 experts, 4 active) |
| Context | 256k advertised, 200k recommended |
| License | Apache-2.0 open-weight, on Hugging Face |
| Hosted identifier | labs-leanstral-1-5 (Labs tier) |
| Hosted price | $0, experimental; listed retirement September 30, 2026 |
| FSR test boundary | Document-first. No hands-on. Vendor results not independently reproduced. |
Contents
On this briefing
The finding: the model is free, the verification system is not
The launch coverage of Leanstral 1.5 repeats a short list: 119 billion parameters, a perfect miniF2F score, five bugs found in open-source code, Apache-2.0, free API. Each item is accurate. Together they invite the wrong conclusion, that adopting Leanstral is close to free.
The access price is genuinely low. The cost of producing a trustworthy proof is not. It helps to separate the two by layer:
| Access | $0 Labs endpoint, or Apache-2.0 weights. This layer is cheap. |
| Inference | Currently $0 on the hosted endpoint, or your own compute if you self-host. |
| Proof-search time | Trajectories up to millions of tokens. Mistral’s AVL proof ran over eight hours. |
| Formalization labor | Writing or approving specifications, translating code into Lean, reviewing proofs. Needs Lean 4 expertise. |
| Governance | Labs data-use terms, endpoint retirement, rate limits, migration. |
The first two layers are where “free” is true. The last three are where the real work and risk sit, and they do not move because the license changed. The rest of this briefing walks each one against Mistral’s own documentation.
What Leanstral actually does
Leanstral 1.5 is a specialized Lean code agent, not a general coding assistant. It runs inside Mistral Vibe, the same agent interface Mistral offers for ordinary software work. According to Mistral’s technical report, the model edits files, runs shell commands, reads Lean compiler and language-server feedback, and compacts its own context to keep working across long sessions. When a run outgrows the context window, it summarizes earlier work and continues, preserving the original task so it does not drift after many rounds of compaction.
The design choice Mistral emphasizes is what it left out. Rather than wrapping the model in a specialized prover scaffold, it trains and runs the model as a general code agent that scales by running longer. In the report’s framing, a user can point Leanstral at a repository much as they would a general coding assistant, while getting a model tuned for Lean.
Two roles should stay distinct. Leanstral generates and edits the Lean proof. The Lean kernel and Mistral’s fork of a tool called SafeVerify do the checking. The model proposing a proof and the system confirming it are separate steps, and the trust in a result comes from the second, not the first.
Hosted, self-hosted, or skip
Mistral offers Leanstral 1.5 through two routes, and they solve different buyer problems. Treating them as interchangeable versions of one free offer is the most common mistake.
| Route | What you get | What you still own |
|---|---|---|
| Hosted Labs | A model priced at $0 and a low-friction way to evaluate Leanstral through Mistral’s API and Vibe tooling | Preview lifecycle, account-level rate limits, a data-use review, proof-search latency, and migration before the endpoint retires |
| Self-hosted weights | Downloadable Apache-2.0 weights and less dependence on the hosted endpoint | Serving hardware, model operations, upgrades, security, and the full cost of long-running inference |
| Do not adopt | No new infrastructure or formal-methods burden | No access to Leanstral’s specialized proof search |
The hosted route is an evaluation path, not a production entitlement. Mistral’s documentation labels Labs models experimental, states they may change or be removed with two weeks’ notice, and says the company does not recommend them for production. Mistral’s Labs listing gives labs-leanstral-1-5 a retirement date of September 30, 2026. Free-tier API limits are also the provider’s lowest and are intended for testing and prototyping; the exact limits are set at the organization and model level rather than published as a universal quota.
The data boundary matters more than the draft price, and here the documentation is direct rather than ambiguous. Mistral’s privacy and data-controls documentation states that enabling Labs models allows data to be used to train Mistral models, regardless of subscription plan or opt-out settings. That is a deliberate exception. Mistral’s general API is not used for training, and paid plans are opted out by default, but the Labs setting overrides both. Mistral’s stronger control, Zero Data Retention, is offered only on the Scale plan and only for stateless API calls, and the public documentation does not say it overrides the Labs training rule. A team weighing whether to send proprietary theorems, unpublished mathematics, or customer code through the hosted endpoint therefore faces a procurement question before a benchmark one.
Self-hosting removes the retirement and data-training problems, but it does not establish a cheap deployment profile. Mistral’s example vLLM configuration uses four-way tensor parallelism and caps the model length at 200,000 tokens. That is a reference configuration, not a published minimum hardware requirement. The responsible reading is that local deployment is supported while the true hardware and total operating cost remain unproven in the current materials.
What a checked proof does not guarantee
Lean’s kernel can establish that a proof follows from a formal statement and its assumptions. It cannot establish that the statement expresses the behavior you intended, covers every relevant execution path, or models the outside system correctly. This gap sits upstream of the proof, and it is where verification projects usually fail.
Mistral’s own bug-finding pipeline makes the gap visible, and this briefing keeps the full funnel rather than the headline. Mistral reports that its automated pipeline translated 57 repositories, generated candidate properties, and produced proofs that 47 of those properties do not hold for the translated code. Mistral then classified 11 of those as genuine bug signals and, after collapsing shared root causes, reported five distinct bugs, all previously unreported. The reduction from 47 machine-checked counterexamples to five reported bugs is not a failure of the checker. It shows that when a machine writes the specification, deciding which specifications are worth trusting becomes the new bottleneck. Mistral notes the discarded flags were properties that were too strong, unreachable from a public interface, or malformed.
The report is also candid about how much this proves. It states that a rigorous comparison against testing, fuzzing, or asking a general model to find bugs is future work. In a footnote, it records that Claude, given the same repository, also found the flagship bug. Leanstral’s demonstrated contribution is narrower than “formal methods beat testing.” Mistral showed an automated pipeline that can produce machine-checkable counterexamples for translated code and surface a small number of plausible bugs for human review.
The Rust pipeline is narrower than the headline
For software, Leanstral does not read your source directly. In Mistral’s experiment, a separate tool, Aeneas, translated Rust into Lean first, and Aeneas defines the edge of what can enter the pipeline. Per the Aeneas documentation, it functionalizes only a subset of safe Rust. Unsafe code and concurrency are outside its supported path, that work is described as in progress, and some control flow such as returning from inside nested loops or breaking to an outer loop is not yet handled. Code that depends on external libraries can require the user to supply hand-written Lean models of those dependencies. Much of what makes real production code hard, unsafe blocks, concurrency, and heavy external dependencies, sits outside the supported path today.
SafeVerify narrows the trust claim again, and its own documentation is specific about its limits. Mistral’s fork re-checks every declaration through Lean’s kernel using Environment.replay, confirms the submission only relies on the three standard axioms (propext, Quot.sound, Classical.choice), and rejects any declaration marked partial or unsafe. Its documentation also states what it does not do: it does not replay imports by default, and constructs such as implemented_by, extern, and noncomputable are hard to catch at the level it works in and may need a separate source-level scan. SafeVerify strengthens assurance around a submitted Lean proof. It does not certify that a real-world software specification is complete.
The buyer conclusion is direct. Leanstral produces proof artifacts inside a larger verification system. It does not, by itself, choose the right property, guarantee the translation covered the program, or replace human review of what “correct” means.
Reading the benchmarks
Leanstral 1.5’s results are strong and specific, and they hold only with their conditions attached. All figures below are from Mistral’s technical report.
| Benchmark | Leanstral 1.5 | Setting | The caveat | Why a buyer cares |
|---|---|---|---|---|
| miniF2F | 244/244 valid, 242/244 test | pass@4, 2M tokens | Mistral calls this saturation, but the initial test run was 242/244; the last two problems fell only on extra attempts, one after 37 | Strong Olympiad-level formal math, not a single clean pass |
| PutnamBench | 587/672 | pass@8, 4M tokens | A closed system (Aleph) solves 668; an open one (Goedel-Architect) solves 597 with natural-language guidance | Not the highest or cheapest entry |
| FATE-H / FATE-X | 87% / 34% | pass@8 | Scoped to systems without natural-language proof access; general reasoners run at pass@64 and score near 0% at these tiers | A genuine lead on hard formal algebra within its class |
| FLTEval | 43.2% | pass@8 | Compared to Claude Opus 4.6 at pass@1, in a different harness (Vibe versus Claude Code) | Efficient on real repository PRs, not a like-for-like win over Claude |
| ArXivLean | 17.1% (7/41) | reported | Aleph tops the board at 34.2% | An honest ceiling on cutting-edge research math |
The cost figures carry one warning. Mistral’s blog cites “about $4 per problem” for PutnamBench, while the technical report’s own table lists $1.68. Both are Mistral’s numbers, both depend on undisclosed assumptions about tokens, hardware, and retries, and neither is an independently verified operating cost. Read them as vendor estimates, not as your bill.
Where Leanstral leads, and where it does not
The PutnamBench leaderboard in Mistral’s report is the clearest picture of the field. It shows Leanstral is neither the strongest nor the cheapest, and clarifies the claim it can actually defend.
| System | Solved (of 672) | Cost per problem (reported) | Openness |
|---|---|---|---|
| Aleph Prover (high) | 668 | $68 | Closed |
| Goedel-Architect (with NL guidance) | 597 | $1.47 | Partial |
| Leanstral 1.5 | 587 | $1.68 | Fully open |
| Seed-Prover 1.5 (high) | 581 | ~$240 (estimated) | See note |
| Goedel-Architect (without NL guidance) | 508 | $0.44 | Partial |
| Aleph Prover (low) | 500 | $23 | Closed |
| AxProverBase | 365 | $12.60 | Partial |
Source: Mistral technical report, PutnamBench leaderboard (abridged). The Seed-Prover figure is Mistral’s estimate, based on $1/hour for the reported 10 H20-days-per-problem budget. Openness labels follow the leaderboard’s own classification. Costs are vendor-reported.
Read against its alternatives: a closed system, Aleph Prover, leads on raw capability at much higher cost; one open competitor is cheaper in a lower-scoring configuration; and Leanstral posts a strong score-to-cost balance among the systems the leaderboard classifies as fully open-source, using a general agent interface rather than a specialized prover. On the hardest FATE algebra tiers, within the class of systems that do not receive natural-language proof guidance, it leads. Those are meaningful, bounded claims. “Best theorem prover” and “cheapest” are not among them.
FAQ
Is Leanstral 1.5 free?
Access is. The weights are Apache-2.0, and the hosted Labs endpoint lists a price of zero. Operation is a different matter: running the weights means paying for substantial compute, and the free endpoint is an expiring preview. Free access does not equal free operation.
Can it be used in production?
The hosted route is not built for it. Mistral classifies Labs models as experimental, does not recommend them for production, and can remove them with two weeks’ notice; the endpoint carries a listed retirement of September 30, 2026. The open weights can be self-hosted, which moves operation and cost to you.
Can I send private or customer code to the free API?
Only after a governance review. Mistral’s documentation states that enabling Labs models allows data to be used to train Mistral models, regardless of plan or opt-out settings. Zero Data Retention is limited to the Scale plan and stateless calls. Confirm the current terms before sending anything sensitive.
Can it verify arbitrary Rust?
No. Rust is first translated to Lean by a separate tool, Aeneas, which supports only a subset of safe Rust and does not handle unsafe code or concurrency. Code outside that subset cannot enter the pipeline. Mistral’s software evidence is two case studies and one pilot, not independently reproduced.
Is it the best Lean 4 prover?
Not outright. On PutnamBench a closed system (Aleph Prover) solves more, and one open competitor solves more with guidance. Leanstral’s defensible claim is a strong score-to-cost balance among fully open systems using a general agent interface, plus a lead on the hardest FATE tiers within its class.
Methodology and sources
This is a Tier C document-first briefing. Future Stack Reviews did not install, run, benchmark, or purchase Leanstral 1.5, and claims no hands-on testing. Figures are vendor-reported unless stated, and benchmark and bug-finding results have not been independently reproduced. The bug counts, the per-problem costs, and the five reported bugs are Mistral’s own classifications and have not been confirmed by third parties.
Primary sources read on July 14, 2026:
- Mistral technical report, Leanstral (hosted on Mistral’s GitHub; carries an arXiv submission stamp dated July 2, 2026):
github.com/mistralai/LeanstralSafeVerify/blob/main/LeanstralReport.pdf - Announcement, Leanstral 1.5: Proof Abundance for All:
mistral.ai/news/leanstral-1-5/ - Mistral docs model card (Leanstral 1.5) and March predecessor
- Mistral docs, Labs policy:
docs.mistral.ai/models/labs - Mistral docs, Privacy and data controls:
docs.mistral.ai/admin/monitor-comply/privacy-data-controls - Mistral Help Center, Zero Data Retention scope
- Aeneas documentation:
github.com/AeneasVerif/aeneas - SafeVerify (Leanstral fork) documentation:
github.com/mistralai/LeanstralSafeVerify
Not confirmed, and treated as open questions rather than facts: account-specific hosted rate limits and any service-level commitment; minimum hardware, memory, and total cost to self-host; independent reproduction of the benchmark scores or the five bugs; and benchmark decontamination. The retirement date reflects Mistral’s Labs listing at the time of writing. Pricing, Labs status, retirement, and the model identifier are volatile and should be re-checked before any decision.
Verdict
Leanstral 1.5 is a serious open release for proof engineering. For a team already working in Lean 4, it lowers the cost of long, mechanical proof search in a way that matters, its mathematics results are strong when read with their conditions attached, and its bug-finding pipeline is a substantive demonstration. Mistral describes that pipeline as, to its knowledge, the first to apply automated deductive verification at scale without a human in the loop; independent evaluation has not yet tested that claim.
The buyer decision is narrower than the launch coverage suggests. The model is free. The verification system around it is not: specification design, translation coverage, verifier scope, compute, Lean expertise, and the lifecycle and data terms of a preview endpoint all remain yours to manage. For a Lean-native research or proof-engineering team, that is a worthwhile trade and a strong candidate for evaluation. For an ordinary software organization hoping to drop in an AI that verifies its code, this is not that product yet.