Jan-Oliver Kaiser

Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming

Derek Dreyer, Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Hoang-Hai Dang, Jan-Oliver Kaiser

The MPI for Software Systems' "Rust Belt" project applies decades of academic research to formally verify the safety guarantees of the Rust programming language against the risks posed by "unsafe" code. By leveraging the Iris framework and mechanizing proofs in the Coq assistant, the team establishes a semantic safety model that independently verifies complex libraries like `Arc` and `Mutex`, successfully identifying critical bugs in memory ordering and reference counting. This methodology ensures that future language evolution and standard library modifications can proceed with mathematical certainty that undefined behavior remains impossible.