Not by far. Actually, the woman who co-invented software engineering in their Apollo program made one for achieving similar reliability if your specs are right at around $10,000 a seat. That and Cleanroom were in production use in the 1980's making low-defect software. Many others showed up afterward with plenty of application to commercial products or significant OSS software. Here's a few.
An early one, Cleanroom, that was often as cheap as normal development due to reduced debugging:
http://infohost.nmt.edu/~al/cseet-paper.html
Margaret Hamilton of Apollo started a company later to make the one below to embody the principles they used for correctness on Apollo. The papers section is also interesting.
http://www.htius.com/Product/Product.htm
Lots of companies applied the B method for things like railway verification. Many successes that cost nowhere near what NASA spent.
http://www.methode-b.com/wp-content/uploads/sites/7/2012/08/...
Altran-Praxis does formal specs, refinement, and provably-correct (wrt specs) code with 50% premium over normal development for their high-assurance stuff.
http://www.anthonyhall.org/c_by_c_secure_system.pdf
This mentions about three, different methods being used in products or experimental projects by defense contractors:
https://www.nsa.gov/resources/everyone/digital-media-center/...
COGENT is doing seL4-style verification at a fraction of its cost with filesytem paper showing how practical it is:
https://ts.data61.csiro.au/projects/TS/cogent.pml
Some companies are straight-up using logic programming to execute precise specs of how software should work on startup budgets:
https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf