Віталік: AI-асистоване формалізоване доведення є «кінцевою формою розробки програмного забезпечення», Ethereum стане безпековим ядром

Співзасновник Ethereum Віталік Бутерін 18 травня опублікував глибокий аналіз, у якому розглянув сучасний стан і перспективи технологій формальної верифікації (Formal Verification). Він вважає, що формальна верифікація, підсилена AI, стане «остаточною формою розробки програмного забезпечення», і зазначає, що Ethereum стане важливою складовою майбутньої архітектури «безпечного ядра».

Формальна верифікація: ключові принципи та застосовні сценарії

За даними зі статті Віталіка, формальна верифікація особливо підходить для сценаріїв, де «ціль значно простіша за реалізацію». Він чітко перелічив чотири категорії ключових технічних компонентів для наступного етапу оновлень Ethereum:

Квантово-стійкі підписи: уже ведеться формальна верифікація варіантів підписів SPHINCS

Система STARK-доказів: проєкт Arklib працює над створенням реалізації STARK із повною формальною верифікацією

Консенсусний алгоритм із відмовостійкістю до візантійських збоїв: зараз фокусується на формальному визначенні та доведенні безпекових властивостей консенсусу Lean

ZK-EVM: проєкт evm-asm має на меті створити повноцінну реалізацію EVM із формальною верифікацією (безпосередньо на RISC-V асемблері)

Віталік посилається на вислів Йоічі Хірай (平井洋一) і називає цей підхід «остаточною формою розробки програмного забезпечення».

Напрям еволюції «безпечного ядра», який описує Віталік

За даними зі статті Віталіка, він описує модель еволюції майбутніх програмних архітектур:

Безпечне ядро: через безперервне посилення формальними методами, несе найвищу довіру; Віталік прямо вказує, що Ethereum, ядро операційної системи та пов’язані з IoT застосунки стануть безпечним ядром.

Небезпечна периферія: периферійні компоненти працюють у середовищі пісочниці, їм надають мінімальні права, необхідні для виконання роботи; якщо периферійний компонент виходить з ладу, безпечне ядро забезпечує захист.

Обмеження підтвердження та сценарії провалу формальної верифікації

Віталік визнає, що формальна верифікація не є всесильною. Він посилається на роботи дослідників на кшталт Надіма Кобеіссі (Cryspen) і підтверджує три основні типи сценаріїв провалу: часткові пропуски верифікації (верифікується лише частина коду, а невирірфікована частина містить критичні дефекти); прогалини у специфікаціях (помилки в самій безпековій специфікації або неправильні припущення в доведенні); атаки через побічні канали (side-channel атаки на межі між софтом і хардом складно вловити наявними моделями).

Віталік підкреслює, що «доказова правильність» за своєю суттю перевіряє внутрішню узгодженість між різними формально вираженими намірами, а не абсолютну відповідність людським реальним намірам.

Інструменти для AI-допомоги у формальній верифікації

За даними зі статті Віталіка, наявні інструменти: Lean (мова математичних доведень, яка автоматично верифікує теореми); Claude та Deepseek 4 Pro (Віталік підтверджує, що їх достатньо для написання Lean-доведень); Leanstral (модель відкритої ваги з 1190 млрд параметрів, спеціально під мікс-доучування для написання Lean, яку можна запускати локально; бенчмарки показують кращі результати, ніж у багатьох загальних моделей значно більшого масштабу).

Питання, що часто ставлять

Чому Віталік вважає, що Ethereum має стати «безпечним ядром»?

За даними зі статті Віталіка, Ethereum подібний до ядра операційної системи: він несе найвищий рівень довіри в процесі цифровізації суспільства. Він зазначає, що мета дизайну безпечного ядра — довести його безпеку до стандарту, за якого не допускається розповзання програм із вразливостями, і спрямувати всю додаткову обчислювальну потужність, яку приносять AI, на посилення безпеки самого безпечного ядра.

Чому формальна верифікація особливо підходить для STARK, ZK-EVM та подібних технологій?

За аналізом Віталіка, спільна риса цих технологій — «ціль значно простіша за реалізацію»: їхні властивості безпеки можна чітко визначити математичною мовою, але конкретна реалізація надзвичайно складна. Саме в таких умовах формальна верифікація найкраще розкриває свій потенціал.

Як Віталік радить розробникам практично використовувати AI-допомогу у формальній верифікації?

За даними зі статті Віталіка, він радить, щоб AI писав код Lean і математичні доведення, а користувачу в підсумку залишалося лише перевірити, чи доведені твердження відповідають очікуванням, без самостійного написання виснажливої базової доводної коди. Він підтверджує, що Claude, Deepseek 4 Pro та Leanstral — це основні інструменти, доступні на сьогодні.