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

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.