A deeper understanding of the program - which is what verification brings to the table - may be useful; even if it is too slow for most code, it can occasionall

A deeper understanding of the program - which is what verification brings to the table - may be useful; even if it is too slow for most code, it can occasionally be used to detect bugs/speed up the most critical parts. It would also be rather useful, although probably quite a bit of work, to have a "verify the optimizations you did" mode. While most errors aren't compiler errors, gcc has been known to optimize bugs into programs...