Недавно на Github появился репозиторий операционной системы Gloire. Gloire использует ядро Ironclad,написанное на языке программирования Ada, и пользовательское окружение GNU. На сайте, посвященном Ironclad, написано что оно находится в процессе «формальной верификации».
( читать дальше… )