Yeah, I think so as well. Limit of formal proofs is reality. Even seemingly simple stuff is super complex and interacts with a plethora of other things. And your conclusion will only ever be as good as the model / specifications you put in. When doing the maths on a crypto algorithm... Have you thought of people whipping out their multimeter to probe the power consumption of the CPU and subsequently work their way back to the secret? Have you favored in everything else that exists on the world, or potentially could exist? If not, your result just won't line up with reality as it is out there.

Formal proofs are very, very good if you made up the parameters. But good luck formalizing reality once it gets down to applied stuff... I mean it's still useful and helps make things better. But it's not like airplane systems don't fail anymore after we've come to do formal proofs on the subsystems. It's just too complex and the real world is involved.