Requested feature: Users should be able to specify and verify type safety invariants.
Use case: Users often encode safety of a type as a relationship between its internal variables, and Kani should provide a mechanism for users to specify the invariants and verify them.
Link to relevant documentation (Rust reference, Nomicon, RFC): https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html