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:
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