It's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....

Cannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.