Not who you asked but I took a quick look.
Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.
At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use.
I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.
Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++.
See for example Can C++ be made as safe as SPARK? - https://www.eschertech.com/papers/index.php which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.eschertech.com/2025/09/09/contracts-have-ar...
Also see articles under Proving C and C++ programs correct - https://www.eschertech.com/articles/index.php
Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961