Прорыв значительным образом повлияет на повышение надёжности критических систем, таких как медицинское оборудование, военное, авиационное, где ошибки в ПО могут иметь катастрофические последствия. "По приблизительной оценке качественно разработанное программное обеспечение имеет около 10 ошибок на тысячу строк кода, а очень качественное – от 1 до 3, - поясняет Хайзер. Это означает, что в системах множество недочётов. Мы же показали возможность добиться намного меньшего, предельного уровня, причём наиболее подверженная риску часть имеет доказанную отказоустойчивость. Я думаю, не будет преувеличением сказать, что это открывает совершенно новый мир для создания систем с высокими показателями надёжности и безопасности".

Проверка ядра, известного как микроядро seL4, включала математическое доказательство корректности 7500 строк программного кода, занимались которым шесть человек в течение более чем пяти лет. "Команда NICTA добилась переломного результата, который изменит подход к критическому с точки зрения безопасности ПО, - продолжает профессор. – Верификация окончательно подтвердила возможность существования кода без ошибок, и в будущем ничто менее передовое не должно признаваться приемлемым в особо важных приложениях".