Retrofitting Proofs onto Existing Rust Codebases

In this episode we sit down with Jay Lorch and Chris Hawblitzel from Microsoft Research, along with Sr Engineer Shuxian Wang from Antithesis, all to talk about Verus. We break down how to retrofit proofs onto code you have already shipped, without starting over from scratch. Learn how modern SMT solvers check your code at compile time, why Rust ownership maps naturally to separation logic, and what happens when AI coding agents try to cheat their way through mathematical proofs.