Is there a benefit to formally verified C over formally verified Rust? Maybe platform support?