Comment by glennfiedler

Yes. You are missing something. They are proving that for all possible inputs the program doesn't crash for a given size of potential inputs at the machine code level. The proof extends to an entire set of inputs and all the code it touches, not just the cases the fuzzer covers. In short, they have better coverage than any fuzzer.