In your blog, you mention the issue of state space explosion with Kani. This is true if you attempt to verify the entire function or library on its own. However, for model checking to work, it is necessary to decompose this library into components that can be verified on their own, then to shadow these components. This process is known as compositional verification.
Build contracts for each component. These contracts should include preconditions about every property required for a given input, and postconditions for every property expected for a given output, side-effect, data structure invariant, etc. Verify through Kani that each component fulfills these contracts. Then, substitute this component for a nondeterministic shadow component that also fulfills these contracts when verifying a component that composes this component. In this way, every function call is shadowed, and state can be kept small.
Next, you need to reduce the model check space to the minimum necessary to exercise each property. This means turning on unwind assertions and reducing the unwind set to the lowest number of iterations necessary to verify a property for any meaningful set of inputs. For example, how many real nodes in a binary tree are necessary to verify a balance operation? How many shadow nodes?
My rule of thumb for model checking C is that each model checking scenario should take a few seconds at most. Rust is more "dense", but still, you should be able to get each model checking scenario to run well under about 10 seconds.
In your blog, you mention the issue of state space explosion with Kani. This is true if you attempt to verify the entire function or library on its own. However, for model checking to work, it is necessary to decompose this library into components that can be verified on their own, then to shadow these components. This process is known as compositional verification.
Build contracts for each component. These contracts should include preconditions about every property required for a given input, and postconditions for every property expected for a given output, side-effect, data structure invariant, etc. Verify through Kani that each component fulfills these contracts. Then, substitute this component for a nondeterministic shadow component that also fulfills these contracts when verifying a component that composes this component. In this way, every function call is shadowed, and state can be kept small.
Next, you need to reduce the model check space to the minimum necessary to exercise each property. This means turning on unwind assertions and reducing the unwind set to the lowest number of iterations necessary to verify a property for any meaningful set of inputs. For example, how many real nodes in a binary tree are necessary to verify a balance operation? How many shadow nodes?
My rule of thumb for model checking C is that each model checking scenario should take a few seconds at most. Rust is more "dense", but still, you should be able to get each model checking scenario to run well under about 10 seconds.