Ethereum contracts are effectively Turing complete (well, technically linear bounded automata complete). But you get the same state space explosion issues as with formal validation of any other language.