Formal code verification and testing offer a way around AI blind spots

Your AI may need AI to oversee its work. Gallic AI biz Mistral is leaning into making AI code generation more reliable with Leanstral, a coding agent for proofs constructed using the open source Lean programming language.

Formal code verification, Mistral argues, reduces the need for human code review, a potentially time-consuming process. Proofs, tests, linting, and specifications can help ground AI code agents in reality so that they produce better output.

Leanstral has been released with open weights (Apache 2.0) as an agent mode within Mistral Vibe, and via a free API endpoint. It is accompanied by results from an as-yet-unreleased benchmark test called FLTEval, designed to evaluate how AI models handle engineering proofs.

According to Mistral, Leanstral-120B-A6B outperforms larger (more parameters) open source rivals like GLM5-744B-A40B, Kimi-K2.5-1T-32B, and Qwen3.5-397B-A17B on FLTEval.

But perhaps more noteworthy is Leanstral's effect on one's bank account.

"Leanstral ...