Crate kani

source ·



  • This module introduces the Arbitrary trait as well as implementation for primitive types and other std containers.
  • Kani implementation of function contracts.
  • This module contains functions to work with futures (and async/.await) in Kani.
  • This module contains functions useful for checking unsafe memory access.
  • Support for arbitrary tuples where each element implements kani::Arbitrary. Tuples of size up to 12 are supported in this file.


  • A macro to check if a condition is satisfiable at a specific location in the code.
  • implies!(premise => conclusion) means that if the premise is true, so must be the conclusion.


  • This creates an symbolic valid value of type T. You can assign the return value of this function to a variable that you want to make symbolic.
  • This creates a symbolic valid value of type T. The value is constrained to be a value accepted by the predicate passed to the filter. You can assign the return value of this function to a variable that you want to make symbolic.
  • Creates an assertion of the specified condition and message.
  • Creates an assumption that will be valid after this statement run. Note that the assumption will only be applied for paths that follow the assumption. If the assumption doesn’t hold, the program will exit successfully.
  • NOP concrete_playback for type checking during verification mode.
  • Creates a cover property with the specified condition and message.

Attribute Macros§

  • Add a postcondition to this function.
  • Declaration of an explicit write-set for the annotated function.
  • Marks a Kani proof harness
  • Designates this function as a harness to check a function contract.
  • Specifies that a function contains recursion for contract instrumentation.**
  • Add a precondition to this function.
  • Specifies that a proof harness is expected to panic.**
  • Select the SAT solver to use with CBMC for this harness
  • Specify a function/method stub pair to use for proof harness
  • stub_verified(TARGET) is a harness attribute (to be used on proof or proof_for_contract function) that replaces all occurrences of TARGET reachable from this harness with a stub generated from the contract on TARGET.
  • Set Loop unwind limit for proof harnesses The attribute #[kani::unwind(arg)] can only be called alongside #[kani::proof]. arg - Takes in a integer value (u32) that represents the unwind value for the harness.

Derive Macros§

  • Allow users to auto generate Arbitrary implementations by using #[derive(Arbitrary)] macro.