> Poor man's runtime "dynamic" version. AKA: A much worse version.

Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.

My rcc C compiler has a compile-time contracts and range/interval prover also. Needs -O3.

For full formal proofs it's easier to use cbmc or esbmc though