Is it really formal verification if the type system is unsound? Due to undefined behavior, a "proven pointer-to-int" may not end up being a valid pointer-to-int at runtime. Even in Haskell, the type system is actually logically inconsistent (see http://okmij.org/ftp/Haskell/impredicativity-bites.html).