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.