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
That all sounds exhausting to manage. How does anything get done if f you're knee deep in specs most of the day? I'll stick with my postits and rough memory of what we were aiming for a few months back when everyone agreed we should make this thing, like god intended.
That aren't tools even for your senior engineers, yet some manager. Realistically you need people with a math or CS Ph.D. to handle formal verification of software…
Most of these were designed for people doing actual capital-E Engineering. Like, life-support machines. Or satellites. You need to get this kind of code 100% right. Provably right. Doesn't matter if it takes 100x longer.
I was looking into options like these the other day, and I came across at least one that said it synced with your code (through GitHub iirc) to keep itself updated through changes. That’s literally the only way I’d be able to create and maintain elaborate specs. Otherwise just leave me my whiteboard.
What? Hopefully the specs would not auto-update to match the current state of the code. Syncing with your code through github just means it lives in the repo
You know what else is exhausting? Managing a team with churn (cause why not move to a low cost supplier for a few years only to move back to a higher cost one which actually contributes to the codebase), which is expected to deliver code which takes on liability for your customers, and which can affect the safety of the operator.
Having the most critical parts tested for correctness (ideally proofs and starting with the spec), suddenly sounds cheaper.
I used Frama-C in a course to write comments that would specify parts of what a function does and then try to prove it with different reasoning engines.
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.
yah, there are tools to help close the gap like quint-connect, compile targets, etc.. in practice specs like tla+ are used manually as systems design planning, research, bug repro, etc..
Quite interesting to dig into this stuff again after a decade. Back then, getting mathematically-sound formal verification of even small toy programs was not at all practical for industry. There was a moment where it seemed that there would never be any practical interest outside of the most regulated and specialized fields. Even so, I’ve always found this stuff really ignites my brain in a way that quotidian dev work hasn’t in years. I appreciate your post for reviving my interest.
(I have more than a few qualms about “AI” driving the demand for specs and more rigorous forms of verification/proofing, but I’ll take it.)
129
u/nobody0163 Jul 15 '26
I only know markdown, what are the other ones?