A methodology for giving operating-system code correctness guarantees at reduced proof cost by combining a language's type system with formal verification. Building on Theseus OS's intralingual design in Rust, it uses linear-type 'representations' as sole-accessors to resources, linear-type proof-of-work to enforce operation ordering, and an intralingual hardware abstraction layer; recognizing that ownership cannot prevent overlap between two instances of the same linear type, it adds type-checkable intralingual specifications and applies formal verification only where the type system cannot reach, trading slightly weaker guarantees for substantially less proof effort (demonstrated on a memory subsystem and a 10 GbE driver).
This cs.OS experience paper reports lightweight correctness techniques for Theseus, an open-source Rust operating system. It advances 'intralingual design' - using the language's type system to enfor…