Колумбийский университет в Нью-Йорке заявил о разработке «устойчивой к взлому» системы облачного ПО

Предположим, что мат.модель верификации гипервизора корректна, полна, и описывает все аспекты функционирования (API в сторону ОС, корректная работа с железом, корректная архитектура). Для формального доказательства корректности исполнения гипервизора необходимо ещё наличие верифицированного компилятора и верифицированной платформы исполнения.
Предположим, верифицированный компилятор существует (несколько реализаций ADA), но о верифицированных платформах я не слышал…
Работу, конечно, проделали коллосальную, но во многом — бессмысленную.