Конкретно в https://people.mpi-sws.org/~dreyer/papers/rustbelt... формально доказывается, что система типов Раста, владение, заимствование и прочее — корректны. Доказывается, что программа безопасна, если написана на безопасном подмножестве Раст. Доказывается, что программа безопасна, если в ней есть вкрапления unsafe, в которых программист не допустил ошибки, UB.
Кроме того, проект RustBelt на текущем этапе занимается формальной верификацией библиотеки std, но полная проверка требует времени. Поэтому библиотеку проверяют по кускам. Да, были найдены и исправлены 2 ошибки в unsafe коде (что показывает, что ребята делом занимались), тем не менее все эти thread, mutex, Arc/Rc формально безопасны.
