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?

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

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