No, I am not. Read what I wrote again :)
> and please don't forget to collect your Turing Award!
Some people have already beat me to it. The 2007 Turing Award was awarded for the invention of model checkers that precisely and soundly check deep properties.
> One problem with model-checking is that you handle loops by replacing loops with approximations
No, that's what sound static analysis with abstract interpretation does. Model checkers are both sound and precise, i.e. they have neither false positives nor false negatives. To the extent they use sound abstraction (i.e. over-approximation), as in CEGAR algorithms, they do so to increase performance and to sometimes be able to handle infinite state spaces. A model checker, however, is always sound and precise, or else it's not a model checker.
> In other words extremely shallow properties.
Model checkers commonly check arbitrarily deep properties. Engineers in industry use them for this purpose every day.
> All mathematics is deductive.
Yes, and all (or much, depending on your favorite philosophy of mathematics) of it has models. If you have two apples in one hand and one apple in the other and you count how many you have, you have not done so using deduction in any logical theory. That had you used such a process you would have also reached the same result is because of soundness and completeness meta-theorems. That mathematics has both proof and model theories, and that they're compatible, is the most important result in formal logic.
> All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
All verification methods are limited by both size of code and depth of properties. For non-trivial property, the least scalable method, on average, is deductive proof. Which is not to say it is not useful when automated methods have failed.