[mr_00ff00]

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.

[dist1ll]

There is a huge body of work around proof-based programming.

If you're looking for a full blown SMT solver and general purpose dependently-typed PL have a look at F*

https://fstar-lang.org