BB is proving things about all turning machines of a general size and it's unsolvable in general because 1. above a certain size you're encoding all the unsolved problems of mathematics 2. Halting problem.
BB and halting problem is also totally irrelevant here. We're talking about proving specific things about specific pieces of software, where we can change the software implementation to make the desired invariants easier to prove. Obviously there's the well known catch of just because you proved x doesn't mean that x being true implies whatever y behavior (security, class of bugs, etc) you're actually interested in but like, that's why we have standards committees and stuff. And the nice thing is there's sort of an evolutionary pressure when it comes to figuring out the right invariants for security in that anything you do will get aggressively stress tested by swarms of increasingly capable agents.
In terms of the alignment problem - the latter is possible and a risk but also you're talking about reward hacking like it's some gotcha instead of a thing people have been thinking about for decades and are spending hundreds billions of dollars on given at least the national security needs here and at worst the risk of catastrophic misalignment/rogue swarms. The huggingface hack is fresh in everyone's memory