All formal verification requires some assumptions. For example, you might assume that a cosmic ray isn't going to alter a bit in your instructions stream (or you might be developing for outer space and you assume that no more than X bits will be flipped in a given amount of time).
Certain assumptions can make it trivial to verify the performance of code (e.g. assume all memory accesses miss cache and happen right at the beginning of a DRAM refresh for the address you are accessing).
That usually ends up too crappy, so you bound the worst case a bit more by using the cache-replacement model of the CPU you are using. Writeback cache make this analysis quite difficult which is one of many reasons for the existance of writethrough cache. In any event, given a certain execution model, it is tractable to bound the worst-case performance of a system formally.
Certain assumptions can make it trivial to verify the performance of code (e.g. assume all memory accesses miss cache and happen right at the beginning of a DRAM refresh for the address you are accessing).
That usually ends up too crappy, so you bound the worst case a bit more by using the cache-replacement model of the CPU you are using. Writeback cache make this analysis quite difficult which is one of many reasons for the existance of writethrough cache. In any event, given a certain execution model, it is tractable to bound the worst-case performance of a system formally.