This is sort of already possible in Rust when you use safe primitives (e.g., RefCell), but it doesn't cover unsafe code invoking Undefined Behavior. Placing something like Fil-C around unsafe code could prove to be interesting, especially since current approaches rely on interpretation (Miri, Soteria Rust) rather than translation.