[Kata-hypervisor] Formal verification

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 :)