Most real world systems would be practically impossible to even write a formal specification for, much less actually prove that the system follows it correctly.