Theoretically, formal verification can only tell you as much as can be encoded in a formal [email protected] problem is that no such kind of specs are known to exist (yet, if ever). As a thought experiment, if the informal specs written in English/Chinese or trapped in our head were as incomplete as a formal spec, we wouldn’t even be able to reason about what to test in the first place.

@ Then there is the limitation of verification tech of course.