Como dice @VitalikButerin, necesitamos una verificación formal de las propiedades de seguridad.

Pero escalar la verificación formal para los contratos inteligentes de Ethereum siempre ha sido un desafío debido a cómo el EVM maneja la memoria: un gran array monolítico sin una asignación explícita. Esto plantea dificultades para los solucionadores SMT porque requiere que los solucionadores infieran invariantes complejos sobre la memoria.

Entonces, ¿cómo superó Certora esto? Desglosemoslo 🧵👇