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

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

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

Introducción al Operador de Implicación El operador de implicación se utiliza frecuentemente como sustituto de la sentencia ya que es más limpio. Considere el siguiente ejemplo: una función que toma dos unsigned...

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

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

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

Sentencias condicionales en CVL y verificación formal de partes de Solady y Solmate Introducción Algunos comportamientos (propiedades) de los contratos son inherentemente condicionales, y el uso de construcciones como if/else en CVL...

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

Constructores en Cairo Un constructor es una función de llamada única ejecutada durante el despliegue del contrato para inicializar variables de estado, realizar tareas de configuración del contrato, hacer interacciones entre contratos y...