Ethereum Foundation выделила $100 000 на разработку формально верифицируемого компилятора для языка смарт-контрактов Vyper. Грант является частью программы ETHSecurity Initiatives Round Two с общим бюджетом $600 000, направленной на устранение расхождений между исходным кодом и байт-кодом EVM.
В работе участвуют Foundation for Verified Software и команда разработчиков Vyper. Проект опирается на исследования в области формальной семантики с использованием инструмента HOL4. Цель инициативы — внедрить режим верифицируемой компиляции в официальный компилятор Vyper.
На текущий момент на базе Vyper работают DeFi-протоколы с совокупной заблокированной стоимостью свыше $2 миллиардов, включая Curve и Yearn. Верификация призвана исключить ошибки компилятора, подобные уязвимости 2023 года, которая привела к потере $70 миллионов.
Ethereum Foundation призвала участников экосистемы к дополнительному финансированию проекта для расширения его масштабов. Формальная верификация должна гарантировать, что байт-код в блокчейне в точности соответствует логике, заложенной в исходном коде смарт-контракта.
