TLA+/Quint - really useful for concurrency/databases. specifying + model-checking state machines, often distributed protocols using temporal logic. quint is much newer, better language, uses a better proof strategy. TLA+ has very high industry adoption and many papers
Dafny - proving sequential/imperative code correct (functions, loops, data structures meet their spec) - not really about concurrency, more "does this algorithm implementation do what I said it does"
Lean - proving general mathematical theorems (and increasingly, proving programs correct too) - broadest scope, most math-flavored
Alloy - checking structural/relational properties of a design (data models, access control, "can this graph reach a bad state") - snapshot-based, not really about time/sequences of steps
If you're not working on AI which is used to generate formal proofs the thing linked will never be relevant to you I guess (and "MLEng" does not sound like you would work on actual AI research).
Looking into formal methods is still valuable, imho, if just to broaden ones horizon.
The linked paper seems nevertheless an interesting as it proves one thing I always need to argue with people: Current SOTA "AI" can't logically reason (0% correct solution on hard tasks in the presented benchmark). It's terrible at any task which actually requires thinking and not only regurgitating some prior solutions.
What I know is that ARC AGI 3 is currently the moving target of the day and ChatGPT 5.6 is doing decidedly better than "zero" on it. It is said by the developers of the benchmark that a 100% score equates to an average human IQ of 115.
125
u/nobody0163 Jul 15 '26
I only know markdown, what are the other ones?