Yeah, all I'm saying is that I agree with you about Xen, but that I don't agree about the centrality of formal methods --- at least on current projects with current verifications, things could get different now that AI lets us be more ambitious with verification --- in determining attack surface.

Generally, the less your OS can do, apart from strictly hypervising guest operating systems, the safer you probably are. Hence why people do things like seL4.