While I really don't have much love for the Mistral products due to being way behind even cheap open weights Chinese mod...

While I really don't have much love for the Mistral products due to being way behind even cheap open weights Chinese models such as the Qwens, DeepSeeks etc of this world, this is an interesting (possibly new) approach:https://www.heise.de/news/Leanstral-1-5-Mistrals-KI-Modell-fuer-formale-Beweise-ist-Open-Source-11355236.html / https://www.heise.de/en/news/Leanstral-1-5-Mistral-s-AI-model-for-formal-proofs-is-open-source-11355532.htmlWith the money quote being:"In addition to mathematical proofs, Mistral demonstrates a pipeline for automatic bug detection in Rust projects. The tool Aeneas translates Rust code to Lean, after which Leanstral derives correctness properties and attempts to prove or disprove them. "This goes past the very elaborated statistical parrots that LLMs are and goes into the formal verification territory. As much as I understand this, this is closer to a model checking approach than what we had before and would in theory thus even allow to check for concurrency is...