Best way to formally verify Rust code for real programs. I use Verus because it just works with Rust repos already, no runtime cost, and fully OSS. You keep Rust’s good memory management, tooling support and performance. The spec is just Rust: fn octuple(x: i8) -> (r: i8) requires -16 <= x < 16, ensures r == 8 * x, `requires` is what every caller must promise. `ensures` is what you get back. Verus proves the body of the function keeps that promise for every input that adheres to `requires`. That formal spec is then removed when compiling so the runtime is not impacted. There’s a Verus playground you can use in your browser and multiple guides that come alongside the OSS repo. I highly recommend you invest time to play with this with your coding agent because it will open your mind to some insane possibilities that work with distributed systems, concurrency, memory constraints, etc. today. Reminder to not vibe verify, check your formal specs. Literally just go and explore, it’s available now. This doesn’t promise ‘bug free’ overall, it promises hardening. I’ll talk more about how to further harden in the future. Follow me for more on verification and agentic engineering.