The problem with formal methods is that any useful program must interact with its environment (customers, filesystems, networks, sensors etc) in order to make a difference, and nobody is able to capture, comprehend or relate to the full specifications of those items and their subsystems. This results of proofs based on a lot of incorrect and incomplete assumptions.

This problem apparently even extends to the model-checking software itself, resulting in systems reported to be correct when then network message saying it is flawed was lost:

https://blog.acolyer.org/2017/05/29/an-empirical-study-on-th...