I understand that formal verification is not panacea.

My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code".

We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.