Crate autokani 

Attribute Macros

extend_arbitrary

Extend the Arbitrary trait for target struct based on its constructor(e.g., new method). Add this attribute to the impl block of the struct.

kani_arbitrary

Impl Arbitrary for a struct by generating the any method based on the fields of the struct.

kani_test

Automatedly generate Kani one test harness for target function. The harness name is check_{function_name}.