alt Hacker NewsYou're responding to a comment where I wrote that I would never use Xen with an argument not to use Xen. All I'm saying is that "formal verification", at least as it exists in current systems, is not why I wouldn't use Xen.
You're responding to a comment where I wrote that I would never use Xen with an argument not to use Xen. All I'm saying is that "formal verification", at least as it exists in current systems, is not why I wouldn't use Xen.
> an argument not to use Xen
Not my intent but perhaps I communicated poorly. It was an argument that the -reason- Xen has had so many bugs is because it was not built for correctness.
Formal verification should be a bare minimum for a TCB component to know many classes of bugs that have plagued the most popular hypervisors cannot happen.
We both clearly agree not to use Xen.
Anyway, I appreciate the engagement on this all the same.
Few even know alternatives to xen exist!