Verified Rust for low-level systems code