#modelchecker — Public Fediverse posts on home.social

JTI @[email protected] · 2026-07-07 · 08:00 UTC

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.html

With 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 issues like race conditions etc reliably.

The hard part there of course was to provide the provably correct bridge between the code to be tested and an efficient model checker representation of the same code. Asking the model checker smart "questions" is another part as is translating findings back to the original code.
Since the LLMs guzzle up RAM and CPU already, the consumption of the model checkers / theorem provers isn't an issue anymore (as long as the model they're being fed is efficient...)

Lets see how well the LLMs do on this work.

I'm sure there are already US or Chinese models that do this or will replicate it in a months time.
I think I read about Meta experimenting on this as well.

Did I get the announcement right? Has anyone had their hands on said model+prover combo already? Is anyone aware of Chinese/US equivalent contraptions?
Any updates @heiseonline @heisedeveloper can provide on those questions in the article, especially on competitors?

#llm #ai #formalverification #modelchecker #modelchecking #concurrency #correctness #meta #mistralai #aeneas #leanstral