Leanstral Model
https://mistral.ai/news/leanstral
Mistral AI introduces Leanstral — an open-source code agent for the Lean 4 programming language (which is also an interactive theorem prover). This model, with 6B active parameters in a sparse architecture, is trained not only to perform tasks but also to formally prove the correctness of implementations. This makes it a powerful tool for code verification.

Available for free in Mistral Vibe https://mistral.ai/products/vibe (via API labs-leanstral-2603) and for download for on-premise hosting and integration with lean-lsp-mcp. This is the first contribution to a future where formal verification becomes commonplace and human review is no longer a bottleneck.

HN Reaction
https://news.ycombinator.com/item?id=47404796
Enthusiasts see a future in "executable specs" where an agent writes code + proofs, making regressions impossible. Skeptics remind that proofs only guarantee validity, not that you proved exactly what you intended, and for ordinary projects (non-mathematical/critical software), this is currently "overkill".

#mistral #newllmmodel