One can define a high-level security property, like "not executing remotely-downloaded code" and try to prove that no execution path of the program triggered by

One can define a high-level security property, like "not executing remotely-downloaded code" and try to prove that no execution path of the program triggered by input data violates it. The formal verification will force you to consider all possible scenarios to be able to prove that this is not going to happen.