Что действительно нужно для того, чтобы Web3 стал надежным?

На прошлой неделе в подкасте @HeliosStaking гостем был @RosuGrigore, который рассказал о verifiability, formal methods и создании доказуемых систем для будущего децентрализованной инфраструктуры.

↓ Вот основные моменты:

От @NASA к blockchain-инфраструктуре: @RosuGrigore начал применять formal methods к системам, критичным для миссий в NASA. Сегодня эти же инструменты используются для блокчейнов, требующих доказуемой корректности.

Как возникла Runtime Verification: @RosuGrigore основал @rv_inc, чтобы внедрить formal methods в системы реального мира. Изначально его отвергли как на конференциях по тестированию, так и по formal methods, но термин “runtime verification” переосмыслил подход — сочетая наблюдение во время выполнения с гарантиями корректности. Сейчас это целая категория системной уверенности.

Почему важна semantics: Без formal semantics языки программирования превращаются в движущиеся цели. Pi Squared использует K Framework и Matching Logic для определения и анализа поведения программ с математической точностью.

Поддержка от @IOHK_Charles и @VitalikButerin: IOHK профинансировал ранние работы по формализации языков в K. Виталик предоставил гранты на проверку Casper protocol, Vyper, Uniswap и ETH2 deposit contract — одни из первых усилий по formal verification в этой области.

Verifiability без порядка: Pi Squared вводит децентрализованный слой расчетов, где claims — будь то от rollups, AI-агентов или бирж — могут проверяться независимо и параллельно. Глобальный порядок не нужен. Только доказательство.

“Без verifiability, это не Web3.”

Корректность становится переносимой.
Правда становится программируемой.