Since I presume your input space is relatively small (the AST of a program, which usually only has a few thousand nodes), it sounds like you have some sort of state-space explosion. Your comment about recursive matching of hypertees sounds like the biggest problem. Just a shot in the dark (having not studied what you're doing yet), but is there any chance you could use partial-order reduction, memoization, backtracking, etc. to reduce the state-space explosion?

I could be wrong, but most of the other optimizations sounded like they address constant factors, like contract checking. But then I don't know much about how contracts work; I guess the verification logic could be rather involved itself.