I agree that a correctness proof for a complete, large program will always have the problem that the specification itself might be buggy. So integration tests w

I agree that a correctness proof for a complete, large program will always have the problem that the specification itself might be buggy. So integration tests will hardly ever become unnecessary. But as others have already pointed out, even then formal verification of critical parts of a program can be useful. I would like to add that it can also be of great value if one can "only" prove that a program will never trigger undefined behaviour, or cause a runtime error. For C programs, that would, of course, be particularly helpful. But even in safe Rust, there can be (in my understanding, I haven't yet used Rust myself) runtime errors in the form of panics. And if your medical device stops working, because the software attempted an out-of-bounds read or write and was therefore aborted with a panic, that isn't really fun. Better to prove statically that such invalid accesses will never occur. And this is still for safe Rust - not even considering unsafe code. Similar arguments hold for other system-level programming languages, I guess, even if they are considered safer than C or C++.