You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specification

You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on. https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev