Formal Verification for Everyone

Formal verification has always been one of those things that sounds great in theory and is impossible in practice. The idea is simple: instead of testing your code and hoping you caught the bugs, you mathematically prove the code is correct. No surprises, no edge cases, no "well it worked on my machine." The reality, of course, is that writing formal proofs is painstaking, slow, and requires expertise that almost nobody in software engineering has [1].

Mistral just released Leanstral 1.5, an open-source AI model that might actually change that math. It is a 119B parameter model (only 6B active, using sparse mixture-of-experts) designed to write and verify formal proofs in Lean 4, a proof assistant language used by mathematicians [2]. And it is licensed under Apache 2.0, which means anyone can use it, modify it, and build on it without asking permission.

What it actually does

Leanstral 1.5 works in two modes. In the first, you give it a theorem statement and it tries to prove it, submitting proof attempts to the Lean compiler and refining its approach based on feedback. In the second, it operates like a developer with filesystem access: editing files, running shell commands, using the Lean language server to inspect types and goals in real time [3]. This second mode is the interesting one, because it means the model can work on real codebases, not just isolated problems.

The benchmark results are striking. Leanstral 1.5 saturates miniF2F, a formal math benchmark ranging from high school to olympiad level, hitting 100% on both validation and test sets. On PutnamBench, 672 problems from the Putnam mathematical competition, it solves 587 [4]. On FATE-H and FATE-X, graduate and doctoral-level abstract algebra benchmarks, it achieves 87% and 34% respectively, both state-of-the-art for open-source models.

But benchmarks are benchmarks. What caught my attention is the bug hunting.

Finding real bugs in real code

Mistral built an automated pipeline: a tool called Aeneas translates Rust code into Lean, and then Leanstral infers what correctness properties the code should have and attempts to prove them. If it cannot prove a property, it tries to prove the opposite, that the property is violated. Across 57 open-source repositories, this process flagged 47 violated properties, with 11 pointing to genuine bugs. Five of those were previously unreported on GitHub [5].

One example: in the Rust library varinteger, the sign function for zigzag decoding had an overflow bug. On input Std.U64.MAX, the expression (value + 1) would overflow, causing crashes in debug mode and silent data corruption in release mode [6]. This is exactly the kind of edge case that unit tests and fuzzing tend to miss, but that formal verification catches by construction.

The cost question

Here is where it gets practical. Leanstral 1.5 solves PutnamBench problems at roughly $4 per problem. The next best open-source competitor, Seed-Prover 1.5, costs an estimated $300 per problem at its high setting, running with a budget of 10 H20-days per problem [7]. That is a 75x cost difference. The only prover that beats Leanstral on PutnamBench is Aleph Prover, which is closed-source and costs $54-68 per problem.

For teams already using Lean 4 in academic or industrial research, this is a big deal. For teams not using Lean 4, it is a reason to start.

Why this matters beyond math

Formal verification has been the holy grail of software reliability for decades, and the reason it never caught on is simple: it was too hard. Writing proofs required PhD-level expertise in logic and type theory, and even experts could spend weeks on a single proof. The promise of AI-assisted formal verification is not that the AI replaces the expert, but that it lowers the barrier enough for ordinary software engineers to use these tools without becoming formal methods researchers.

Leanstral 1.5 is not going to prove the correctness of a full operating system tomorrow. It proved time complexity guarantees for AVL tree operations, and that proof ran for 2.7 million tokens across 22 context compactions [8]. That is impressive, but it is also a single data structure. The gap between "can prove AVL trees are O(log n)" and "can prove a distributed database is linearizable" is enormous.

But the direction is right. The model is open-source, the cost is low, the results are real, and it found actual bugs that humans missed. The gap between formal methods and practical software engineering is closing. Not fast, but it is closing.

And when that gap closes enough, the question shifts from "can we formally verify this?" to "why are we shipping code that we have not verified?"