I wouldn't say "clearly" false, though it depends on what you mean by "cost". In a computational complexity sense, most methods are exponential, barring some special-case methods, though in practice you can scale up to pretty big problems anyway. For example, SMT solvers have complexity growing exponentially with the problem size, unless you greatly restrict the formalism, but can verify fairly large designs. The techniques I know of for verifying multithreaded programs have cost growing exponentially with the number of threads as well.
He seems to be talking about proofs by hand, though, where you model a protocol mathematically and then write out a paper proving the protocol to be have desired properties. I have no idea if anyone's tried to quantify how that kind of complexity scales.
I don't know how it scales either, but I'd guess that if your proofs grow even quadraticly with code size then you're doing something wrong. Exponential growth is just clearly wrong. Note that even for SMT solvers, there is not exponential growth with program size. Even with small programs, the model space can be infinite, and general automated theorem proving is undecidable, not NP. Do you have evidence that a million line program is inherently harder to check with an SMT solver than is a thousand line program? Both are probably jut checking approximations to the model.
Similarly, with multi-threading, either the program works for a simple reason that it's author understands, or its correctness is not understood (and it probably doesn't work). People don't work through exponentially increasing number of cases in a growing project, and nor will formal proofs.
He seems to be talking about proofs by hand, though, where you model a protocol mathematically and then write out a paper proving the protocol to be have desired properties. I have no idea if anyone's tried to quantify how that kind of complexity scales.