As explained in Comparison with other tools, Kani is based on a technique called model checking, which verifies a program without actually executing it. It does so through encoding the program and analyzing the encoded version. The encoding process often requires "modeling" some of the library functions to make them suitable for analysis. Typical examples of functionality that requires modeling are system calls and I/O operations. In some cases, Kani performs such encoding through overriding some of the definitions in the Rust standard library.

The following table lists some of the symbols that Kani overrides and a description of their behavior compared to the std versions:

assert, assert_eq, and assert_ne macrosSkips string formatting code, generates a more informative message and performs some instrumentation
debug_assert, debug_assert_eq, and debug_assert_ne macrosRewrites as equivalent assert* macro
print, eprint, println, and eprintln macrosSkips string formatting and I/O operations
unreachable macroSkips string formatting and invokes panic!()
std::process::{abort, exit} functionsInvokes panic!() to abort the execution