Como @VitalikButerin diz, precisamos de verificação formal das propriedades de segurança.

Mas escalar a verificação formal para contratos inteligentes do Ethereum sempre foi um desafio devido à forma como a EVM lida com a memória - um grande array monolítico sem alocação explícita. Isso apresenta dificuldades para os solucionadores SMT, pois requer que os solucionadores inferem invariantes complexas sobre a memória.

Então, como a Certora superou isso? Vamos analisar 🧵👇