SOSP 2024 Digest
13 papers selected. Verus: A Practical Foundation for Systems Verification Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al. TL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency. Why notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date. ...