Mistral’s Leanstral wants to kill off human-in-the-loop code checks, but is it blowing in the wind?

Mistral AI launched Leanstral, an open-source coding agent built on Lean 4 that can generate code and prove it matches a specification.

The pitch is to cut human review by using machine-checkable proofs for software output.

But the article stresses that formal verification only helps if the requirements are complete, accurate, and current.

If the spec is flawed or missing details, mathematically proven code can still be the wrong solution.