> Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify tha

> Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify that code... Proofs can be written with incorrect assumptions (human error) in the same way that code can be written with incorrect assumptions. As one of the people in the article acknowledges, writing good proofs is challenging; "challenging" inescapably means "prone to human error". I think those statements are rather inaccurate, or at a minimum prone to erroneous interpretations. Formal verification is usually based on machine checked proofs. It doesn't matter how much error occurs in the creation of a proof, once it is checked it is known to be a valid proof with mathematical certainty. That does depend on the correctness of the proof checker, but in principle that can be formally verified as well. I think the main issues with formal verification lie elsewhere than where you seem to be placing them. Such as the problem that the specification itself may be incomplete or contain errors.