I think the last paragraph is the real point here. Formal Verification can't really guarantee zero bugs, but it's often advertised as such so people rightfully question it.
The most obvious ways that it misses bugs in my experience (in hardware design but I guess it's the same in software) are:
* Mistakes in the formal properties
* Omitting properties that should be proven
* Adding assumptions that actually aren't true
* Bugs in the prover
There's also an insidious failure mode for SystemVerilog in particular in that the semantics of the language for formal verification are subtly different from the simulation semantics. And that can be different from the synthesis semantics which are not actually even specified anywhere (SystemVerilog is a language for simulation of hardware that has been co-opted for synthesis).
It's like if you could compile your TLA+ code to C but the semantics of the C code were slightly different in a few places to the TLA+ semantics.
The most obvious ways that it misses bugs in my experience (in hardware design but I guess it's the same in software) are:
* Mistakes in the formal properties
* Omitting properties that should be proven
* Adding assumptions that actually aren't true
* Bugs in the prover
There's also an insidious failure mode for SystemVerilog in particular in that the semantics of the language for formal verification are subtly different from the simulation semantics. And that can be different from the synthesis semantics which are not actually even specified anywhere (SystemVerilog is a language for simulation of hardware that has been co-opted for synthesis).
It's like if you could compile your TLA+ code to C but the semantics of the C code were slightly different in a few places to the TLA+ semantics.