Открыты исходники seL4!
General Dynamics C4 Systems и NICTA рады объявить об открытии исходных кодов seL4 — первого в мире ядра операционной системы с доказанной корректностью:
бинарный код микроядра seL4 правильно реализует поведение, описанное в его абстрактной спецификации; данные не могут быть изменены либо прочитаны без разрешения; ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации. Теперь же дополнительно показана двоичная корректность. Исходные коды доступны для широкой публики на github.
isabelle, l4
