"intuitive and feature rich formal verification frameworks for the major programming languages" I doubt that such things are really possible. I see two problem

"intuitive and feature rich formal verification frameworks for the major programming languages" I doubt that such things are really possible. I see two problems: 1. computers in general don't have domain knowledge, so they can't really say what "correct" means; 2. computers don't have a conceptual model of what it is a human is trying to do, so they can't determine if that way is correct. I thought about this when I was playing with microcontrollers. There are all sorts of bizarre flags and ways and means of configuring and controlling a peripheral. If there was only one correct way of doing things, then it wouldn't make much sense to give such fine-grained control. In one particular case I was writing to a peripheral. Normally one would block processing until the transfer was complete. However, I needed the operation to be done frequently, and blocking would have consumed much-needed computing cycles. My solution was to simply write to the peripheral. I knew that it would be complete by the time I made the next transfer. Well, the thing is, a checker just can't reason in that way. It takes a human to do that. Humans can of course be wrong, and often are, but thems the breaks. Formal checking may be able to establish a few things, but as a general exercise, there is no more chance of some kind of AI proving your program to be right as there is of solving the halting problem.