> It also found the bug that Leanstral 1.5 found and the authors highlighted

This is a little bit like someone pointing the moon and you look at the finger.

The formal proof domain goes way beyond just finding bugs.

It has tons of usages in term of functional safety, protocol validation, cryptography, etc...

The fact Mistral tackle this kind of problem is both smart and not so surprising.

Smart because it is niche enough that they do not front face the big competitors (yet).

No so surprising because the French labs have a well known and long time expertise with formal proof tools (Coq and all its Ocaml associated tools). It has been historically mainly pushed by the aerospace and train industries (Airbus, Dassault, Alsthom).