Вот только парочка их достижений:
-- 8700 строк верифицированного кода микроядра ОС (http://www.ok-labs.com/_assets/image_library/Klein_EHACDEEKNSTW_09.pdf). Очень интересный жизненный цикл получения этого кода (сам код на C, но прототип на Haskell. У меня складывается, что написание сразу двух эквивалентных программ на двух разных языках является сейчас магистральным направлением для хорошо верифицированных и надежных программ -- тот же Harold Lawson употребил этот прием для архитектуры Cy-Clone, коды которой писал на ассемблере, а исполнимые комментарии на чем-то типа Паскаля, а затем добивался одинакового исполнения кодов и комментариев -- "для проверки". Ребята из ERTOS потратили 2 человеко-года на написание Haskell-прототипа, и 2 человеко-месяца на переписывание его на С. И затем грохнули 20 человеко-лет на доказательство правильности кода -- 11 человеко-лет на само доказательство и 9 человеко-лет на инструментарий для этого доказательства. Т.е. стоимость "доказанного кода" идет к стоимости "недоказанного кода" примерно как 10:1).
-- автоматический синтез кода драйвера (при этом код получается верифицированным "по определению"): http://www.ok-labs.com/_assets/video_thumbs/Automatic_device%20driver_synthesis_with_Termite.pdf
Фирма, которая коммерциализирует эти теоретические результаты: http://www.ok-labs.com/
Еще они там хвастаются, что вышеприведенные два супердостижения -- это единственное за 42 года, что Австралия сумела презентовать на конференции ACM по операционным системам. Ага, Австралия. Вот фотография, например, автора статьи про синтез драйвера: http://www.e1os.org/rus/team.html. По русски он говорит не хуже нас с вами.
dz, когда мир (а не только русскоязычные коллеги) услышит про ваш Фантом (http://www.dz.ru/solutions/phantom)? 