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 While also asserting "an error occurred" Boil it down: typ == expected AND simultaneously: typ != expected Logically impossible. What the Solver Did Z3 (or any SMT solver) takes one look and concludes: Unsat (Unsatisfiable) In formal verification, this usually means: "No execution path exists where the error occurs." So the engine outputs: ✅ Verified Where It Went Wrong Here's the thing. The solver didn't prove the code safe. It proved the question itself was invalid. Vacuous Truth This