he is applying risk based assessment which tests are required to provide a high quality implementation.
If a system misbehaves you will catch in higher level tests in the test pyramid eventually.
The bug was found regarding the null pointer, he can and should add a dedicated unittest to reproduce the issue when he fixes the bug, since there is evidence that his assessment was wrong. This is not bad but usually quite efficient if this doesn't occur often or has a large impact on the system's user base.
In a software solution you can't prove 100% correctness - neither through "standard" type-systems nor through tests.
If you want to show formal correctness of a program have a look at https://cs.stackexchange.com/questions/13785/formal-program-...