The Most Dangerous Word in AI Coding: "Verified"

Got a "Verified" result from my formal verification engine. Problem was, it was completely wrong. The Setup 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. The Contradiction Unpack it and here's what you get: Error occurs when typ != expected But we're assuming typ == expected W