I was involved in formal verification at UC Davis back in 1993, and I'm sure it started before that. And yet we still can't do it effectively all these years later. The language lab was using HOL (higher order logic), us security geeks were using BAN (Burrows-Abadi-Needham logic). BAN logic turned out to have problems and GNY logic was supposed to fix those, but it had problems too... all those logics were failing us in edge cases that we could hardly conceive of. No matter how precise things were specified, no matter how rigorous things were, there were always edge cases that could be pried open to present practical attacks. What I eventually took away from it is that even the smartest humans aren't actually smart enough.
Rogaway was one of the smartest people I ever met. The fact that OCB2, proven secure, had a gaping hole discovered in 2018 doesn't leave me much hope that we'll ever have proveably secure anything.