The Ethereum Foundation has allocated $100,000 to develop a formally verified compiler for the Vyper smart contract language. This grant is part of a larger $600,000 security initiative focused on Vyper, aimed at ensuring that EVM bytecode accurately reflects source code.
The project involves collaboration with the Foundation for Verified Software and utilizes research from the Verifereum project and the HOL4 proof assistant. The Vyper development team is also participating to ensure the verification aligns with the compiler's architecture.
Vyper currently secures over $2 billion in total value locked across DeFi protocols, including Curve and Yearn. The initiative seeks to prevent compiler-level bugs, such as the 2023 reentrancy vulnerability in Vyper that resulted in approximately $70 million in losses.
The foundation intends to integrate a verified compilation mode into the official Vyper compiler. The Ethereum Foundation has invited further contributions from the ecosystem to expand the scope of the project beyond the initial funding.
