WYIL: verification transformer now compiles.
WYIL: VerificationCheck now compiles as well.