Nah. I made a low-level VM in 2001 similar to this funclets proposal cwzwarich linked to (Hi, Cameron), and verification was a fast local check. Each funclet had a signature, you collect the signatures before you start verifying the code, and then track changes to the stack as you walk through the code, using the signatures for the effects of any calls you encounter, and finally insisting that the funclet match its declared effect. Control flow within a funclet is reducible. (I didn't call them funclets, but it sounds like the same basic scheme on glancing through. One simplification: my VM could loop only through the tail calls.)