Comment by mafribe

Since there is often a misconception that formally verified software must be absolutely free from problems, from the conclusion of the paper: "Extensive testing on formally verified software is necessary for at least two reasons. First, the formal specification may not guarantee all the properties expected by users, but only critical ones (e.g. no miscompilation for CompCert). Second, critical bugs may still remain, because the formal specification might not exactly fit reality. However, in this case, critical bugs are in the—much smaller and simpler—[trusted computing base]"