Leanstral 1.5 is an advanced open-source (Apache-2.0) formal verification model featuring 119B total parameters with a 6B active parameter architecture. Designed for Lean 4, it represents a significant advancement in automated proof engineering, characterized by its ability to saturate the miniF2F benchmark, solve 587/672 problems in PutnamBench, and achieve state-of-the-art performance of 87% on FATE-H and 34% on FATE-X.

Core Methodology

The model’s training pipeline involves three distinct stages: mid-training, supervised fine-tuning, and reinforcement learning utilizing the CISPO (Context-Integrated Sequential Proof Optimization) framework. Leanstral 1.5 operates through two specialized environments:

1. Multiturn Environment: The model engages in an iterative loop where it submits proofs to the Lean compiler. It receives real-time feedback regarding compilation success or error diagnostics, enabling it to refine its strategy until a solution is reached or its computational budget is exhausted.
2. Code Agent Environment: The model functions as an autonomous developer within a filesystem. It executes bash commands, edits files, and interfaces with the Lean language server. This environment allows for long-horizon planning, such as constructing auxiliary lemmas or performing context compaction when proofs grow complex.

Test-Time Scaling and Performance

Leanstral 1.5 exhibits exceptional test-time scaling properties. Performance on PutnamBench follows a monotonic increase correlated with token budget expansion:

• At a 50k token budget: 44 solved problems.
• At a 4M token budget: 587 solved problems.

The model demonstrates an ability to persist through long-duration reasoning, exemplified by an AVL-tree verification task that spanned over 2.7 million tokens across 22 compactions, effectively managing state across massive reasoning chains.

Real-World Verification and Bug Discovery

Beyond pure mathematics, the model demonstrates high efficacy in real-world code verification:

• Time Complexity Proofs: Using structural induction and the $TimeM$ monad, the model formally verified that AVL tree insertions and deletions maintain $O(\log n)$ height complexity. It established a bound of 48 steps per height unit plus a constant factor.
• Automated Bug Detection: By utilizing Aeneas to translate Rust code into Lean, the model infers correctness properties. Through a process of attempting to prove properties or their negations, it identified 11 genuine bugs across 57 repositories, 5 of which were previously undocumented. A notable example includes a $Std.U64.MAX$ overflow vulnerability in the datrs/varinteger library, which eluded traditional fuzzing methods.

Leanstral 1.5 offers a cost-effective alternative to proprietary models, achieving a $Pass@8$ of 43.2 on FLTEval at one-seventh the cost of comparable commercial solutions. The model is accessible via Hugging Face and a free API, integrated into the Mistral Vibe ecosystem for practical proof engineering.