To be fair to Rust, the issue was an "unwrap" in the Rust code[0]. "unwrap" means "if the operation did not succeed then panic". Production Rust code should not use "unwrap", and should instead have logic to handle the failure case.
You don't need exotic formal verification methods to enforce this best practice. You just need a linter.
[0] https://blog.cloudflare.com/18-november-2025-outage/#memory-...