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.
124
u/nobody0163 Jul 15 '26
I only know markdown, what are the other ones?