Mistral AI says Leanstral 1.5 found five previously unreported bugs in a public test across 57 open-source repositories. One was an integer overflow in a Rust library that panics in debug builds and silently produces incorrect output in default release builds.

Released on July 2, 2026, Leanstral 1.5 is a 119-billion-parameter open-source model built for formal verification in Lean 4. Its job is to help write mathematical proofs about code and mathematical statements, with a verifier checking the results.

The repository findings are a useful reason to examine the model beyond its math benchmark scores. They suggest that automated proof work could help uncover errors in ordinary libraries, although five findings don't establish how reliably it will work across other codebases.

The Rust overflow finding

The clearest example in Mistral's report is datrs/varinteger, a Rust crate that encodes and decodes variable-length integers using zigzag encoding. Its zigzag decoding function performs a (value + 1) operation. When value is u64::MAX, the largest unsigned 64-bit integer, that addition overflows.

Rust handles this differently depending on the build settings. In debug mode, the overflow triggers a panic. In release mode, where overflow checks are disabled by default, the addition wraps around and produces incorrect decoded output. That difference can complicate diagnosis because the same input causes different behavior in development and production.

A unit test using u64::MAX could catch this bug. A fuzzer could also find it if it reached the relevant input and checked the result appropriately. The problem is coverage: neither approach guarantees that a particular boundary case has been exercised.

Formal verification approaches the function differently. A proof obligation covering overflow across the input range forces that boundary case to be accounted for. If the claimed property doesn't hold, the proof cannot be completed as stated. Investigating that failure can expose the bug.

Mistral describes all five findings as previously unknown. The age of the varinteger bug and whether it caused any production incidents aren't established in the reporting available as of July 12, 2026.

What a proof adds to testing

Unit and integration tests check behavior for selected inputs and scenarios. Fuzzing expands that coverage by generating inputs automatically. These methods provide evidence that code behaves correctly, but passing a test suite generally doesn't prove a property across every possible input.

Formal verification can establish that a specified property holds for every input covered by a formal model and its assumptions. For example, a verified proof that a function cannot overflow is stronger than a collection of tests in which no overflow occurred. The property being proved and the model's relationship to the running code still matter.

The longstanding obstacle is the work involved. Writing proofs in systems such as Lean, Coq, or Isabelle requires specialist knowledge and can take substantial time. Formal verification is used in areas such as aerospace software and security-critical cryptographic primitives, where the consequences of an error justify that effort. Many ordinary libraries haven't received the same attention.

Leanstral 1.5 is intended to reduce the proof-writing burden. It could make some verification projects practical without removing the need for someone to decide what the code must guarantee.

How Leanstral works

The model uses a mixture-of-experts architecture with 119 billion total parameters and about 6 billion active for a given inference. Activating only part of the model reduces computation compared with using all 119 billion parameters for every token. That doesn't make it equivalent to a small model in every resource requirement, but it is an important part of its inference design.

Its context window holds 256,000 tokens. Long proof tasks can require considerably more work than fits in a single window. Mistral reports that an AVL tree proof required 2.7 million tokens of reasoning and 22 context compactions, which reduce accumulated context so work can continue. That example illustrates the scale of the task compared with a 4k or 8k context window, as well as the need to manage context even with a much larger one.

Training followed three stages: mid-training on proof corpora, supervised fine-tuning, and reinforcement learning using a technique Mistral calls CISPO. The reinforcement-learning stage used two environments. One was a multiturn theorem-proving loop with compiler feedback. The other was a code-agent environment with a filesystem and a Lean language server.

That feedback is central to the approach. The model can propose proof steps, receive verifier errors, and revise its work rather than simply generate text that resembles a proof.

For Rust, the workflow uses Aeneas to translate source code into a Lean representation. This avoids manually rewriting the Rust implementation in Lean before starting verification. The translation tooling still needs to be configured, and the properties to be checked still need to be specified.

Benchmarks and the cost of longer searches

Mistral reports strong results on several formal mathematics benchmarks:

  • miniF2F: 100%, solving every problem in a set that ranges from high-school mathematics to math olympiad difficulty.
  • PutnamBench: 587 of 672 problems drawn from the William Lowell Putnam Mathematical Competition, a leading North American undergraduate mathematics competition. According to the release, this places Leanstral 1.5 behind only the closed-source Aleph Prover and ahead of previous open models.
  • FATE-H and FATE-X: 87% and 34%, respectively. These benchmarks cover master's- and doctoral-level algebra, including group theory and ring theory. Mistral describes both scores as state of the art.

The reasoning budget makes a substantial difference. In the reported PutnamBench scaling results, the number of solved problems rises from 44 at a 50,000-token budget to 587 at 4 million tokens. Mistral reports that performance increases monotonically across the tested budgets.

That creates a practical tradeoff. More computation can give the model more opportunities to find a valid proof, but the larger budgets also mean more time and expense. A critical encoding function may justify a longer search than a lower-risk utility.

The distinction is between the chance of completing a proof and the strength of an accepted proof. A larger budget helps the search. The verifier still checks the resulting proof against the stated property. Math benchmark scores also don't directly measure how much engineering work is needed to verify a production library.

Where an evaluation makes sense

The clearest candidates are cryptographic primitives, serialization and deserialization libraries, numeric encoding functions, protocol parsers, and data structures with memory-safety requirements. Errors in these components can lead to security vulnerabilities, corrupted data, or crashes, making specialist verification effort easier to justify.

For routine Python glue code in a web application, formal verification is less likely to be the best immediate use of engineering time. Conventional tests and other development tools remain useful, including for the boundary cases that a proof-oriented workflow might uncover.

As of July 12, 2026, the model is available under an Apache 2.0 license on Hugging Face. Mistral also offers a free API endpoint during the beta period, scheduled to run through September 30, 2026. That provides a way to evaluate it without hosting the model.

Leanstral is also integrated into Mistral Vibe, Mistral's agentic IDE environment. That may make experimentation easier, but an IDE-driven loop doesn't remove the need to understand what is being verified. Lean 4 remains specialist tooling.

The work that remains

Formal verification tools, including Lean, Coq, Isabelle, and TLA+, have developed over decades. Proof-writing expertise remains a constraint that a capable model could help ease.

A team using Leanstral still needs enough Lean 4 knowledge to review the formal statements and understand the generated proofs. It must set up translation tooling where applicable and define the properties that matter. A model may infer some useful properties, but it cannot be assumed to identify every requirement.

If a model could handle 80% of the proof-writing work for a critical function, the remaining 20% might become a manageable specialist task. That is a hypothetical illustration of the potential savings, not a measured productivity result for Leanstral 1.5.

The five reported bugs provide a concrete starting point for evaluation. A team can then assess whether it can specify and verify an important property in its own code at an acceptable cost, with a clear understanding of what the proof covers and what remains outside it.