1. 1. Getting started
   1. 1.1. Installation
      1. 1.1.1. Building from source
      2. 1.1.2. GitHub CI Action
   2. 1.2. Using Kani
   3. 1.3. Verification results
2. 2. Crates Documentation
3. 3. Tutorial
   1. 3.1. First steps
   2. 3.2. Failures that Kani can spot
   3. 3.3. Loop unwinding
   4. 3.4. Nondeterministic variables
4. 4. Reference
   1. 4.1. Arbitrary Trait
   2. 4.2. Attributes
   3. 4.3. Bounded Non-deterministic variables
   4. 4.4. List Kani Metadata
   5. 4.5. Experimental features
      1. 4.5.1. Automatic Harness Generation
      2. 4.5.2. Coverage
      3. 4.5.3. Stubbing
      4. 4.5.4. Contracts
      5. 4.5.5. Loop Contracts
      6. 4.5.6. Concrete Playback
      7. 4.5.7. Quantifiers
5. 5. Application
   1. 5.1. Comparison with other tools
   2. 5.2. Where to start on real code
   3. 5.3. Debugging slow proofs
6. 6. Developer documentation
   1. 6.1. Coding conventions
   2. 6.2. Working with CBMC
   3. 6.3. Working with rustc
   4. 6.4. Migrating to StableMIR
   5. 6.5. Command cheat sheets
   6. 6.6. Testing
      1. 6.6.1. Regression testing
   7. 6.7. Performance comparisons
      1. 6.7.1. benchcomp command line
      2. 6.7.2. benchcomp configuration file
      3. 6.7.3. Custom parsers
   8. 6.8. Profiling Kani
7. 7. Limitations
   1. 7.1. Undefined behaviour
   2. 7.2. Rust feature support
      1. 7.2.1. Intrinsics
      2. 7.2.2. Unstable features
   3. 7.3. Overrides
10. 8. FAQ