Use static verifier kani in our test?

[NobodyXu]

kani can verify that unsafe code does not have:

• Memory safety (e.g., null pointer dereferences)
• User-specified assertions (i.e., assert!(...))
• The absence of panics (e.g., unwrap() on None values)
• The absence of some types of unexpected behavior (e.g., arithmetic overflows)

[ParkMyCar]

Hey @NobodyXu! Very sorry I didn't respond to this earlier. I'm open to using kani, would you be able to put up a proof of concept PR?

[NobodyXu]

Sure

[NobodyXu]

Sorry I've been busy, I probably won't have the time for a proof of concept PR.

[ParkMyCar]

No problem :) I'll keep it open for now in case someone else wants to give it a shot