rust verification tools

2022-01-13 ยท 1 min read

Rudra #


Rudra is a static analyzer to detect common undefined behaviors in Rust programs. It is capable of analyzing single Rust packages as well as all the packages on

Prusti #


Prusti is a prototype verifier for Rust, built upon the Viper verification infrastructure.

By default Prusti verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable. Overflow checking can be disabled with a configuration flag, treating all integers as unbounded. In Prusti, the functional behaviour of a function can be specified by using annotations, among which are preconditions, postconditions, and loop invariants. The tool checks them, reporting error messages when the code does not adhere to the provided specification.



MIRAI is an abstract interpreter for the Rust compiler's mid-level intermediate representation (MIR). It is intended to become a widely used static analysis tool for Rust.