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