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

Mistral AI's Leanstral is an open source code agent that uses formal verification via the Lean 4 theorem prover to mathematically prove code correctness, aiming to eliminate human code review bottlenecks. Built on a Mixture-of-Experts architecture with 119B total parameters (6.5B active), it targets high-stakes domains like aerospace and cryptography. However, experts caution that formal verification only proves code matches its specification — not that the specification itself is complete or aligned with real-world requirements. Additional gaps exist because Leanstral operates in Lean 4, requiring translation to production languages like Rust or Python, introducing a correctness gap. The consensus is that human judgment shifts rather than disappears, moving from detailed code review to higher-level oversight of specifications and risk assessment.