Do you use the Cargo "contracts" for Design-by-Contract style invariants that plugs into Facebook's MIRAI prover thing? I always thought it this was super neat

Do you use the Cargo "contracts" for Design-by-Contract style invariants that plugs into Facebook's MIRAI prover thing? I always thought it this was super neat: https://crates.io/crates/contracts https://crates.io/crates/contracts https://github.com/facebookexperimental/MIRAI/blob/main/examples/shopping_cart/src/main.rs https://github.com/facebookexperimental/MIRAI/blob/main/exam... [dependencies] mirai-annotations = ... contracts = {version = "XXX", features = ["mirai_assertions"]}