Post

Antithesis
@antithesis.com

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!)

youtu.beRetrofitting Proofs onto Existing Rust CodebasesIn 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…

0 reposts3 likes

Antithesis
@antithesis.com

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.