Add verification using Kani

[Lol3rrr]

Hey there,

I wanted to use kani to verify certain parts of my codebase, which uses this crate (among others). Would this project be open to accept contributions to add verification using kani?

I have not yet started on this and dont want to make any false promises, but would love some feedback or input from others on this.

Rough Goal / Motivation

My main goal with this would be to add function contracts to a variety of functions to make verification of code using this crate easier as they can avoid the actual implementation and rely on the contracts.

I don't really expect to find any issues.

[cuviper]

I have no experience with kani, so I don't know how burdensome this would be. If it can be added without adding much maintenance overhead, that's probably fine, especially if it does uncover any issues.