Don't Unwrap in Production: A Formal Verification Guide
TL;DR: On November 18, 2025, a single .unwrap() call caused a 3-hour global Cloudflare outage. Formal verification tools like Verus could have caught this at compile time—before it reached production. This post shows how Verus’s built-in specifications for Option::unwrap() and Result::unwrap() can mathematically prove panic-freedom, with working examples you can run today. The Bug On November 18, 2025, Cloudflare experienced a 3-hour global outage. The root cause? A panic in Rust code: ...