Surely it wouldn't be aimed at proving a 10 million line black box of code, right? In my mind it would have to be built from the ground up, sub unit tests for

Surely it wouldn't be aimed at proving a 10 million line black box of code, right? In my mind it would have to be built from the ground up, sub unit tests for function proofs and maintain 100% coverage as you go along. As long as the constituent parts are proven you don't have to zoom out to a macro level.