Quis custodiet ipsos custodes?

Juvenal, (Satire VI, lines 347–8)

It’s been a while since I lectured about the formal construction of Java compilers and virtual machines. But nowadays, all the action has moved to an even more basic layer of the software infrastructure: the hypervisor, the core of the operating system virtual machine manager. But it’s just déjà-vu all over again, an instance of the eternal recurrence in the software world, since the first virtual machines originated at the operating system-level (IBM 360 Model 67). Even so, verification is still a key step to solve many Gordian knots, rooted in the same fashion of Thompson’s Reflections on Trusting Trust : from concurrency verification in Hyper‑V to the more advanced Typed Assembly Language and Proof-Carrying Code techniques.