Post

Verus is a formal verification tool for code written in Rust. It's one of the most exciting directions in formal methods today, because it checks the executable code, not just a specification. (Our recent blog post explains why this matters!)

Jay Lorch and Chris Hawblitzel at Microsoft Research are two of the central contributors to Verus, and they join us today to wrap up this season of the Bug Bash podcast. They spoke to Shuxian Wang about how Verus works, how it was built, and, of course, what LLMs will do for formal methods.