[Kata-hypervisor] Formal verification

Jessie Frazelle (TUPPERWARE) jessfraz at microsoft.com
Thu Jun 7 19:11:41 UTC 2018

I didn't want to fork the other thread too far off base but I was wondering if people had thought or implemented formal verification for hypervisors and if they could share any details.

Everything I've read on formal verification of hypervisors is purely from papers but not from industry so I am wondering if there are discrepancies between academia and industry here 

Thanks :)

More information about the Kata-hypervisor mailing list