Formal? Computer assisted proof checkers? Building strong cryptosystems is notoriously hard, especially when you start composing different systems since some are only secure given certain preconditions which are on you to remember and ensure.

Proof checkers only check for invariants you knew to check for. They're not future proofing against exploits, they're merely a solidification of what you knew about your attack surface at a time.