Yes, formal methods can be useful, they help uncover bugs. It's a debugging tool, albeit a very demanding one. For some software, it makes sense to use it. Rea

Yes, formal methods can be useful, they help uncover bugs. It's a debugging tool, albeit a very demanding one. For some software, it makes sense to use it. Real deployment of VMs has larger problems with security than not formally verified hypervisor so I think the answer for most hosting companies is "the juice is not worth the squeeze" here, the squeeze being the restriction to academic verified design. Hosting VMs is mostly about features and reliability. Those who need also real security, will host on their own HW and won't allow foreign VMs, so formally verified hypervisor is less of a requirement there too. It's a "nice to have".