Comment by afdbcreid

There is more than one formal verification library for Rust, although none is as integrated as SPARK I believe.