> Such compiler would require solving halting problem.

I don't think so. As long as false-negative results are acceptable. (i.e. it is ok if for some programs no proof if found even though they fulfill the specification)

Occasional false-negatives seem perfectly fine for real-world use.