IRONSIDES uses SPARK to show freedom of exceptions or single-packet DOS. A translation to Rust would probably preserve most of those properties. I also thought a parallel development between Ada2012/SPARK and Rust would be interesting to see if one set of checkers catch something another misses in same piece of software.
http://ironsides.martincarlisle.com/
IRONSIDES uses SPARK to show freedom of exceptions or single-packet DOS. A translation to Rust would probably preserve most of those properties. I also thought a parallel development between Ada2012/SPARK and Rust would be interesting to see if one set of checkers catch something another misses in same piece of software.