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.
Well... it might have raised a red flag about how incredibly dangerous the feature was, because there would be no way to make the verification shut up about the code that implemented the feature (if the verification did a good job).
I don't know about log4j, but in the case of many such features, there would be a PM or somebody insisting that you have to implement his pet idea, no matter how much the tool screams.
How could it help with that? JNDI lookups were a documented feature of log4j. An incredibly dangerous one, but it was intended to work like that.