That's the whole point of doing a provably correct transformation from a simpler model domain. Even complicated OOOE engines are fairly tractable if you don't try to implement them at an RTL level...

Perhaps we are imagining different formal verification methodologies. Can you tell me what kind of formal verification you're referring to?