There's a model checker that can directly verify Rust code, Kani https://model-checking.github.io/kani/ - I wonder if Servo could use it in this case?

Or maybe https://github.com/tokio-rs/loom