Виталик: Использование искусственного интеллекта для формальной проверки кода может одновременно повысить его эффективность и безопасность

По сообщению Foresight News, Виталик Бутерин опубликовал статью, в которой рассматривает перспективы применения формальной верификации в области безопасности блокчейна. В статье отмечается, что в передовых разработках Ethereum формируется новая парадигма: код пишется напрямую на байткоде EVM, ассемблере или Lean, а его корректность проверяется при помощи математических доказательств в Lean, которые могут быть автоматически проверены. Исследователь Йоичи Хираи назвал такую парадигму «окончательной формой разработки программного обеспечения». Виталик считает, что формальная верификация с поддержкой искусственного интеллекта способна одновременно повысить эффективность и безопасность кода, особенно в таких ключевых модулях безопасности как STARK, ZK-EVM, постквантовые подписи и алгоритмы консенсуса. В статье также подчеркивается, что формальная верификация не является панацеей и может быть неэффективной из-за неполного покрытия доказательства, ошибок спецификации или уязвимостей через аппаратные каналы. В будущем программное обеспечение, возможно, будет делиться на «безопасное ядро» и «небезопасную периферию», а Ethereum станет одним из важных безопасных ядер.