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, in

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.