В статье рассказывается о недавних достижениях на пути к строгой верификации промышленных операционных систем (ОС). Под промышленной ОС имеется в виду система, активно используемая в некоторой области, развиваемая и сопровождаемая на протяжении значительного времени. Статья не касается исследовательских ОС, разработанных обычно с целью проверки некоторых идей. Рассматривается декомпозиция задача верификации ОС на подзадачи верификации ее различных частей и отдельных свойств и применение для этого разнообразных методов верификации. В статье делается попытка описать и осмыслить опыт, полученный в рамках нескольких проектов по верификации различных частей ОС в ИСП РАН.