total formal verification is not possible in 2020

'20.11.3: co.quora/adds/cyb/sec/total formal verification is not possible in 2020:

current efforts at formal verification

cannot yet find all unknown vulnerabilities in software:

. as pointed out by the SeL4 team, in

“What is Proved and What is Assumed”

who used formal verification to debug a microkernel,

they are still vulnerable to inaccuracies of the hardware model;

ie, assuming the hardware acts a particular way

when under special conditions it actually does something else.

. some CPU chip instructions are reprogrammable by the manufacturer

with on-chip microcode; eg Intel Microcode

 (https://en.wikipedia.org/wiki/Intel_Microcode);

this could either make the CPU more correct

or make it vulnerable to malicious modification?

. also, there was some of the SeL4 software

that was not practically verifiable yet:

"there may still be faults remaining in

specific low-level parts of the kernel

(TLB, cache handling, handwritten assembly, boot code)."