The IC3 research group at Cornell, and especially Elaine Shi's group, has been thinking about this recently. They are (I think) working on some kind of program analysis framework using deep PL techniques to formally verify smart contracts.