The correctness proof idea sounds intriguing. Ada does this already yes?

And do you have any examples of where UB from unsafe rust leaks to outside the program? Surely you would look back at the unsafe code always to fix it.