Hola
Que esté corriendo un OS o el hipervisor tiene que ver con:
(* Execution Modes *)
Inductive exec_mode := usr | svc.
Inductive os_activity := running | waiting.
Cuando el estado del sistema está en estado waiting, el que corre es el hipervisor.
Saludos, Carlos