The Leanstral team has recently released Leanstral 1.5, a lightweight open-source artificial intelligence model designed to advance formal verification and automated proof engineering. Licensed under Apache 2.0, the model features a hybrid architecture with 119 billion total parameters and only 6 billion active parameters, making it highly efficient for complex reasoning tasks. The release marks a significant step toward democratizing rigorous formal methods by providing both open weights via Hugging Face and a complimentary API endpoint. The development of Leanstral 1.5 involved a rigorous three-stage training pipeline encompassing mid-training, supervised fine-tuning, and reinforcement learning utilizing the CISPO framework. Training occurred across two distinct environments: a multiturn theorem proving arena where the model iteratively refines proofs based on Lean compiler feedback, and a code agent workspace where it operates within a raw filesystem to edit files, execute shell commands, and interact with the Lean language server in real time. This dual approach enables the model to navigate long-horizon proof engineering workflows, including completing partial proofs and generating auxiliary lemmas, with final correctness verified through a custom fork of SafeVerify. Performance evaluations demonstrate state-of-the-art capabilities across multiple formal reasoning benchmarks. Leanstral 1.5 fully saturates the miniF2F dataset, solves 587 out of 672 Putnam Mathematical Competition problems, and achieves new record scores on FATE-H at 87 percent and FATE-X at 34 percent. The model exhibits exceptional test-time scaling, with problem-solving success rates climbing monotonically as token budgets increase from twenty-five thousand to four million tokens. Notably, Leanstral 1.5 delivers these results at approximately four dollars per problem, drastically undercutting the estimated hundreds of dollars required by comparable high-performance provers. On the FLTEval benchmark, which tests practical proof engineering against real-world repository pull requests, the model outperforms both larger open-source alternatives and proprietary systems at a fraction of the computational cost. Beyond theoretical mathematics, Leanstral 1.5 has demonstrated robust utility in software verification. In a comprehensive case study, the model successfully proved O(log n) time complexity guarantees for a real-world AVL tree implementation, requiring structural induction and exhaustive case analysis across millions of tokens. When deployed in an automated verification pipeline across fifty-seven open-source repositories, Leanstral identified forty-seven violated properties and uncovered five previously unreported software defects. One critical finding involved a buffer overflow in a Zigzag decoding library that caused silent data corruption in release builds, highlighting the model capacity to detect edge cases that traditional testing and fuzzing methodologies frequently miss. Users can now deploy Leanstral 1.5 immediately through the provided Hugging Face repository or the free API. The development team recommends integrating the model with Mistral Vibe for an optimized agentic experience, with optional Lean LSP MCP configuration available for developers seeking deeper IDE integration. This release establishes Leanstral 1.5 as a highly accessible, cost-effective tool for researchers and engineers aiming to apply formal verification to complex mathematical and software engineering challenges.