> что-то у Вас не сходится - Вы сами пишете, что верификация, которая
> выполнялась для Haskel-а, а уже потом был перевод на C, заняла 20 лет.

У тех, кто лишь ту новость и читал, но ни по каким сылкам не ходил:
http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
> The overallsize of the proof,including framework, libraries, and generated proofs (not shown in the table)is 200,000 lines of Isabelle script.
> The abstract spec took about 4 person months to develop
> About 2 person years (py) went into Haskell prototype

...
> The initial C translation was donein 3 weeks, in total the C implementation took about 2 pm,for a total costof 2.2 py including the Haskell effort.

...
> The cost of the proof is higher,in total about 20 py.

и с верификацией знаком лишь из заголовка новости - все может быть.