I'm really surprised this isn't in SPARK considering security is a priority. Rust's type system still isn't capable of formal verification of lack of run-time errors... You know, considering security is a priority.