Leanstral: Open-Source foundation for trustworthy vibe-coding

Mistral AI has released Leanstral, the first open-source code agent designed for the Lean 4 proof assistant. The model is intended to help with high-stakes domains like mathematics and critical software by formally proving its own implementations against strict specifications. Benchmarks show the efficient, sparse-architecture model is cost-effective and performs competitively against larger open-source models and proprietary alternatives like Anthropic's Claude Sonnet. Leanstral is available under an Apache 2.0 license and can be used for tasks like debugging, code conversion, and proving program properties.