True, I should have remembered to express it as Non-exhaustive testing cannot... I also consider formal methods not testing. But model checking (e.g. with tlc)

True, I should have remembered to express it as Non-exhaustive testing cannot... I also consider formal methods not testing. But model checking (e.g. with tlc) is something in between, and sort of takes advantage of the "This usually isn't feasible, but it's nice when it is.": when you limit your domain enough, it becomes feasible, yet exhaustively checking each small-world scenario gives a pretty good confidence on the model being correct.