Refinement type verification for Rust (Verus-inspired, z4 backend) - View it on GitHub