[danielvf]

I've used formal verification in anger, as well as working with a vendor to formaly verify some critical code for us. This rings very true. It is extraordinarily difficult to write correct rules. It ends up being the same problem as wishing against an evil genie.

Most rules that you come up with at first end up having a class of obvious exceptions in the real world, which the verifier finds, and then even more unobvious exceptions, and soon your logic around the exceptions to the rules become at least as complicated as the code you are attempting to verify. And in this any wrong assumptions that falsely allow bad behavior are not caught or flagged because they pass.

Even giving perfect proving software, it's still a far harder challenge to write rules than to write code. And current software is still far from perfect - you are likely to spend a lot of your rules time fighting with your prover.