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 ex

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.