A gentle introduction to checking code correctness in Verus
I'm going to talk about the tool we've been building, called Verus, which is a tool to verify Rust, and specifically to verify Rust code in the domain of system software: operating systems, file systems, things like that.