20 x 1000 x 1000 Lines Of Code can be made error free.

Wrong. As Dijkstra famously observed half a century ago, testing can only show the presence, not the absence of bugs. The only way to ensure that a program is free of bugs is to prove it correct. But such correctness proofs do not scale to millions of lines. The first OS to be proved correct is seL4, consisting of about 10 kSLOC, and that was an effort of about a dozen person years. Formal proofs of less complex software may be possible to scale to maybe 100kSLOC these days, but not beyond for the time being.

This is the fundamental reason why where security or safety is paramount, only a microkernel, such as seL4, will provide the answer -- Gernot

Phil must also add that without testing formal proofs should not be trusted, to quote:

“Beware of bugs in the above code; I have only proved it correct, not tried it.” - Donald Knuth

And yes we will do both.