Interesting. Using a fully automatic SAT solver for the easy stuff and Coq for the things the SAT solver can't prove maker good sense. We did that 40 years ago in the Pascal-F system. The Oppen-Nelson cooperative decision procedure system (the first SAT prover) did the easy stuff - proofs that only need addition, subtraction, multiplication by constants, and logic. Beyond that you had to write a "rule" and prove it with the Boyer-Moore prover, which is a constructive system that uses induction. About 95% of the verification conditions were solved without adding new rules.

This group got about as far as we did - arrays, but not dynamic allocation, pointers, or objects. "WP cannot currently work with dynamic allocation, " they write. That's the point at which describing what "valid" means becomes difficult, and you get into specification languages separate from the program.

I notice they put in what they called "ghost code", code which has meaning only at proof time. We called that "proof code". It's written in the same language as the real code, and can look at values from the output, but can't change them. This is a programmer-friendly way to write specifications. It's easy to write code to check a sort or a lookup if you're not concerned about speed or space. Then you prove that the dumb check and the complex algorithm get the same result.

One big problem with proof of correctness systems is that they tend to be designed by people in love with the formalism. They need to be designed by people who hate and fear bugs. The Microsoft Static Driver Verifier is probably the best example of a system aimed squarely at preventing crash-type bugs. It's the main tool Microsoft used to prevent drivers from crashing Windows 7 and later.