The best example of this problem is probably SPARK, a variant of Ada which permits formal verification. Its verifiers are awfully finicky, and tuning the param

The best example of this problem is probably SPARK, a variant of Ada which permits formal verification. Its verifiers are awfully finicky, and tuning the parameters (including selecting the most appropriate verifier) can mean the difference between successful completion in a few seconds, and outright non-termination/timeout-with-failure. It's true that the answer is to have better verifiers, but that's not just a matter of tweaking the verifier code, it's a serious research challenge. One of the most serious problems with formal methods is the ability to scale. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)