I think some timing attacks could be reasoned about in a formal context. You could model the timing details of a given CPU and then prove that two assembly language functions were indistinguishable with respect to that model. (For example, in the case of a comparison function that bailed out early when it found a difference leading to a timing discrepancy, you could replace it with a `for` loop like `for(i = 0; i < size; ++i) mismatch_ctr += src[i] != dest[i]` and then prove that the function takes the same amount of time regardless of whether `src` and `dst` are identical.)