<p>Mistral has released <a href="https://mistral.ai/news/leanstral" target="_blank" rel="noopener nofollow">Leanstral</a>, an open-source coding agent built specifically for Lean 4, a formal proof assistant language. The idea is straightforward: instead of hoping AI-generated code is correct, you ground it in formal proofs and specifications that can actually be verified.</p>
<h2>What it is</h2>
<p>Leanstral-120B-A6B uses a sparse mixture-of-experts architecture with only 6 billion active parameters. Despite that relatively lean footprint, Mistral claims it outperforms much larger open-source models on the FLTEval benchmark — including Qwen3.5-397B and Kimi-K2.5-1T — and beats Anthropic’s Claude Sonnet on the same benchmark at a fraction of the cost. A pass@2 run costs around $36 with Leanstral versus $549 with Claude Sonnet.</p>
<p>The FLTEval benchmark is based on the Fermat’s Last Theorem (FLT) project, a large real-world Lean codebase, which makes it a more realistic test than synthetic benchmarks.</p>
<h2>What it can do</h2>
<p>In practice, Leanstral handles the kinds of tasks that come up in real proof engineering work:</p>
<ul>
<li>Diagnosing and fixing issues when migrating code between Lean versions</li>
<li>Translating program properties defined in Rocq (formerly Coq) into Lean 4 and generating proofs</li>
<li>Writing and verifying formal proofs in realistic codebases</li>
</ul>
<p>It supports MCP (Model Context Protocol) integration, so it can plug into existing tooling.</p>
<h2>How to access it</h2>
<p>Mistral is making Leanstral available in a few ways:</p>
<ul>
<li><strong>Mistral Vibe</strong> — a no-setup web interface for trying it immediately</li>
<li><strong>Free API endpoint</strong> — for building on top of it</li>
<li><strong>Apache 2.0 weights</strong> — for self-hosting</li>
</ul>
<p>Mistral also released Mistral Small 4 alongside this, a general-purpose model covering reasoning, coding, and chat.</p>
<h2>Why it matters</h2>
<p>Formal verification has always been the gap between “the code looks right” and “the code is provably correct.” The tooling has historically been expensive, slow, and required deep expertise in proof assistants. If an agent can handle the mechanical parts of writing and checking Lean proofs at this cost point, it makes formal verification accessible to teams that would have skipped it entirely. Whether Leanstral holds up on real production codebases beyond the benchmark is still an open question, but the cost comparison alone is hard to ignore.</p>


Collections

Mistral has released Leanstral, an open-source AI coding agent designed for Lean 4, a formal proof assistant language. The model uses a sparse mixture-of-experts architecture with only 6B active parameters but claims to outperform much larger models like Qwen3.5-397B and Kimi-K2.5-1T on the FLTEval benchmark, and beats Claude Sonnet at roughly 1/15th the cost ($36 vs $549 for a pass@2 run). Leanstral handles real proof engineering tasks including migrating code between Lean versions, translating Rocq/Coq properties into Lean 4, and writing and verifying formal proofs. It supports MCP integration and is available via a web interface, free API, and Apache 2.0 weights for self-hosting. The release also includes Mistral Small 4, a general-purpose model. The key promise is making formal verification accessible to teams that previously couldn't afford the expertise or tooling costs.

Mistral releases Leanstral, a formal code verification agent for Lean 4