Separation logic verification for Rust (Creusot-inspired, z4 backend) - View it on GitHub