If researchers fuzz Ethereum smart contracts they will discover critical bugs in the Ethereum Virtual Machine, then decide formally verifying Solidity written c

If researchers fuzz Ethereum smart contracts they will discover critical bugs in the Ethereum Virtual Machine, then decide formally verifying Solidity written contracts was a waste of their time. Of course these bugs will be patched but there will be a never ending river of bugs for researchers to find later just like there is in every other VM. Rewriting the VM, and using a language amenable to formal verification for the contract DSL, then releasing their own implementation would probably be a better use of their skills and resources instead of dressing up Solidity. Imagine pwn2own had a $100k bounty on the EVM except you also have the added incentive of keeping all the ETH you can grab as well https://arstechnica.com/information-technology/2017/03/hack-that-escapes-vm-by-exploiting-edge-browser-fetches-105000-at-pwn2own/ https://arstechnica.com/information-technology/2017/03/hack-...