In this case 3 of the bugs would be caught when trying to prove the absense of undefined behaviour/use of uninitialized value. Can existing formal proof tools be used for that?