Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic

Hoang-Hai Dang, Gregory Malecha

We present the current progress of specifying and verifying the NOVA microhypervisor at BlueRock Security. We carry out these tasks using the BRiCk C++ program logic and verification tools, building on top of the Iris framework for concurrent separation logics (CSLs), in Rocq. We found that the use of CSLs has enabled us to carry out highly modular specifications and verifications of even sophisticated, fine-grained concurrent algorithms in NOVA. We believe this is a significant step forward over other hypervisor verification projects that are either limited to single-threaded verification or are highly non-modular.

rocq c++ program verification separation logic brick concurrency nova hypervisor skylabs-ai bluerock-security

paper conference link talk

@inproceedings{dang2026-specifying-and-verifying-nova,
  title={Specifying and {V}erifying the {NOVA} {M}icrohypervisor in {C}oncurrent {S}eparation {L}ogic},
  author="Hoang-Hai Dang and Gregory Malecha",
  booktitle={Rocq for Programming Languages 2026},
  location={online},
  year="2026",
  month="January"
}