[kaba0]

Thanks for the informative answer!

Just a note, I (personally) don’t consider TLA+ a FV technique — it is a really good technique that actually scales much better than formal verification programs like Agda or Coq.

[hwayne]

It's formal verification of an abstract machine as opposed to running code. The problem is that formal methods as a field doesn't yet have a rich enough vocabulary to distinguish between its flavors. I use "code verification" and "design verification", which is a little more specific, but has its own issues.

Is TLA+ a sandwich?

[Y_Y]

> TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.

[kaba0]

But it only proves a model, not the actual code — that’s a major distinction.