Віталік: Формальна верифікація за допомогою AI може одночасно підвищити ефективність і безпеку коду

За повідомленням Foresight News, Віталік Бутерін опублікував статтю, в якій обговорюється перспективи застосування формальної верифікації у сфері безпеки блокчейнів. У статті зазначається, що в передових дослідженнях Ethereum формується нова парадигма: безпосереднє використання EVM байткоду, асемблера або Lean для написання коду і верифікації його коректності за допомогою математичних доказів, які можуть бути автоматично перевірені в Lean. Дослідник Yoichi Hirai називає цю парадигму «остаточною формою розробки програмного забезпечення». Віталік вважає, що формальна верифікація за підтримки AI здатна одночасно підвищити ефективність і безпеку коду, особливо для таких ключових безпекових модулів, як STARK, ZK-EVM, квантово-стійкі підписи та алгоритми консенсусу. У статті також наголошується, що формальна верифікація не є універсальним рішенням і може втрачати ефективність через неповноту охоплення доказом, помилки у специфікаціях або проблеми на апаратному рівні. У майбутньому програмне забезпечення, ймовірно, поділиться на «безпекове ядро» та «небезпечну периферію», причому Ethereum стане одним із важливих безпекових ядер.