Как вычислялась эта метрика?

Даже если иметь кривые руки, плохую голову и что-то натянуть против раста, то верификация unsafe в его собственных библиотеках потребует в разы меньше усилий чем верификация сишных библиотек со сравнимым функционалом.

В среднем по больнице, unsafe-код в Rust более регулярен и проще (менее комплексный) чем подобный в сишных библиотеках.

Есть и обратный эффект, в unsafe-функциях концентрация странностей/мутностей больше чем в средней glibc. Но это только потому, что в rust есть возможность и стремление отделять мух от котлет, а в glibc любые unsafe операции могут быть в любом месте (в самом безобидном и неожиданном).

Конечно, можно найти зубодробительные unsafe-сценарии, но тогда и сравнивать их надо с аналогичными сишными случаями.

Нисколько не хочу принизить ценность проекта и достигнутые там результаты, но всё-таки нужно слегка критично читать написанное с осознанием всего комплекса проблем/задач.

Формальная/математическая верификация покрывает часть функционала, т.е. "не всё".
При этом возникает некая проблема/задача верификации "самого верификатора", т.е. доказательства что сформированного списка свойств достаточно для "верифицированного компилятора".

Например, предположим что у вас есть "верифицированный компилятор". В нём могут быть баги ?
- если "нет, багов быть не может", то упомянутый компилятор нельзя назвать верифицированным.
- если "да, баги могут быть", то верификация перестаёт что-либо гарантировать на практике.

Поэтому все подобные верификации всегда с массой уточнений и оговорок "тут рыбу заворачивали, сюда не смотрим" и "если остальное работает верно".
Соответственно, отсутствие "формализированной системы типов" им не только не мешает, но и может помогать (сокращать поверхность).

Им пришлось написать самописный null_mute, модифицировать transmute() подменив там crate::null_mut на самописный... и даже после этого получается ошибка компиляции

error[E0133]: dereference of raw pointer is unsafe and requires unsafe function or block
error: could not compile 'cve-rs' (lib) due to previous error

Кекспертизм опеннетный, аз из
Да и то, что для появления проблем (т.е. чтобы найти баг в компиляторе - ведь "работатет" оно только с кастомным null/transmute) там целый консилиум корпел не одну неделю (см. обсуждение на гитхабе) - кексперты скромненько умалчивают.
И правда, какая разница: заиметь UB после траха^W написания кастомного null и принудительного каста типа данных - или заиметь UB, просто сложив два числа или забыв пустую строку в конце исходника ...