Creusot is a deductive verifier for Rust code that translates to WhyML, the verification and specification language of Why3 https://github.com/creusot-rs/creusot @rustlang #Formal #Verification