Towards a Formal Verification of the Bao Hypervisor

Hypervisors form the trusted foundation of modern embedded and safety-critical systems, yet few of them come with formal assurance. This paper reports on our ongoing effort to bring rigorous verification to Bao, a lightweight open-source static partitioning hypervisor. We contribute (i) a formal specification and SMT-based validator to automatically detect configuration errors, and (ii) a model checking framework to verify key implementation routines, focusing on Bao’s virtual memory subsystem that enforces isolation. Our compositional, contract-driven approach mitigates scalability issues and has already uncovered subtle flaws in the codebase. These results represent a significant step toward achieving practical industrial-grade assurance for hypervisors in real-time and mixed-criticality environments.