That is true. Scaling this to processor with caches and deep pipelines is completely non-trivial. There has been some attempt to scale to more "realistic" designs with compositional (stepwise) verification.

http://www.ccs.neu.edu/home/pete/research/ieee-vlsi-composit...

http://www.ccs.neu.edu/home/pete/research/todaes-safety-live...