Combining Type Checking and Formal Verification for Lightweight OS Correctness

Ramla Ijaz, Kevin Boos, Lin Zhong

This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust OS, Theseus. First, we report new developments in intralingual design that…