Proving test coverage is just as (in)feasible as proving correctness. This is the elephant in the room for testing: it relies on programmer intuition to enumerate cases. It's easy to neglect a case both in the implementation and in the test. This is why tests are better at finding regressions than new bugs.