Vitalik publica artigo sobre verificação formal, destacando o seu papel na segurança e eficiência da Ethereum

Segundo a ChainCatcher, Vitalik publicou hoje um artigo intitulado «A shallow dive into formal verification», no qual aborda como a verificação formal pode melhorar tanto a segurança como a eficiência no desenvolvimento do Ethereum. Os programadores podem usar Lean, bytecode EVM ou linguagem assembly para escrever código e verificar a sua correcção através de provas matemáticas verificáveis automaticamente. Vitalik referiu que a verificação formal é particularmente adequada para sistemas complexos como STARKs, consenso com tolerância a falhas bizantinas, ZK-EVM e assinaturas pós-quânticas, embora tenha limitações, incluindo erros de especificação, cobertura incompleta do código e ataques a nível de hardware.