Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other methods too, without the burden of formal verification.

Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.

I know of at least three:

Hamilton's 001 Tool Suite http://htius.com/

Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html

Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf

All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time.

There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two:

http://www.missioncriticalit.com/technology.html

https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf

Which is great given they're precise statements about what you want to do that are easier for humans and computers to analyze. They don't have the language-level problems either. Tools can then turn those into code or do much of the work from there.

If your spec is wrong, your code will be wrong anyway. More often, people use the code as the spec which is IMHO (for this kind of programing) really bad.