Пока все используют нейросети, чтобы генерировать картинки или писать простенькие скрипты, я решил проверить: сможет ли ИИ стать штурманом в хардкорной математической верификации кода. Как итог — 185 доказанных модулей ядра и работающий на железе исследовательский прототип.
Что общего у сварщика и микроядра seL4? Ничего. Кроме одного человека, котор…