Or create another language that compiles to the Ethereum virtual machine. There are several already, and at least two in development designed to be better for formal verification.
Yes that is what I meant - I don't know Ethereum as well, so I assumed Solidity is the already the level of the VM (the "assembly"). Thanks for clarifying!
I don't think it makes that much sense, after all, you could also create another language that compiles to Solidity, and that is verifiable.
I mean it is OK, just not as much of an improvement as they make it sound.