Overflow y Mathint En CVL, el tipo representa enteros no acotados, a diferencia de los tipos de tamaño fijo de Solidity como . Realiza operaciones aritméticas sin overflow ni underflow, lo que permite razonar basándose en...

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...

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...

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...

Introducción al operador bicondicional El operador bicondicional nos permite establecer relaciones de si y solo si entre valores booleanos. La implicación () establece que si se satisface la condición P, entonces Q...

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...

Verificando formalmente Ownable.sol Ownable es un contrato abstracto que proporciona control de acceso basado en el propietario. Al ser heredado, restringe funciones específicas al propietario mediante el modificador. Tiene tres...

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...

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...

Verificación formal de Nonces.Sol en OpenZeppelin. Los nonces, que significan "número usado una vez", se utilizan en esquemas de firmas digitales para prevenir ataques de repetición. Para los propósitos de este artículo, asumimos...

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...