and you can use MIRAI, that takes the contracts defined by this crate and check them at compile time

or, use prusti, that has contracts with a similar syntax checked at compile time as well