Thanks, this is for once in this thread, a real caveat in the application formal verification (or rigorous type systems). It's hard, it's not unlimited, and one may have fail to state crucial properties that matter in the first place.

Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.)

The cost may indeed be prohibitive, though.