May 25, 2026
MicroVMM: AI-Assisted Verification-Oriented Virtual Machine Monitor
Thanh Do
Modern agentic systems increasingly execute untrusted AI-generated code inside lightweight sandboxing environments. While many existing sandboxes rely on operating-system namespaces, recent advances in autonomous vulnerability discovery have exposed weaknesses in these traditional isolation boundaries. At the same time, vulnerabilities in virtualization infrastructure itself demonstrate that lightweight VMMs remain difficult to reason about formally due to complex shared-memory device protocols such as VirtIO. This project explores whether AI-assisted workflows can help construct formally analyzable virtualization software centered around explicit protocol invariants. Motivated by CVE-2026-5747, we derive queue lifecycle invariants from the vulnerability and construct a minimal verification-oriented VMM in Lean 4. We define abstract operational semantics for queue lifecycle behavior and establish refinement proofs connecting executable implementation behavior to the abstract model. The resulting system proves several safety properties, including post-activation queue immutability, directly eliminating the motivating vulnerability class within the modeled semantics. Our results suggest that AI-assisted development workflows can reduce the engineering complexity of refinement-oriented systems verification when combined with intentionally verification-oriented architectural design.
No reviews are available yet
Cite this work
@misc {
title={
(HckPrj) MicroVMM: AI-Assisted Verification-Oriented Virtual Machine Monitor
},
author={
Thanh Do
},
date={
5/25/26
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


