Restringir variables fantasma en invariantes En el capítulo anterior, vimos cómo las variables fantasma sin restricciones pueden generar falsos positivos. También aprendimos cómo se puede usar una sentencia para restringir eficazmente...

Reglas de SafeMint y SafeTransfer en ERC-721 Introducción Este capítulo es la cuarta parte (4/5) de nuestro recorrido por el código de la especificación CVL de ERC-721 de OpenZeppelin y se centra en verificar formalmente...

Entendiendo el Spec File en Certora CVL En el último capítulo, vimos que para realizar la verificación formal utilizando Certora Prover, necesitamos proporcionar al Prover los siguientes elementos clave: Smart...

Introducción a las propiedades de los métodos Introducción En el capítulo anterior, aprendimos sobre las reglas paramétricas, las cuales nos permiten verificar formalmente propiedades que se espera que se cumplan independientemente de qué...

Introducción a las Reglas Paramétricas Hasta ahora, en capítulos anteriores, hemos escrito reglas para verificar el comportamiento de métodos específicos y su impacto en el estado de un contrato. Por ejemplo: En el Capítulo 2,...

Pruebas de msg.sender y msg.value en CVL Introducción En este capítulo, introducimos la variable en CVL, la cual nos permite crear reglas para funciones que dependen de , , y otras variables globales en...

Verificando formalmente un Counter En el capítulo anterior, aprendimos la parte teórica de la verificación formal, incluyendo qué es y cómo funciona. En este módulo, iremos más allá de la teoría y aprenderemos...

Certora Require, Assert y Satisfy En el capítulo anterior, aprendimos que una especificación es un fragmento de código escrito en CVL que describe el comportamiento esperado de un contrato inteligente. Un...

Introducción a la Verificación Formal La verificación formal es el proceso de demostrar matemáticamente que un programa cumple con una especificación. Este artículo presenta conceptualmente cómo la verificación formal...

Verificando formalmente Initializable.sol Este artículo describe cómo Certora verificó formalmente el contrato Initializable.sol de OpenZeppelin. Asumimos que el lector ya está familiarizado con el funcionamiento de este contrato...

Verificación formal del saldo de direcciones En el capítulo anterior, cubrimos cómo razonar sobre las funciones dependientes del entorno en CVL centrándonos en contextos non-payable. En esos ejemplos, el acceso...

Pruebas de la llamada revert en Certora En este capítulo, aprenderemos cómo usar las etiquetas de métodos ( y ) y la variable especial en CVL para verificar los reverts esperados en la ejecución de contratos inteligentes. Configuración...