Earlier quoted context omitted.
In short: Yes. In many cases having solid formal foundation allows to fomulate high-level properties which would allow to catch even bugs like recent log4j. There is alreay a lot of work on formalization of ISA/CPU definitions which could allow to catch low-level bugs/expoloits.
"catch even bugs like recent log4j" 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.
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.