Even formal verification misses visible behaviors, the line is just a little farther down. Correct runtime visible behavior can also include side effects like the amount of time taken (e.g. constant time cryptography), or even the amount of heat generated [0]. You're not going to encode everything you could possibly want in a type system without modeling the entire universe, so draw an opinionated line somewhere reasonable and be happy with it.

[0] https://news.ycombinator.com/item?id=39751509#39761349