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?
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.