Lots of talk about formal methods, but I think the high order bit would be for unsafe code to use debug_assert! to check its preconditions.

Right now it doesn't, because of rather silly technical reasons regarding how libcore is built and tested.