There’s definitely some good patterns in here. Needs worked examples

I was hoping for a TLA+ example, but it never got there.

As a counterpoint, Dijkstra [0] makes a distinction between what he calls “postulational” and “operational” (more like what TFA is describing) formal methods. (Sidenote: I think people nowadays would use “denotational” instead of “postulational” (e.g. denotational vs. operational semantics), but Dijkstra wrote this in the 1980s)

Instead of thinking of a program as a set of potential execution traces, he advocated thinking of programs as formulas (e.g. pre/postconditions) that can be used to construct proofs without having to simulate any executions. His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties, reckoning that his way would be less work and result in more elegant programs.

I am just an amateur but it seems like formal methods as a whole is often conflated with model checking and other operational formal methods.

[0] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD101...