For distributed systems this makes sense. Most people aren't writing distributed system components though but things where the risk usually isn't technical like business software. I worked on a project where I got into arguments with the PMs because I pushed back on optimizing performance on the main page of our pre-launch product. I argued that we don't have any real feedback that the page is what is needed and the PM thought I was insane for doubting the main page was needed. We completely redesigned that page twice, deleted it entirely and then had to bring it back because the sales team liked it for initial demos.
Every process is a tradeoff and it anyways depends on your specific circumstances which choice is best for your team and project.
Is it absolutely important that your system is correct? ... begs the question, correct with respect to what? Generally: a specification.
There are lots of situations where you don't know what your system is supposed to do, where testing a few examples is sufficient, or it's not terribly important that you know that it does what you say it ought to. Generating a batch report or storing some customer responses in a database? Trust the framework, write a few tests if you need to, nobody is going to find a formal specification valuable here.
However, if you need to deploy configuration to a cluster and need to ensure there is at least two nodes with the a version of the configuration that matches the database in the load balancer group at all times during the migration? Need to make sure the migration always completes and never leaves the cluster in a bad state?
Even smaller in scale: need to make sure that references in your allocator don't contain addresses outside of your memory pool? Need to make sure that all locks are eventually released?
It's definitely much faster to iterate on a formal specification first. A model checker executes your model against the entire state space. If you're used to test-driven development or working in a statically typed language, this is useful feedback to get early on in the design process.
What the scope is that is appropriate for using tools like this is quite large and not as niche as some folks imply. I don't do aerospace engineering but I've used TLA+ to model deployment scripts and find bugs in OpenStack deployments, as well as to simply learn that the design of certain async libraries are sound.
Every process is a tradeoff and it anyways depends on your specific circumstances which choice is best for your team and project.