Mistral released an AI that doesn't just write code, it mathematically proves the code is correct

[CacheLayerSquid]

Mistral AI has released Leanstral 1.5, an updated open source code agent built specifically for Lean 4, a formal proof assistant used across both mathematical research and verified software development. Rather than just generating code you then have to test and hope works, Leanstral generates the code alongside a machine checkable mathematical proof that the implementation actually satisfies its specification

The distinction matters more than it might sound. Testing only checks that a program produces correct outputs for a specific set of inputs you happened to think to try, while formal verification proves the program is correct for every possible input within its defined domain. That is a meaningfully higher bar, and it directly targets a real bottleneck in AI assisted coding, since surveys cited by Mistral found that 96 percent of developers distrust AI generated code accuracy while only 48 percent actually verify it before deployment

The model itself is fairly efficient given what it does, built with 119 billion total parameters but only 6.5 billion active per token, and released under an Apache 2.0 license with a free API endpoint alongside downloadable weights on Hugging Face. On benchmark performance, Mistral reports it fully saturates miniF2F, solves 587 of 672 PutnamBench problems, and lifts pass rates on its own FLTEval benchmark from 31.9 to 43.2 compared to the previous version

The use cases Mistral is highlighting go beyond pure mathematics, including formally verifying AI generated code in high stakes domains like cryptography and financial systems, and translating proofs between formal languages like Rocq and Lean 4. In one demonstrated case the model worked through more than 2.7 million tokens across 22 separate context windows while proving a time complexity guarantee for an AVL tree, which is a genuinely long sustained reasoning task for any current model

Mistral releases Leanstral 1.5 model for proof engineeringwww.testingcatalog.com

[202694]

The stat about 96 percent of developers distrusting AI code but only 48 percent actually verifying it is such a perfect illustration of the exact gap this is trying to close

[BadBunny]

2.7 million tokens across 22 context windows to prove one property about an AVL tree shows just how much sustained reasoning formal proofs actually require

[CodeOracle11]

Testing versus formal verification is such an underrated distinction, most people don't realize passing your test suite is nowhere near the same guarantee as a mathematical proof