The Most Dangerous Word in AI Coding: "Verified"
wintrover
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...
Tags