Explore what subset of a WASMable language can be formally verified to help with future smart contract VM recommendations.