While zerocopy is conceptually complex, the amount of code that executes in order to perform a particular operation is often very small. This makes it a perfect target for formal modeling and verification techniques.

This issue tracks testing or proving the correctness of our core algorithms using these tools.

Currently, we use formal modeling or verification in the following places (TODO: better way to keep this list up-to-date automatically?):

• [ci] Run byteorder tests under Kani #394
• Prove correctness of layout len utilities with kani #402