Yep, I have the same impression. Anything that proves something about stuff that's not the actual running code is nearly useless to me. The code will be changed

Yep, I have the same impression. Anything that proves something about stuff that's not the actual running code is nearly useless to me. The code will be changed every single day by developers who may not be familiar with that code. The verification must work on that implementation code. As I see it, the only way to do it properly is to embed the proof in the code like we embed types in the code. For example, we've been able to get rid of NullPointerException completely by using the checker framework, all we need to do is maunually annotate all values that may be null (everything else is assumed non-null, if you try to assign it to null the compiler won't compile): @Nullable String getSomething(); The annotation is not a layer on top of the code, it is code. The compiler can check it (with appropriate extensions). I even played with adding support for dependent types, I am convinced the compiler extension would allow me to do that, but unfortunately I have other things to do.