Бутерин опубликовал статью под названием «Краткий обзор формальной верификации», где констатировал: за последние несколько месяцев стал более популярным метод программирования на языках очень низкого уровня. Речь о байт-коде Виртуальной машины Эфириума (EVM) или языке Lean. Главная фишка метода — проверка кода с помощью автоматически проверяемых математических доказательств, написанных на Lean. Бизнесмен уверен, что при правильном подходе такой метод способен повысить уровень безопасности кода по сравнению с обычными методами программирования.
Программист утверждает, что формальная верификация — математическая проверка кода на ошибки до того, как их найдут хакеры, поможет защитить Эфириум и другие блокчейны от взлома. Все более мощные ИИ-инструменты помогают находить скрытые ошибки кодирования, а также серьезные уязвимости в смарт-контрактах, которые человек может не заметить. ИИ не способен заменить человека, однако способен повысить эффективность его работы, написал Бутерин. По его словам, сейчас аналитики и программисты используют ИИ не только для обнаружения угроз, но и для более быстрого создания безопасного кода. Сооснователь Эфириума считает это важным достижением криптоиндустрии.
Бутерин сослался на бывшего инженера Ethereum Foundation Йоичи Хираи (Yoichi Hirai), назвавшего это «финальной формой разработки программного обеспечения». Хираи работал над безопасностью смарт-контрактов Эфириума, однако в 2018 году покинул свой пост, опасаясь, что предложение EIP-867 для стандартизированного формата возврата потерянных средств может нарушать законодательство Японии.
Однако Бутерин оговорился: если подобные ИИ-инструменты будут использовать злоумышленники, они смогут выявлять программные ошибки за считанные минуты, что станет серьезной угрозой для блокчейн-индустрии. Поэтому сооснователь Эфириума призвал разработчиков не пренебрегать более надежными методами верификации, более безопасными языками программирования и более строгими стандартами создания программного обеспечения.
Ранее Бутерин выразил опасения: если искусственный интеллект оставить без контроля, он может восстать против человечества и стать «высшим видом планеты». В феврале программист предложил сделать Эфириум сетью, где платежные операции обслуживал бы ИИ.
