Tutorial

NOTE: This tutorial expects you to have followed the Kani installation instructions first.

This tutorial will step you through a progression from simple to moderately complex tasks with Kani. It's meant to ensure you can get started, and see at least some simple examples of how typical proofs are structured. It will also teach you the basics of "debugging" proof harnesses, which mainly consists of diagnosing and resolving non-termination issues with the solver.

You may also want to read the Application section to better understand what Kani is and how it can be applied on real code.