I do know of one researcher working on this: Julian Bangert at MIT out of Dartmouth has modeled x86 family processors in SMT, and is able to prove that all paths through a particular piece of code compile so that all cache hits are identical, CPU ticks are identical, etc. Brilliant young man - I expect we'll be seeing a lot more from him.