[naasking]

"Unverified code" isn't the problem, because a module could do exactly what it's verified to do. The problem is that the underlying execution model exposes capabilities that the high-level language cannot represent. This lets attackers silently violate invariants that your language is supposed to enforce.

For instance, at one point on the CLR you could throw an object of any type, it didn't have to inherit from System.Exception. But the C# compiler required you to inherit from System.Exception, so a properly crafted callback from a "malicious" module could escape the your C# program's control-flow by throwing an exception that you couldn't catch.

There are loads of full abstraction failures in the JVM and other languages. So if your cryptocurrency VM can execute arbitrary programs, but your surface language is a non-Turing complete language, unless you're very, very careful, you're virtually guaranteed to introduce vulnerabilities due to full abstraction failures.

This property is incredibly subtle, so I wouldn't discount it so easily, particularly when there's so much money involved.