Like other tools, Kani comes with some limitations. In some cases, these limitations are inherent because of the techniques it's based on. In other cases, it's just a matter of time and effort to remove these limitations (e.g., specific unsupported Rust language features).

In this chapter, we do the following to document these limitations: