This paper explores the combination of lightweight formal methods and agentic AI, specifically to find bugs in a production security-critical hypervisor. Building on the executable-specification framework of Memarian et al.\ for the Android pKVM hypervisor, we use an OpenAI Codex-based agent to write and refine specifications, expressed in the ambient C programming language, for a recent version of pKVM. We use this for bug-finding, with encouraging preliminary results: the agent found four previously unknown and substantial bugs, including violations of the intended page-ownership discipline and bugs that can lead to guest-memory leakage or hypervisor memory corruption. Interestingly, all the bugs claimed by the agent to be serious were actual bugs, without false positives, and the experiment needed less than one month of human work with a ChatGPT Pro subscription.