O que realmente é necessário para tornar o Web3 confiável?

O episódio da semana passada do podcast @HeliosStaking contou com @RosuGrigore, abordando verificabilidade, métodos formais e a construção de sistemas comprováveis para o futuro da infraestrutura descentralizada.

↓ Aqui estão os destaques:

De @NASA à infraestrutura blockchain: @RosuGrigore começou aplicando métodos formais em sistemas críticos de missão na NASA. Hoje, essas mesmas ferramentas estão sendo usadas em blockchains que exigem correção comprovável.

Como a Runtime Verification tomou forma: @RosuGrigore fundou a @rv_inc para levar métodos formais a sistemas do mundo real. Inicialmente rejeitada por conferências de testes e métodos formais, o termo “runtime verification” reformulou a abordagem—misturando observação em tempo de execução com garantias de correção. Agora, define uma categoria inteira de garantia de sistemas.

Por que a semântica importa: Sem semântica formal, linguagens de programação tornam-se alvos móveis. Pi Squared usa o K Framework e Matching Logic para definir e raciocinar sobre o comportamento de programas com precisão matemática.

Apoio de @IOHK_Charles e @VitalikButerin: a IOHK financiou trabalhos iniciais na formalização de linguagens em K. Vitalik concedeu bolsas para verificar o protocolo Casper do Ethereum, Vyper, Uniswap e o contrato de depósito do ETH2—alguns dos primeiros esforços de verificação formal na área.

Verificabilidade sem ordenação: Pi Squared apresenta uma camada de liquidação descentralizada onde reivindicações—sejam de rollups, agentes de IA ou exchanges—podem ser verificadas de forma independente e paralela. Sem necessidade de ordenação global. Apenas prova.

“Sem verificabilidade, não há Web3.”

A correção torna-se portátil.
A verdade torna-se programável.