I suspect those sort of liveness properties (and likely some safety properties in unsafe code) cannot be encoded in Rust's type system and you'd have to use a m

I suspect those sort of liveness properties (and likely some safety properties in unsafe code) cannot be encoded in Rust's type system and you'd have to use a model checker at some point. Still, it's cool to see such a system used and providing immediate benefits. Happy hacking!