Сооснователь Ethereum Виталик Бутерин в новом эссе на своем сайте заявил, что сочетание искусственного интеллекта с формальной верификацией способно стать «конечной формой» разработки программного обеспечения — этапом, когда высокооптимизированный код будет подкреплен машинно-проверяемыми доказательствами корректности. По его мнению, такой подход особенно уместен в случаях, где цель гораздо проще реализации: квантово-устойчивые подписи, протоколы консенсуса, ZK-EVM и системы доказательств STARK.
Бутерин сослался на практический пример проекта Lean Ethereum, где участнику удалось с помощью ИИ сгенерировать и машинно верифицировать доказательство одной из самых сложных теорем, лежащих в основе безопасности STARK. Это, по его словам, указывает на будущее, в котором ИИ-инструменты помогут разработчикам выражать желаемые свойства на языке доказательств, а затем автоматически искать и проверять, что конкретная реализация им действительно удовлетворяет.
Несмотря на оптимизм, Бутерин подчеркнул, что формальная верификация не панацея. Для сквозной безопасности потребуется проверять всё — от высокоуровневой спецификации до реализации на RISC-V или арифметизации прувера. Он также напомнил, что совершенная безопасность невозможна, поскольку человеческие намерения трудно формализовать, но верификация способна устранить более 99% негативных последствий от уязвимого кода. Ранее в этом году Бутерин уже призывал направлять примерно половину прироста производительности за счёт ИИ на тестирование и формальную верификацию, чтобы приблизить криптоиндустрию к коду, практически лишённому ошибок.
