The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program.
It is not a big deal, I think formal verification is a very useful tool to help one approach correctness, but let me explain myself. When a program is written it is trying to solve a problem, when it solves that problem correctly it has no bugs, and when it solves that problem incorrectly those are bugs. For complex problems it turns out to be very difficult(impossible) to solve them correctly. Why is there an assumption that the formal verification spec will be any more correct than the program itself? They are both trying to solve very complex problems.
I was trying to get a feel for this by reading through the sel4 git changes trying to figure out how many bug fixes were for the OS and how many were for the spec. No real conclusion unfortunately. because they almost always have to fix both at the same time. a bug found in the OS means you have a bad spec and a bug found in the spec means your OS probably has a bug.
It is not a big deal, I think formal verification is a very useful tool to help one approach correctness, but let me explain myself. When a program is written it is trying to solve a problem, when it solves that problem correctly it has no bugs, and when it solves that problem incorrectly those are bugs. For complex problems it turns out to be very difficult(impossible) to solve them correctly. Why is there an assumption that the formal verification spec will be any more correct than the program itself? They are both trying to solve very complex problems.
I was trying to get a feel for this by reading through the sel4 git changes trying to figure out how many bug fixes were for the OS and how many were for the spec. No real conclusion unfortunately. because they almost always have to fix both at the same time. a bug found in the OS means you have a bad spec and a bug found in the spec means your OS probably has a bug.