Also worth noting that the verifier is under active development not only to verify more legitimate programs, but also to reject programs with exploits and side channels (and there are runtime defenses too, like dead code elimination and ALU sanitation).