Ethereum Foundation Backs Verified Compiler for DeFi-Secure Vyper
The Ethereum Foundation has awarded a $100,000 grant to fund a formally verified compiler for Vyper, a Python-flavoured smart contract language used by DeFi protocols with over $2 billion in total value locked.
The goal of the project is to build a publicly accessible 'verified compilation' mode into the official Vyper compiler, allowing developers and auditors to confirm that on-chain bytecode matches reviewed source code.
This comes after a reentrancy vulnerability tied to specific Vyper compiler versions drained around $70 million from several Curve pools in 2023. The root cause was a compiler bug, not bad source code.
The work involves the Foundation for Verified Software and the Vyper development team, building on formal semantics research conducted in HOL4, a proof assistant used to mathematically verify software.