'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)."
