I think you're conflating three issues. One is of course unsafe native code, which could at least in part be fixed by picking a different programming language (

I think you're conflating three issues. One is of course unsafe native code, which could at least in part be fixed by picking a different programming language (cough Rust) that has stronger guarantees. Another is correctness of the implementation with regard to the specification. That is a lot more difficult to verify, and understandably a very big security concern. Third is the security of of the specification itself, which might be easier to prove, but is still no simple feat.