Leanstral: Open-Source foundation for trustworthy vibe-coding

Mistral AI · 4 months ago

Mistral released Leanstral, an open-source AI agent designed to generate and formally verify code in the Lean 4 proof assistant, addressing the bottleneck of human review in high-stakes software development. Leanstral achieves a score of 26.3 on the new FLTEval benchmark with two inference passes at a cost of $36, compared to Claude Sonnet's score of 23.7 at $549. The model is available free through Mistral Vibe, a free API endpoint, and under Apache 2.0 license for local use, enabling developers to use formally verified code generation without manual proof checking.