O bug do @Zcash levou ao Ironwood, à verificação formal do circuito de pagamento Orchard. Eu amo e apoio isso. Também quero destacar que o @Starknet vem fazendo isso — verificação formal — há mais de 5 anos. É importante apoiar grandes projetos como o Zcash por reagirem rapidamente, como neste caso. Também é importante reconhecer projetos que são futuristas e à frente da curva, como o Starknet. (Detalhes no artigo abaixo) Já disse muitas vezes que o Starknet é o sistema que já possui o que outras cadeias afirmam que terão em breve. Isso já foi verdade em muitos aspectos. Estivemos na vanguarda de muitas escolhas impopulares que agora todos reconhecem como importantes, incluindo ZK-STARKs seguros pós-quantum como a melhor solução para escalabilidade e privacidade, zkVMs enxutos (Cairo é o melhor), disponibilidade de dados Validium e verificação formal. Verificação formal significa que você usa ferramentas automatizadas, como o sistema Lean, para provar matematicamente que seu código é seguro. É muito difícil capturar todos os aspectos do que significa para um código ser seguro, mas liderados pelo nosso CTO @LiorGoldberg2 (co-criador do Cairo zkVM e da linguagem), estamos nisso há mais de 5 anos. O primeiro artigo sobre verificação formal de afirmações relacionadas a ZK (Professor Jeremy Avigad, Yoav Seginer e outros) demonstrou que o conjunto de restrições polinomiais que definem a Cairo VM está correto. Se você tem acompanhado as notícias recentemente, o bug recentemente descoberto por IA e agora corrigido no Zcash (outro projeto que co-fundi e do qual tenho muito orgulho e apoio) estava relacionado a uma restrição ausente. A decisão de verificar seu código para excluir outros bugs desse tipo é o passo correto. Executar esse tipo de verificação para o core VM do Cairo nos forneceu, à equipe StarkWare, certeza matemática de que não há restrição ausente em nossa Cairo VM. Portanto, além de provar o core VM do Cairo, também provamos o sistema S-two STARK, parte do compilador, e muitas das funções na biblioteca padrão do Cairo. O trabalho está concluído? Não. Há muitas outras coisas que podem ser provadas formalmente. Mas estamos comprometidos em continuar provando formalmente todas as propriedades centrais relacionadas à solidez e segurança dos nossos sistemas. É ótimo ver outros projetos adotando a verificação formal como uma ferramenta importante. Tenho orgulho de que a StarkWare tenha liderado o caminho nesse aspecto também. Esse é o significado de blockchain futurista para nós. Quer saber mais? Aqui está uma conta detalhada dos nossos esforços de prova com Lean nos últimos anos