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.