These tools can take an extreme amount of time to use and require specialised skillsets that are difficult to hire for. They go far beyond standard software engineering practices like unit and E2E testing. It is genuinely, seriously not practical to verify the average startup's SaaS web app with TLA+; you'd go bankrupt.

Someone who's used them more than me might be able to comment on exactly how hard it would be, but I felt it was unfair to you not to explain.

Wait, code is not simple. Are the requirements simple? Oh wait, in reality they aren't simple either.

The complexity of the formal specification must ramp up with the complexity of the code, because the task being asked is complex.

So where does the debugging end if the specification is wrong?

How do you prove the requirements are correct?

Unit testing is helpful but wasn't the panacea, because the most important bugs are in integration.

I'm also going to guess that formal proofs will have hellacious issues with system boundaries. They can't prove correctness of the state on the other end of the pipe.

So you overcome that, time and money. What happens when the requirements/specification changes? How much of the verification is invalidated?

Proof systems need to prove their economic validity in the he software realm. Heck, where are the proof systems for subsections of the Linux kernel or other vitally important inner loops of computing? Those actually have stable specifications. Weren't go multitasking formally verified/provably correct in some sense? Why haven't correctness tools tackled other things?