Good as DBC/assertions are, it absolutely does not "approach the robustness of formal verification in practice" especially for potentially large states.
Also DBC/assertions are of little value unless you provide test code to exercise that asserted section, so that's more work, unless you're ok with the assertion triggering by the user after you've shipped it.
Also comprehensively asserted code (with assertions switched on / compiled in) can absolutely crawl because preconditions that formal verification ensures have to be repeatedly checked at runtime - that's your assertion being run ten thousand times instead of being known-true in the code.
It is very good, I use it extensively, but it is not even comparable to formal proofs. Nowhere near.
Also DBC/assertions are of little value unless you provide test code to exercise that asserted section, so that's more work, unless you're ok with the assertion triggering by the user after you've shipped it.
Also comprehensively asserted code (with assertions switched on / compiled in) can absolutely crawl because preconditions that formal verification ensures have to be repeatedly checked at runtime - that's your assertion being run ten thousand times instead of being known-true in the code.
It is very good, I use it extensively, but it is not even comparable to formal proofs. Nowhere near.