Here’s an example how safety-critical C is written and formally verified: https://www.absint.com/

Based on what I know about Rust, it’s harder to write Rust to that same level of confidence, but I haven’t kept up with their safety-critical initiative.