A difficulty of formal verification is that specifying programs can be hard. Certain kinds of programs can end up having a specification that is as complex as the code itself. In this case it is better to focus on more interesting and understandable properties rather than an equivalence proof with a specification.
