Like other tools, Kani comes with some limitations. In some cases, these limitations are inherent because of the techniques it's based on, or the undecidability of the properties that Kani seeks to prove. 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: