Note however that the page does list a bunch of useful, completely[1] verified components just below that sentence. [1] Modulo things like the correctness of t

Note however that the page does list a bunch of useful, completely[1] verified components just below that sentence. [1] Modulo things like the correctness of their C semantics, assembly semantics, various extraction procedures.