Model checking, for example, is not as hard as it sounds and not nearly as expensive or time consuming as building the wrong thing. Most programmers I’ve taught don’t seem to have too much difficulty learning TLA+ or Alloy. The concepts themselves are fundamentally rather simple.
Theorem proving does take some expertise. But it’s also not an insurmountable obstacle.
However I agree that there’s a spectrum of cost and the higher you go down the assurance chain the effort and time it will take. Often we do price in the cost of errors into the holistic process of software (eg: SRE style error budgets, iterative development, etc).
One angle that works for me when deciding when to use a more substantial FM is the cost of getting it wrong (or conversely, how important is it that we get some key thing right)?
If I’m building a financial database can my business afford to lose customers’ money? Do we have that liability built into our insurance?
Sometimes you need to go slow at first in order to go fast later.
And some properties are simply too hard to trust to some boxes and arrows and a prayer.