High-Fidelity Specification of Real-World Devices. - Liam Murphy 003; Albert Rizaldi; Lesley Rossouw; Chen George; James Treloar; Hammond Pearce; Miki Tanaka; Gernot Heiser (PLOS@SOSP, 2025)