The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification.

Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish.

I do see value in formal verification of IPC/threading communication primitives (locks, semaphores, queues, whatevs), but then formal verification usually require assumptions for hardware behavior and those aren't always correct, so. But I've never used formal methods outside exposure in an undergrad survey class, so I dunno.

Nitpick: You don't necessarily need any specification at all in order to reap benefits. Formal verification languages come with a lot of conditions that your program must fulfill in order to be accepted: Every loop terminates, every object you want to read/write is non-null, every list or array access is in bounds, etc.

For example, if you load an arbitrary C program into Frama-C, you'll have tons of properties to prove before you can even think of adding your own specification. The promises you get is that the program will always terminate and will never invoke undefined behavior. These properties are extremely useful, and these requirements are unlikely to change! And yes, C is... special. But pretty much any language has lists or arrays, nullable/option types, and unbounded loops. "No crashes/panics/uncaught exceptions" should be worth it.

And then, even absent a specification, you can start modeling invariants of the system anyway. This list is always sorted, this number is always strictly positive, this data structure never contains duplicate entries, etc. Anything that today would be a comment saying: "Important! The caller must ensure that..." This can help you gain confidence in your system. And if some day a requirement comes along that really requires you to violate one of these invariants, well, you can just remove it, the same way you would remove a test that no longer reflects something that should hold.

What we get typically is a second or third-hand summary of an analysis someone else did about how the current version works, with no indication of what stuff has to stay as-is in our replacement and what stuff can be improved.

At my last job, I got a formal specification for one project. But the implementation happened in parallel for time reasons, so by the time the spec was frozen, 90% of the code was written.