Не совсем правда.
Вот есть seL4, не просто статистически проверено, но даже формально верифицировано.
Оно на 73% написана на С, https://github.com/seL4/seL4

Правда есть 2 существенных НО:
1. оно маленькое - там оклоло 36к строк на С, из которых 11к это пустые и комментарии (что уже намекает на сложность).
(с другой стороны микроядро и должно быть маленьким)
2. его писали руками, сразу думая о том как они будут его верифицировать.
Пришлось потрудиться и использовать Isabelle и Haskell.
Кол-во строк скриптов только первой было больше 200к строк.

И это было довольно дорого
The abstract spec took about 4 person months (pm) to develop. About 2 person years (py) went into the Haskell prototype (over all project phases), including design, documentation, coding, and testing.
The executable spec only required setting up the translator; this took 3 pm. The initial C translation was done in 3 weeks, in total the C implementation took about 2 pm, for a total cost of 2.2 py including the Haskell effort.
(статья https://cseweb.ucsd.edu/~dstefan/cse227-spring20/papers/sel4...)