Don't Unwrap in Production: A Formal Verification Guide
TL;DR: On November 18, 2025, Cloudflare had a ~3-hour global outage that traced back to a Rust panic triggered by a single .unwrap(). Tools like Verus can force you to prove that an unwrap() can’t panic before code ships. This post explains how Verus’s built-in specs for Option::unwrap() and Result::unwrap() work, with examples you can run today. The Bug On November 18, 2025, Cloudflare experienced a ~3-hour global outage. The immediate cause was a panic in Rust code that looked totally reasonable in a quick review: ...