Examples of smart contracts which are hard to formally verify

What are some examples of smart contracts that pose challenges in formal verification? I'm interested in exploring code that poses issues for formal verification, as I would like to tackle the problem through symbolic generation of code.