Isn't this just an extension of design by contract? What advantages come from using a framework like this instead of traditional assertions for contracts?
It is indeed just an extension of that very idea, developed at the same institution where design-by-contract has been introduced a few decades ago.
However, instead of crashing at runtime due to a failed assertion, you get a guarantee that your program will in fact not violate said assertions and behave correctly.
It also entails a nice speed bonus, instead of checking the assertions all the time, which could be quite a complex feat for non-trivial post-conditions, you do it once, symbolically, for all possible executions.
