But this level of formal verification gets you to the level of confidence you’d have if you had written the program in Rust or Java in the first place. The original post was talking about formally verifying what the system does as a whole, not just verifying the absence of a certain class of errors. I’m not questioning the value of eliminating null pointer dereferences that do exist, just the value of holding a formal proof of the absence of null pointer dereferences in a certain piece of code, given that there are many other possible bugs that that code could contain.
I mean, if I had a formal proof that my banking system could never double-spend money, that could be a useful property that someone would want to know about the system. If I have a proof that my banking system never dereferences a null pointer, there’s not very much I can be sure of on the basis of such a proof.