Got a "Verified" result from my formal verification engine. Problem was, it was completely wrong. Looking at a simple function: checkType from Bitcoin Core. The engine generated this SMT query: (assert (= throwsRuntimeError (not (= typ expected)))) (assert (= typ expected)) (assert throwsRuntimeError) At first glance? Looks fine. But there's a fatal flaw in there. Unpack it and here's what you get:
- Error occurs when typ != expected
- But we're assuming typ == expected
- While also asserting...