the correctness proof of CompCert C guarantees that all safety properties verified on the source code automatically hold as well for the generated executable. На сайте компании не только компилятоп есть, но и статический анализатор, который проверяет исходник и safety properties
вообще как бы идея не самая плохая — вместо того чтобы как в судо или дуэз раздавать права правилами на запуск бинарников, раздавать правила на конкретные системные действия типа "смонтировать флешку" или "отправить компьютер в слип"
можно было бы даже вместо спайдерманки вкорячить quickjs от фабриса беллара, он гораздо быстрее и неинтерактивный. но за три года существования обеих проектов эта идея в голову пришла одному мне.
Помните, неделю назад я спрашивал, как в OpenBSD 6.9 настроить reply-to то pf. Всё поломалась, ничего не работает. Причём в прямом смысле этого слова. Во время грозы сгорели все три сетевушки.