Comment by fragmede

LLMs are not at the point where they can reliably complete this kind of task without making mistakes. The model checker can tell you whether the formal design specification contradicts itself, but it can't tell you whether it matches the implementation, nor whether it matches the programmers' intentions. And it's too much for humans to review by hand.

This is importantly different from formal code verification, in which the specification that needs to match the programmers' intentions is small enough to review, while the bulk of the LLM's output is proof tactics and such, which don't need human review because the verifier guarantees* that they're right.

I suppose you could just tell Fable "hey try using TLA+ to look for bugs in this code" and see whether it finds any.

* Uh, usually. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

Because AI have a recall of 80% or 90% at best. While it might be better than some human, it won't hit the 100% TLA+ modeling aims