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.
I don’t know why anyone thinks that you can’t or shouldn’t use unwrap in a production environment. If this was enforced you’d likely end up with people using something like “.expect()” and there are real world cases where you KNOW that unwrapping will never cause issues.
The reality is the code should not have used unwrap, but that doesn’t mean using unwrap is bad.
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-...