In many cases we don't even know ourselves what the program should do. There are many edge cases, business decisions, dark and not dark patterns, misunderstood requirements, etc. What can it verify, that the program is doing correctly what we actually did not want it to do? At least we could end up with no bugs in the ORM, but it's not there that my customers are making money.