Mistral Release Notes

Regional control, production-grade reliability

Mistral is advancing AI sovereignty by offering enterprises and countries control over AI models, infrastructure, and compute capacity, ensuring regional compliance and reliability. The company is expanding open model access, introducing regional endpoints and priority tiers, and forming a coalition to secure long-term European AI compute capacity. With plans to build up to 1 GW of capacity by 2030, Mistral aims to provide a scalable, sovereign AI infrastructure that retains value and control for users.

At Mistral, we believe every enterprise and country must be in control of the models it uses, choose where the intelligence runs, control the compute capacity to scale it, and retain its compounding value.

Today, we are taking three concrete steps as we build the foundations of our customers' AI sovereignty: strengthening the reliability and regional control of inference, expanding access to third-party open models within that infrastructure, and bringing together enterprises and institutions to secure long-term commitments for compute capacity in Europe.

Most of our customers run our models inside their own data centers and cloud environments today. As AI becomes more deeply embedded in production, they need confidence that the underlying capacity will remain available, resilient, and under the regional controls their workloads require. For some, that means complementing infrastructure they manage themselves with capacity provided and operated by Mistral.

At the inference layer, that means two things: keeping data and processing in-region, and having dependable access to capacity when demand peaks. We are strengthening both.

Mistral Regional Endpoints, now generally available, let customers choose whether their inference runs in Europe or the US, helping them align inference location with their data-residency, regulatory, and latency requirements. Inference and the associated processing take place in the selected region, subject to limited, safeguarded transfers to sub-processors that may occur outside that region, as described in our Trust Center. Our new Mistral Priority Tier, now in public preview, provides committed service levels for mission-critical workloads, including custom rate limits, and is backed by an uptime SLA. Mistral is the only European AI lab to offer both: choice of processing region and a committed, SLA-backed service level.

Of course Mistral models will continue to be available through partners, as well - you can learn more about our close partnerships here.

Sovereign intelligence, built on open model choice

Control over where AI runs, however, is only one part of AI sovereignty. Customers also need control over the intelligence they choose to run on that infrastructure. Today’s AI systems are no longer built on a single model but on an ensemble of capabilities: extended reasoning, high-volume production, or work shaped around a company's own data. Mistral builds for each, from frontier models to specialist ones like Mistral OCR and Voxtral to custom models trained on a company's own knowledge.

Our customers particularly value us for pioneering open models. Open weights give them what mission-critical work demands: the ability to see inside a model, adapt it, and retain the intelligence they build with it. This is why we are enthusiastic contributors to the Open Secure AI Alliance and NVIDIA Nemotron Coalition. We are now extending that openness beyond our own models. Mistral’s platform will support third-party open models, starting with Z.ai’s GLM-5.2. This and future open models will run on the same infrastructure, regional controls, and service commitments as Mistral models, so customers can broaden model choice without fragmenting where their AI runs.

"Different workloads need different models, and that will keep changing as the frontier evolves. Mistral allows us to run open models under strict regional controls and service commitments, making it easy for us to maintain data residency and compliance requirements while furthering our commitment to open source"

Matan Grinberg, CEO and cofounder of Factory

A coalition that secures long-term AI capacity

Open intelligence is inseparable from the compute beneath it. And without assured access to that compute, Europe cannot control the AI systems on which its industries, institutions, and future competitiveness will depend. Capacity is increasingly strategic, yet remains scarce, fragmented, and difficult to secure.

Mistral is bringing together an anchor group of enterprises whose multi-year commitments can support infrastructure in Europe at a scale no participant could secure alone. Aggregating long-term demand in this way will help determine what capacity is built, where it is located, and whom it serves. European Compute Units, or ECUs, convert those commitments into access to Mistral-built infrastructure over multiple years. Participants can use that capacity across the range of products available on Mistral Compute as their needs evolve.

"As the neutral execution layer and trusted system of record at the core of the global travel industry, Amadeus bridges raw foundational data with modern Agentic AI to improve the traveller experience for everyone everywhere. In an AI-driven world, capacity, deployment control, and operating continuity become increasingly important for all enterprises. Equally crucial, at the same time, is ensuring businesses have the confidence to make long-horizon commitments at scale; something that Mistral’s massive compute undertaking supports."

Luis Maroto, CEO of Amadeus

"Few industrial endeavors will matter more to Europe’s next generation than building the capacity to develop and run AI on its own terms. Mistral is taking on that challenge with the scale, ambition, and staying power it demands, giving enterprises the confidence to build their most consequential workloads on that foundation."

Christophe Fouquet, CEO of ASML

"Building AI capacity isn't just a technology question - it's a question of who shapes the future of European industry. This program is about giving our clients the compute, the partnerships, and the confidence to run their most critical AI workloads on infrastructure built for scale and built to last."

Aiman Ezzat, CEO, Capgemini

"Europe needs sovereign infrastructure to ensure its technological independence. Mistral embodies this ambition by providing a robust, scalable platform aligned with our values, enabling businesses to deploy critical solutions with confidence. Innovating without relying on foreign actors is an imperative for Europe. With Mistral Compute, we now have a European neocloud capable of competing on a global scale while retaining control over our data and models. The IRN (Digital Resilience Index) will further help businesses measure their digital dependence. This is a major breakthrough for our ecosystem."

Olivier Sichel, CEO of Caisse des Dépôts

"AI is the industrial revolution of our time, including for non-tech companies like CMA CGM, a global Group active in shipping, logistics and media. We chose Mistral for its world-class technology, its ability to co-develop robust and resilient solutions tailored to our operational needs and to efficiently deploy them at scale. That deployment is already under way among thousands of employees and across geographies. It is transforming areas such as customer care to improve quality, responsiveness and reliability for our customers."

Rodolphe Saadé, Chairman and CEO of CMA CGM

A framework for advancing AI sovereignty

Europe is the place where this framework begins, but the same challenge exists everywhere: organizations and governments need to harness the power of frontier AI for their mission-critical needs without surrendering control over the infrastructure and intelligence loop.

The path will differ by region, but the foundations are the same: operational control, choice of intelligence, and assured access to compute. Europe can show how these elements come together to create an AI ecosystem that remains open to global innovation while preserving institutional autonomy.

That is the model Mistral is building toward: one in which enterprises, public institutions, and startups can use the best AI available, shape it around their own knowledge, and retain the value it creates.

Shieldstral introduces a 3B open-weights multimodal safety classifier that outperforms models up to 7x its size by framing content moderation as a policy-adaptive question-answering task.

Unlike traditional guardrail models, it accepts plain-language policies at inference time, unifying text and image safety evaluation without retraining. Released under Apache 2.0, it delivers calibrated safety scores across diverse benchmarks while running efficiently on a single 16GB NVIDIA GPU.

A 3B open-weights, policy-adaptive multimodal safety classifier that matches models up to 7x its size on text safety and sets a new state of the art on multimodal moderation.

“Does this content promote violence against a protected group? Is this image safe to show to a minor? Did the assistant refuse the request?”

Every product that ships a model needs to answer questions like these — but the right answer depends on the product, the audience, and the moment. The same content can be fine for a cybersecurity research tool and harmful on a mental-health platform. Most guardrail models bake a fixed taxonomy of harm categories into their weights, so re-targeting them to a new deployment context means retraining. And because safety definitions differ across applications and domains, there is no single "correct" set of categories to model in the first place.

Shieldstral takes a different approach: you write the policy as a plain-language question at inference time, and the model returns a calibrated safety score. No retraining, one interface for text and images, and a verdict from a single token. Please refer to our technical report here.

As an inaugural member of the Open Secure AI Alliance with NVIDIA and other organizations, today we're releasing Shieldstral as open weights under Apache 2.0, available for download here.

Moderation as a question

Shieldstral frames content moderation as a binary question-answering task. Each request has three parts:

• — the evaluation context, strictness, and (optionally) a definition of what counts as unsafe content.
• — a single yes/no question, e.g. "Does this content promote physical violence?"
• — the content to judge: a prompt, a response, a prompt–response pair, or an image with optional text.

At inference the model reads out only the yes and no logits and softmax-normalizes them into a continuous safety score. This one simple formulation does a lot of work: it unifies prompt classification, response moderation, refusal detection, and toxicity detection into a single problem; it lets policies live entirely in the prompt, so one checkpoint adapts to novel policies at deployment time.

Highlights

• Strong performance — matches or outperforms open guard models up to 7× its size across text safety, refusal detection, policy adaptability, and multimodal benchmarks.
• Adaptive and flexible — a single natural-language interface covers text, image, and text+image content across prompts, responses, and prompt–response pairs. Policies are supplied as free-form queries and re-targeted at inference time, without retraining.
• Small, trained on heterogeneous sources — a 3B model that runs on a single 16GB GPU, trained on real and synthetic data with diverse label formats and taxonomies, consolidated into one framework.
• Continuous safety score — returns a calibrated yes/no probability from a single forward pass, so you can threshold or rank by confidence rather than relying on a discrete label.
• Open — Apache 2.0 weights.

Benchmarks

We evaluate Shieldstral against open guard models up to 7x its size across four axes. All evaluation samples are held out from training.

Text safety

Refusal detection

Policy adaptability

Multimodal safety

How we built it

The core idea is that a small model can beat much larger ones if the data is right. Getting the data right meant solving four problems:

Unify heterogeneous data.

Public safety datasets disagree on taxonomies, labels, and annotation conventions — from binary safe/unsafe flags to fine-grained multi-label taxonomies. We convert every dataset into the same instruction–query–document format with a per-dataset processor, and we vary the wording of instructions, queries, and prompt–response delimiters so the model generalizes across phrasing instead of overfitting to one style. We also calibrate strictness per source — strict for adversarial jailbreaks, lenient for response-quality data — so the model learns calibrated decision boundaries. This lets us consolidate sources that would otherwise be incompatible.

Teach discrimination, not memorization.

If trained on a fixed set of policy labels, a model learns only to classify those predefined policies, rather than reasoning about the precise boundaries of a given policy. This prevents generalization to novel policies. Instead, we construct sets of deliberately similar, easily confused policies and ask an LLM to rewrite safe text into contrastive pairs: each rewrite is engineered to violate one policy but not its sibling. This trains the model to distinguish which specific policy a piece of content violates, a skill that transfers to unseen, user-defined policies at inference time.

Ground safety in images.

Unsafe images can't be synthezised by an LLM the way text can, so visual safety data is scarce. We supplement limited moderation datasets with general-purpose image datasets as high-quality negatives, mutate queries to augment the dataset, and filter every image–query pair through a vision–language reranker to reduce mislabeled data and hallucinations.

Combine complementary checkpoints.

We fine-tune with LoRA and merge — via SLERP — a checkpoint calibrated on public data, one that adds fine-grained policy discrimination from generated data, and the base instruct model. The merge recovers common policy calibration and policy adaptability in a single model, and instruction-following from the base model transfers to the moderation task.

Forge.

We built Shieldstral end to end on Forge, our platform for training, aligning, and evaluating custom models. Forge managed the infrastructure, data and model sharding, metrics, and logging on top of state-of-the-art distributed training, so the team could stay focused on the data which is what determines the safety model's quality.

What's next

Shieldstral is a step toward moderation that adapts to context instead of forcing every product through one frozen taxonomy. We're continuing to push on multilingual coverage, longer-document robustness, and broader multimodal safety — and we'd love to see what the community builds on top of it.

BTW, we're hiring! If you want to help make AI better, see our careers page.

What's Changed

• Update AGENTS.md structure and add explicit keyword args rule by @juliendenize in #270
• Validate special_token_policy strings when decoding by @sarathfrancis90 in #273
• Add auto-detecting chat template generation from tokenizer file by @juliendenize in #272
• Reject thinking chunks in tool messages by @juliendenize in #275
• Emit all render_content macro args explicitly by @juliendenize in #274
• Fix documentation drift from code by @juliendenize in #276
• Bump version to 1.11.7 by @juliendenize in #277

Full Changelog: v1.11.6...v1.11.7

What's Changed

• Raise ValueError instead of ValidationError in audio chunk validators by @sarathfrancis90 in #255
• Reject AudioConfig with sampling_rate < frame_rate instead of a later ZeroDivisionError by @CharlesCNorton in #253
• Decode normal tokens under SpecialTokenPolicy.RAISE in SentencePiece by @sarathfrancis90 in #256
• Auto-select grammar variant from tokenizer by @juliendenize in #260
• Fix seed field not bridged in SpeechRequest OpenAI conversion by @winklemad in #262
• Restore deprecated reasoning parameter in select_jinja_template by @juliendenize in #266
• Bump version to 1.11.6 by @juliendenize in #267

New Contributors

• @winklemad made their first contribution in #262

Full Changelog: v1.11.5...v1.11.6

Most enterprises struggle with unmanaged, scattered AI prompts and skills, leading to inconsistent behavior and untraceable issues.

Studio provides a centralized system of record for versioning, ownership, and traceability, enabling fast iteration and controlled deployment while maintaining compliance. By treating prompts as production assets with immutable versions, clear ownership, and audit logs, Studio ensures AI behavior is governed, discoverable, and aligned with business policies.

Most enterprises can't say which version of a prompt is running in their AI right now. The instructions that decide how that AI behaves get scattered the moment more than one team touches them, leading to an inconsistent experience for users and an untraceable problem for teams.

As of today, Studio gives your Prompts and Skills a system of record: a single place where each one is versioned, owned, and traceable.

Prompts and skills outgrew the way they're managed

Prompts and Skills are production assets. They hold the business logic, the tone, and the policy your AI follows when it answers a customer or makes a call. What your AI does in front of a customer comes down to the prompts and skills in use. When that behaviour is wrong, the fix has to ship as fast as any production incident, not wait for the next code release.

And in most enterprises, they're managed like scratch notes. Prompts started as quick experiments, then they shipped. Now they sit in code repos, notebooks, and Slack threads, with no clear owner and no shared history. Skills get rebuilt, or forked by one team because they lacked visibility to another team’s version.

In many enterprises, prompts already live in version-controlled code, which means tracking changes was never the hard part. The friction is elsewhere. The people who understand the instructions best, the line-of-business teams who set the policy and the wording, don't work in the codebase, so every change waits on an engineer. And refining an instruction takes iteration and testing, which a codebase makes expensive: one version ships at a time, and every attempt means editing code and waiting for a deploy.

So most teams stop iterating early. They ship a version that's good enough and then may leave it, and the instructions that shape every customer answer can stay well short of what they could be.

Iterate fast, ship with control

While you're building, iterating on an instruction should be quick. In code, even a one-line change to a prompt can mean waiting on a CI run before you see how it behaves. Studio lets any AI builder, developer or not, edit a prompt or skill and test it right away, without a pipeline run for every attempt.

Shipping to production is different, and it should be. A change bound for production goes through the tests and approvals your enterprise already requires. What changes is who can drive it. A domain expert or line-of-business owner can improve a production instruction the same way a developer would, and the promotion using simple labels still triggers your CI/CD, for example through the SDK in a GitHub Actions workflow. The people closest to the work improve the behaviour, inside the controls you already run.

Because every asset is governed and discoverable, good work spreads instead of getting rebuilt. Anything in a workspace is available to that whole team today, so a prompt one person gets right is usable by their colleagues at once.

A system of record for AI behavior.

Studio treats every prompt and skill as a tracked, versioned asset with an owner, a full history, and a lineage.

• Immutable versions. Every version is recorded and fixed. A version that shipped can't be quietly changed after the fact, so the record always matches what ran.
• Rollback. Compare any two versions, see exactly what changed, and revert to a known-good version in minutes.
• Clear ownership. Every asset has a named owner, so there's always an audit trail to track changes.
• Classification labels. Helps call or find the right prompts and skills by their labels easily (e.g. “Production” vs “Staging”).
• Audit logs. Each change is logged with who made it and when. The trail an auditor will ask for exists by default.

The part a standalone catalog can't do.

A separate prompt tool can list your assets. It can't tell you whether they work, because it sits outside the system that runs them.

Because your prompts and skills live where your AI runs, Studio can connect them to how it actually behaves. Through Observability, lineage and telemetry trace a production output back to the version of the asset behind it, and back to the usage that prompted the last change. The skills your agents run are reachable as MCP servers straight from Studio, so what executes in production is the same governed asset you versioned, not a copy that drifted. You define behaviour, watch it run, and improve it, all against one source of truth. That closed loop is the difference between cataloging your AI and governing it.

Control for the people who answer to auditors.

Ungoverned prompts are a liability for the people who answer to auditors. They embed data-handling rules and policy decisions someone will eventually have to defend, and today they often live where no compliance team can see them.

Studio changes the default. Every asset moves through a clear path to production, from a staging version to a tagged production version, so shipping a change is deliberate rather than accidental.

An asset starts as visible only to its creator, then when appropriate can be promoted to the workspace and, in time, across the organisation, with control over who can use it at each step. Across every deployment mode, your data stays inside your perimeter.

Available now in Studio.

Prompts and skills are available to Mistral Studio customers today. If you run AI in production, Studio turns scattered prompts and skills into governed assets you can trust.

Read documentation:

• Create reusable prompts in Studio
• Create reusable skills in Studio

Or explore Prompts and Skills in Studio.

Robostral Navigate is an 8B model that enables robots to autonomously navigate complex environments using only a single RGB camera, achieving 76.6% success on unseen R2R-CE benchmarks—outperforming multi-sensor approaches while being more efficient. Built entirely in-house with simulated data and token-efficient techniques, it generalizes across robot types and adapts to real-world obstacles unseen during training. The model combines pointing-based navigation with reinforcement learning for continuous improvement, paving the way for unified embodied AI in robotics.

Today we're introducing Robostral Navigate, our first model built for embodied navigation. It's an 8B model that takes RGB images and a plain-language instruction and moves a robot through an environment:

“Leave the lobby, walk through the corridor, enter the supply room, and stop to face the second shelf.”

To perform such tasks, other models often employ depth sensors, LiDAR, or several cameras working together. Robostral Navigate uses only one ordinary RGB camera and no depth sensors, yet still achieves 76.6% on R2R-CE (Room-to-Room in Continuous Environments) validation unseen, the benchmark for following instructions in environments held out of training. Consequently, it beats the best single-camera approach by 9.7 points and the best system using depth or multiple cameras by 4.5 points, despite using neither.

Navigation

Our model is designed for robotic navigation, enabling robots to autonomously navigate complex environments, including offices, residential and commercial buildings, and outdoor settings.

Robostral Navigate running fully autonomously in one long-horizon instruction route through a working office.

This technology unlocks numerous applications across manufacturing, delivery, logistics, and hospitality, making it one of the most in-demand capabilities for our customers today. Give Robostral Navigate one instruction and it completes the entire task on its own, moving through a live space full of people and obstacles it was never shown, capable of adapting to any setting.

Highlights

• State-of-the-art performance on R2R-CE
  • 79.4% Success Rate on validation seen
  • 76.6% Success Rate on validation unseen
• Operates from a single RGB camera, with no LiDAR or depth sensors
• 8B model, built in-house and trained entirely in simulation
• Runs on wheeled, legged, and flying robots, and generalizes across robot sizes
• Robust to differences in camera intrinsics
• Token-efficient training via prefix-caching

Navigation via pointing

Given a task and a history of observations, Robostral Navigate predicts where the robot should move next via pointing: it infers the image coordinates of the target location in the robot's current camera view, together with the desired orientation upon arrival. Unlike commands relying on metric displacements, pointing makes the policy naturally robust to changes in camera intrinsics and world scale.

However, this method cannot handle cases where the target location lies outside the current field of view. When pointing does not apply, the model falls back to displacements in the robot's local coordinate frame, such as:

"Move 2 meters forward, 1.5 meters to the left, and turn 25 degrees left."

Built from the ground up

Robostral Navigate is built entirely in-house and does not rely on existing open-source VLMs.

The model is initialized from our vision-language model specialized for grounding tasks such as pointing, counting, and object localization. Navigation emerges as a natural extension of these capabilities: once it understands where things are, it learns how to move.

We built an efficient data generation pipeline entirely in simulation. This enabled rapid iteration on the data, resulting in a dataset of approximately 400,000 trajectories collected across 6,000 scenes.

Efficient supervised training

A key ingredient of Robostral Navigate is an efficient training algorithm based on prefix-caching. Using a tree-based attention-masking strategy, our method compresses an entire episode into a single sequence, enabling training on all time steps in a single forward pass while preventing information leakage between time steps.

Compared to training with one sample per time step, our approach reduces the number of training tokens by 22× while preserving all of the learning signals. In practice, this method transforms training runs that would take months into runs that complete in days.

Online reinforcement learning

We leverage our knowledge of post-training LLMs at scale, using online reinforcement learning, to boost the performance of Robostral Navigate. After the supervised training stage, we further improve the model's performance using CISPO, an online reinforcement learning algorithm. This enables the model to learn from trial and error, recover from failures, and acquire exploratory behaviors, effectively mitigating the distribution shift issue of vanilla behavior cloning. This alone improved the success rate by 3.2%. We are not seeing any plateauing, so we are confident that more training and more experiments will continue to push this number up.

What's Next

Robostral Navigate is only the first step toward a unified embodied agent.

We believe navigation is a foundational capability for general-purpose robotics. By combining large-scale simulation, efficient training, and strong grounding priors, Robostral Navigate demonstrates that state-of-the-art embodied navigation can be achieved with a compact model and a single RGB camera.

Start your journey to embodied frontier AI, talk with our team.

BTW, we're hiring!

The release of our navigation models marks a significant step forward, but our journey is far from over. Our ambition is to enable robots to autonomously navigate complex environments—offices, homes, commercial buildings, and outdoor spaces—and there's a lot more work to do. We are actively expanding our robotics team and looking for talented research scientists and engineers who share our ambition.

If you're interested in joining us on our mission to bring seamless navigation to robots everywhere, we welcome your applications to join our team!

By Théo Cachet, Arjun Majumdar, Srijan Mishra, Thomas Chabal, Chris Bamford, Elliot Chane-Sane, Benjamin Tibi, Ludovic Ho Fuh, Olivier Duchenne - AI Science Robotics

Leanstral 1.5

Leanstral 1.5, a free Apache-2.0 licensed model with 6B active parameters, delivers a major performance upgrade in formal verification, saturating miniF2F, solving 587/672 PutnamBench problems, and achieving state-of-the-art results on FATE-H (87%) and FATE-X (34%). Trained through mid-training, supervised fine-tuning, and reinforcement learning with CISPO, it excels in agentic proof engineering and real-world code verification, uncovering 5 previously unknown bugs across 57 repositories tested. Fully open-sourced and available via Hugging Face and a free API, Leanstral 1.5 is now accessible for practical proof engineering in Lean 4.

Since its launch, Leanstral has offered an open, practical approach to proof engineering in Lean 4. Today, we are releasing Leanstral 1.5, a free Apache-2.0 licensed model with 119B total and only 6B active parameters, delivering a performance upgrade that makes formal verification more powerful and accessible than ever.

Leanstral 1.5 saturates miniF2F, solves 587/672 PutnamBench problems, and achieves a new state-of-the-art of 87% on FATE-H and 34% on FATE-X. Beyond benchmarks, it verifies complex code properties and uncovers previously unknown bugs in open-source repositories—proving that rigorous formal methods can be both effective and practical for real-world use.

Training Leanstral

Leanstral 1.5 goes through a three-stage process: mid-training, supervised fine-tuning, and reinforcement learning with CISPO. Leanstral 1.5 leverages extensive training on two RL environments:

In the multiturn environment, the model is given a theorem statement and must either prove or disprove it. The model submits a proof, receives Lean compiler feedback, and refines its approach with each attempt. If the proof compiles it succeeds; otherwise the loop continues until the model either solves the problem or exhausts its budget.

In the code agent environment, Leanstral operates like a developer in a raw filesystem: it edits files, runs bash commands, and uses the Lean language server to inspect goals, errors, and type information in real time. This allows it to tackle long-horizon tasks like completing partial proofs in a repository, building auxiliary lemmas, and persisting through multiple rounds of context compaction. The model learns to navigate the full proof-engineering workflow and is finally verified by our fork of SafeVerify for correctness given a list of target theorems.

Evaluation

We evaluate Leanstral on the following benchmarks:

• miniF2F is a cross-system benchmark for formal mathematics, ranging from elementary problems to IMO-level challenges, testing diverse proof abilities across algebra, combinatorics, and number theory.
• PutnamBench consists of 672 problems from the Putnam Mathematical Competition, requiring deep reasoning and long proof chains to solve challenging mathematical problems.
• FATE-H and FATE-X are abstract algebra benchmarks for graduate and PhD-level problems, respectively, testing advanced reasoning in areas like group theory, ring theory, and module theory.
• FLTEval is based on real pull requests from the Fermat’s Last Theorem repository, testing practical proof engineering with real-world complexity.

We saturate miniF2F completely, reaching 100% on both the validation and test sets. On PutnamBench and FATE-H/X, we compare Leanstral 1.5 against Goedel-Architect without natural-language guidance, Seed-Prover 1.5 at its high setting, and AxProverBase. Leanstral reaches a new state-of-the-art on FATE-H/X, solving 87 and 34 problems respectively. On PutnamBench, it edges out Seed-Prover 1.5 high by 7 problems at far lower cost: about $4 per problem, against an estimated $300 or more for Seed-Prover, whose high setting runs with a budget of 10 H20-days per problem. The only provers ranked higher operate under different conditions—some receive natural-language proof guidance, others cost far more to run, like Aleph Prover at $54–68 per problem.

Leanstral 1.5 shows the strongest test-time scaling we have seen from a formal-reasoning model. The figure below tracks Pass@8 on PutnamBench as we raise the token budget per attempt from 25k to 4M: performance climbs smoothly and monotonically the whole way, from 44 problems solved at 50k to 244 at 200k, 493 at 1M, and 587 at 4M. Rather than giving up when a proof runs long, Leanstral keeps reasoning, editing files, and revising across millions of tokens, turning that budget directly into solved problems—the same behavior behind the AVL-tree proof below, which ran for over 2.7 million tokens across 22 compactions.

With this release, we also fully open source FLTEval. Leanstral 1.5 lifts pass@1 on the benchmark from 21.9 to 28.9 and pass@8 from 31.9 to 43.2, surpassing Opus 4.6's 39.6 at one-seventh the cost. It also widens its lead over open-source models 3–10× larger, as shown in the figure below.

Code Verification Case Studies

While being primarily trained for mathematics, Leanstral 1.5 exhibits strong abilities in code verification. We present 2 critical case studies to demonstrate its impact.

AVL Trees: Proving Time Complexity

AVL trees are self-balancing binary search trees that maintain O(log n) height through rebalancing during insertions and deletions. Leanstral 1.5 proved these time complexity guarantees for a real implementation—a task that required structural induction to mirror the tree’s recursive structure, careful handling of monadic time tracking, and exhaustive case analysis for rebalancing paths. Over 2.7 million tokens and 22 compactions, Leanstral systematically unfolded each layer of the TimeM monad, exposing the underlying computations despite their interleaving with control flow. It established an almost tight bound of 48 steps per height unit plus a constant for insertion, then connected height to tree size via a logarithmic relationship, delivering complete, verified proofs that insertion and deletion are indeed O(log n).

Bug Discovery: Finding Hidden Flaws

To test Leanstral’s bug-catching abilities, we built an automated pipeline: Aeneas translates Rust code to Lean, while Leanstral infers the user intent and generates correctness properties from the code. Leanstral then attempts to prove each property in four attempts. If they all fail, it tries to prove the negation instead, also with four attempts. Across 57 tested repositories, this process flagged 47 violated properties, with 11 pointing to genuine bugs—5 of them previously unreported on GitHub.

One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. Leanstral’s pipeline caught it automatically, demonstrating that formal verification can already be applied to real-world codebases and find bugs that some traditional methods overlook.

Get Started

Leanstral 1.5 has a Apache-2.0 license. The weights can be found on Huggingface, while also being available now as a free API endpoint as leanstral-1-5. We recommend using it in Mistral Vibe. To begin your journey, grab an API Key, and:

1. Set up Mistral Vibe

uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup

1. Install Leanstral 1.5

/leanstall
exit

1. Launch the agent

vibe --agent lean

1. Install Lean LSP MCP (Optional)

It is highly recommended to install Lean LSP MCP by adding the following to your ~/.vibe/config.toml

[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600

If there are no existing MCP servers, you may have to remove mcp_servers = [].

1. Start proving

Ask Leanstral to tackle a theorem, debug a proof, or contribute to a repository. It’s that simple.

What's Changed

• Add chat templates integration by @juliendenize in #163
• Deprecate RawAudio in favor of str | bytes by @juliendenize in #227
• Generalize normalizer aggregation with dual separators by @juliendenize in #235
• Consolidate multimodal ContentChunk support for all message roles by @juliendenize in #241
• Fix AudioChunk.to_openai() serialization for raw audio bytes and prefixed base64 audio strings. by @haoruilee in #245
• Resolve tokenizer from local cache in offline mode by @sarathfrancis90 in #249
• Remove to_openai and from_openai from InstructRequest by @juliendenize in #251
• Bump version to 1.11.4 by @juliendenize in #252

New Contributors

• @haoruilee made their first contribution in #245
• @sarathfrancis90 made their first contribution in #249

Full Changelog: v1.11.3...v1.11.4

Today, we are introducing several new capabilities in Connectors for a more secure experience integrating to external enterprise platforms. Starting now, you can use:

• Enriched admin controls (GA) to set connector access per workspace and switch individual tools on or off across an org or workspace
• API keys with connector scopes (GA) to prevent impersonation in automated AI workloads that integrate with 3rd-party systems
• Multi-account connectors (GA) allowing users to authenticate to a single connector with multiple accounts
• Connectors Debugger (Public Preview) for end-to-end root cause analysis for MCP connectors
• Connectors in Vibe Code (GA) to reuse your connectors in developer interfaces
• Connectors in Workflows (Public Preview) allow for uninterrupted long-running tasks powered by all the tools you need

Async agents are moving into everyday work. For an agent to be trustworthy and useful inside an organization, it needs real enterprise data: CRM records, repositories, inboxes, knowledge bases. Connecting an agent to that data in a demo is easy. Running it in production is where most setups stall.

Production connectivity has a few non-negotiables. A connector should respect two sets of rules at once: the permissions already set in the source platform, and the controls your administrators set in Mistral Studio or Vibe. Automated work should run on behalf of a user or a service account, never impersonate the person who wrote it. When a connection breaks, you should be able to find out why. And an administrator should be able to decide, down to the individual tool, what is available in each part of the organization.

More control over what connectors can do

Enriched admin controls work at two levels: across your teams, and inside each connector.

• Workspace and org controls let you give each team its own connector access. Your finance workspace can reach internal data sources with no open web access, while engineering gets developer tools and the internet. Same directory, different rules per team.
• Tool-level controls go a step deeper. Inside any connector, turn individual tools on or off for a whole org or one workspace. Block anything that writes data, or one specific action like delete_file on a knowledge base. The connector stays connected; only the tools you approve can run.

API keys with connector scope handle identity. When you create a key, you choose whether it reaches only a workspace's shared connectors or your private ones too, so an automated job runs with exactly the access it needs. Paired with service accounts, automated work runs as a defined identity, never as the person who wrote it.

Multi-account connectors let one connector hold more than one login. Connect a personal and a work account to the same connector, set a default, and switch between them per task. Each account is stored and refreshed on its own, so an agent acts in the right one without you standing up a second connector.

See why a connection fails

Connectors Debugger tells you exactly where a connection breaks. Point it at an MCP server URL, add OAuth credentials if the server needs them, and run the check. It walks the connection through 11 steps, from reaching the server to opening the MCP session, and logs each one. A failure that used to mean guesswork, like a broken OAuth token exchange, shows up at the exact step it happens.

Connectors in Workflows and Vibe for Code

Connectors in Workflows keep long and scheduled runs from breaking on auth. You declare the connectors a Workflow needs, and the accounts it should run with, right in the Workflow definition; Studio resolves those dependencies when you start a run. Personal credentials stay out of automated work, and a job won't fail halfway because a token expired. A nightly run can pull from a CRM, update a tracker, and read a knowledge base across the whole job without dropping a connection.

Connectors in Vibe Code bring the same governed access to the coding agent. Type /connectors to pick from local MCP servers and the workspace connectors your admins approved, choose which tools to enable, and start a task. Async agents can reach Outlook, Jira, Notion, Linear, and Confluence under the same rules you set everywhere else.

We're adding connectors continuously. The directory now covers more than 60 integrations, and when the platform you need isn't listed, a custom MCP connector fills the gap.

Start building

Enterprise controls, Connector Credentials, and Connectors in Vibe Code are generally available now. Connectors Playground and Connectors in Workflows are in public preview. All of it is live in Studio.

• Connectors documentation
• Connectors in Vibe Code documentation
• Connectors in Workflows documentation and cookbooks
• Open the Studio console

Today, we're releasing Mistral OCR 4, featuring bounding boxes, block classification, and inline confidence scores alongside extracted text. The model supports 170 languages across 10 language groups, runs in a single container for fully self-hosted deployments, and serves as an ingestion component for enterprise search, RAG, and domain-specific retrieval pipelines. OCR 4 is a small, focused model, and this post covers what's new, how it performs on public and internal benchmarks, the known limitations of those benchmarks, and guidance on when to use the model API versus Document AI.

Highlights

• Breakthrough performance. Independent annotators prefer OCR 4 over every leading OCR and document-AI system tested, with win rates averaging 72%, alongside the top overall score on OlmOCRBench (85.20). See Benchmarks below for methodology and known scoring limitations.
• Segmentation, not just text. Alongside the extracted text, OCR 4 returns bounding boxes, typed-block classification (titles, tables, equations, signatures, and more), and inline confidence scores. Bounding boxes, our most-requested capability, localize text for in-context highlighting and reliable data pipelines. At the same time, block types and confidence scores drive source-grounded citations, redactions, and human-in-the-loop verification.
• Integrated with Mistral Search Toolkit (public preview). OCR 4 is an ingestion component of Search Toolkit, Mistral's open-source, composable search framework, announced at the AI Now Summit. Its structured output supplies citation-ready inputs to the toolkit's ingestion, retrieval, and evaluation workflow for RAG and enterprise search.
• Multilingual coverage. Support for 170 languages across 10 language groups, with measurable gains on specialized and low-resource languages where several competing systems degrade.
• Run on your own infrastructure. OCR 4 is compact enough to deploy on a single container, keeping document data in your environment for residency, sovereignty, and compliance, while supporting cost-efficient, high-throughput batch processing. Self-managed deployment is available to enterprise customers.

Overview

Mistral OCR 4 extracts and structures content from a wide range of documents. Where previous generations focused on converting a page into clean text and tables, OCR 4 returns a structured representation of the document. Each block is localized with a bounding box, classified by type, and inline confidence scores are generated per-page and per-word. Downstream systems, therefore, have access not only to what the document says but also to where each element sits, what role it plays, and how confident the model is in each region.

This structure supports several downstream workloads:

• Semantic chunking for RAG: clean, classified blocks become better retrieval units.
• Structural primitives for agents: agents move from reading documents to acting on them (form filling, invoice processing, compliance checks).
• Structured content for connectors: consistent, typed output for ingestion and indexing pipelines.

OCR 4 accepts common enterprise formats, including PDF, DOC, PPT, and OpenDocument, and supports 170 languages across 10 language groups, including specialized and low-resource languages that many systems handle poorly. As a compact model deployable in a single container, it is suited to both cost-sensitive and high-volume deployments. It can run fully self-hosted, allowing organizations with data-sovereignty requirements to keep document data within their own infrastructure.

Developers integrate the model via API, and teams can use Document AI in Mistral Studio for an application-level, no-code path to the same engine. Mistral OCR 4 through the API is priced at $4 per 1,000 pages, with a 50% Batch-API discount, reducing the cost to $2 per 1,000 pages. Document AI is priced at $5 per 1,000 pages.

Benchmarks

“We benchmarked Mistral OCR 4 against the leading agentic document parsers across a chart and figure dense financial QA dataset and reached equivalent accuracy at roughly 8x lower cost and 17x lower latency. For production use cases at scale, that delta compounds fast.” - Aidan Donohue, AI Engineer, Rogo

To evaluate OCR 4, we compared it against leading AI-native OCR models, frontier general-purpose models, enterprise document services, and our own Mistral OCR 3.

Human Preference Evaluations

Automated benchmarks carry the scoring artifacts described above, so we complemented them with a head-to-head human evaluation on documents chosen to reflect real usage. We assembled 600+ documents across 12+ languages, sourced from third-party vendors to represent real industry use cases, and asked independent annotators to blindly rank each competitor's output against OCR 4's, document by document.

Annotators preferred OCR 4 in the majority of documents across all systems tested. Because these are human judgments on realistic documents rather than string comparisons against fixed references, they sidestep much of the annotation and formatting noise that affects automated scores.

Overall Performance

“Mistral OCR is roughly 4x faster per page than our incumbent provider, an impressive result for the high-volume docketing workflows where speed is critical to managing our customers' IP timelines.” - Ivan Mihailov, AI engineer, Anaqua

In addition to placing first in our human preferences, OCR 4 achieves the top overall score amongst the models we tested on the public OlmOCRBench (85.20) and leads our internal Crawl Multilingual evaluation (.98), ahead of both AI-native and enterprise solutions.

On OmniDocBench, OCR 4 achieves a score of 93.07. We report this figure with a caveat: both OlmOCRBench and OmniDocBench have known limitations in how they score certain outputs, and a single aggregate number can both understate and overstate real-world performance.

When we audited the mismatches behind our scores, most were not model errors but artifacts of how the benchmarks compare output. The recurring categories:

• Ground-truth errors. Some reference annotations are themselves incorrect: missing or extra text, transcriptions of redacted regions, or typos (for example, a cited author's name misspelled in the reference but read correctly by the model from the page). The output matches the source document, yet it is still marked wrong.
• Equivalent math notation. Different LaTeX that renders identically is counted as a mismatch, The rendered equation is correct; the string comparison is not.
• Equation segmentation. Whether an expression is emitted as a single equation or split into several inline fragments affects the match, even when the rendered content is identical, because the matcher cannot align the pieces.
• Multi-column reading order. Words split across a column boundary (for example, "certifi-cates") and column-ordering assumptions cause correct extractions to be scored as reading-order failures.
• Block-type attribution. The benchmark does not expect headers/footers in the output. To resolve this we strip headers footers from our output before scoring. But the test then checks for a string that also happens to be the title of the page which should actually be present and flags it incorrectly.

These artifacts concentrate in mathematical, scientific, and multi-column documents, and they more often penalize correct output than reward incorrect output. We therefore treat the aggregate score as directional rather than definitive.

These benchmarks are directional. All competitor scores reflect internal reproductions. We recommend evaluating on your own documents.

Performance Details

Crawl Multilingual breakdown. On our internal multilingual evaluation, OCR 4 leads across all eight language groups — English, Western Europe, Eastern Europe, Middle Eastern, Chinese, East Asian, Southeast Asian, and specialized languages (Hindi, Japanese, Georgian, Bengali, Armenian, Hebrew, Greek, Gujarati, Tamil, Malayalam, Kannada, Telugu). The gap is widest for specialized and low-resource languages, where many competing systems degrade sharply, while OCR 4 maintains high accuracy.

Recommended use cases

OCR 4 supports both high-volume pipelines and interactive document workflows, including:

• Document parsing and extraction: complex, multilingual documents.
• Retrieval-Augmented Generation (RAG): structured, classified, citation-ready content for semantic chunking and source-grounded answers. With Search Toolkit, OCR 4 output can be fed directly into retrieval pipelines.
• Agentic workflows: providing agents with the structural primitives to complete tasks such as form filling, invoice processing, and compliance checks, especially in legal, financial services, and healthcare.
• Structured data pipelines using confidence scores to enable efficient use of human verifiers: form/invoice extraction, redactions, and compliance-driven processes.
• Enterprise search and knowledge bases: OCR as a data-source component for custom ingestion and entity extraction.

Early users are applying OCR 4 to turn invoices into structured fields, digitize company archives, extract clean text from technical and scientific reports, and power enterprise search.

A note on out-of-scope use.

OCR 4 is a document-understanding model, not a decision-maker. It is not intended for medical diagnosis, legal advice or judgment, high-stakes financial decisions, safety-critical systems, real-time/latency-sensitive processing, or non-document inputs (raw audio, video, etc.).

OCR 4 API: Understanding Your Options

Mistral's OCR 4 is available through a single API endpoint. Every request runs the same underlying OCR model and always returns extracted content, bounding boxes, block types, confidence scores, and markdown-structured text. What varies is how much you layer on top.

Use OCR 4 in pure extraction mode when you want to:

• Embed fast, accurate document extraction directly into your application, agent, or data pipeline.
• Work directly with the raw response, bounding boxes, block types, and confidence scores to drive custom downstream logic.
• Run high-volume or batch ingestion with full control over throughput and cost via the Batch API.
• Self-host for strict data-privacy, sovereignty, or compliance requirements.

Activate Document AI capabilities (same endpoint, additional parameters) when you want to:

• Return structured JSON in a schema you define — pass a JSON schema alongside your document, and the OCR output is fed to mistral-small-2603 to generate content shaped to your spec.
• Annotate detected images with structured JSON by passing an image annotation schema, triggering an additional vision-language model call per image.
• Use a custom prompt alongside a JSON schema to guide how the extracted content of the full document is interpreted or summarized.
• Enable business users, solutions teams, or pilots to produce structured results without writing downstream parsing logic.

The practical decision rule: if you need raw extracted content, use OCR 4 as-is. If you need the output reshaped into a structured format, annotated with domain-specific fields, or processed with a custom instruction, add the Document AI parameters to the same call. You always get the OCR result regardless; Document AI simply adds structured layers on top of it.

Now available

“The availability of Mistral Document AI with OCR 4 in Microsoft Foundry marks an important milestone in our partnership. Together, we’re enabling customers to bring advanced, structured document understanding directly into their AI workflows, combining Mistral’s innovation with Microsoft’s enterprise platform to deliver scalable, trusted solutions for real-world business needs.” -Kimmi Grewal, VP, AI Ecosystem Partnerships, Microsoft

Both Mistral OCRv4 and Document AI (powered by OCRv4) are available via API through Mistral Studio, Amazon SageMaker, Microsoft Foundry, and coming soon Snowflake Parse Document. For organizations with stringent data-privacy requirements, OCR 4 also offers a self-hosting option so sensitive information stays within your own infrastructure. To explore self-deployment, let us know.

Get started

We offer a few ways to get started and learn more quickly.

• Try OCR 4. The new Getting Started with OCR 4 Cookbook walks through a first extraction, working with bounding boxes, and block classification.
• OCR 4 webinar. We'll cover what's new in OCR 4 with demos and Q&A on July 7th at 6:00 PM CET. Register for the OCR4 in Production webinar.
• Contact Sales for more information.

We released OCR 4 (mistral-ocr-4-0). mistral-ocr-latest now points to it.

MODEL RELEASED

Introducing include_blocks in our OCR API. When set to true, each page returns a blocks array with paragraph-level bounding boxes and a structural label (text, title, list, table, image, equation, caption, code, references, aside_text, header, footer, signature) in reading order. Learn more in our OCR documentation.

API UPDATED

The pages parameter in our OCR API now also accepts a string of comma-separated digits and ranges (e.g. "0,1,2", "0-5", or "0,2-4") in addition to a list of integers.

API UPDATED

What's Changed

• Raise multiple format of reasoning for from_openai by @juliendenize in #224
• Preserve zero OpenAI seed in chat request conversion by @pragnyanramtha in #226
• Pin uv required-version and bump pre-commit hook by @juliendenize in #228
• Add to_openai reasoning format for AssistantMessage by @juliendenize in #223
• fix(tokenizer): point users at from_hf_hub on unknown model (#229) by @NishchayMahor in #231
• Fix: forward continue_final_message in tekken normalizers (V7/V15) by @matdou in #233
• Version 1.11.3 by @juliendenize in #239

New Contributors

• @pragnyanramtha made their first contribution in #226
• @NishchayMahor made their first contribution in #231
• @matdou made their first contribution in #233

Full Changelog: v1.11.2...v1.11.3