Jan 17, 2026
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
