You may be interested in applying Kani if you're in this situation:

  1. You're working on a moderately important project in Rust.
  2. You've already invested heavily in testing to ensure correctness.
  3. You want to invest further, to gain a much higher degree of assurance.

If you haven't already, we also recommend techniques like property testing and fuzzing (e.g. with bolero). These yield good results, are very cheap to apply, and are often easy to adopt and debug.

In this section, we explain how Kani compares with other tools and suggest where to start applying Kani in real code.