Introducción a los Fantasmas Persistentes En capítulos anteriores, usamos variables fantasma (a través de hooks) para registrar valores de almacenamiento y cantidades que no se rastreaban explícitamente en los contratos inteligentes — por ejemplo, el...

Invariantes para ERC-721 Introducción En capítulos anteriores, exploramos cómo funcionan los invariantes de CVL: propiedades que deben cumplirse a lo largo de toda la ejecución del contrato. Los invariantes pueden funcionar como precondiciones en...

Restringiendo los valores fantasma en las reglas En el capítulo anterior, aprendimos cómo las variables fantasma permiten que la información fluya desde los hooks hacia las reglas. También aprendimos que: Al inicio de la verificación...

Reglas parcialmente paramétricas para ERC-721 Introducción Este capítulo es la parte final (5/5) del recorrido por el código de la especificación CVL de ERC-721 de OpenZeppelin, la cual verifica formalmente lo siguiente...

Reglas de transferencia y aprobación para ERC-721 Introducción Este capítulo continúa como la tercera parte (3/5) de nuestro recorrido por el código de la especificación CVL de ERC-721 de OpenZeppelin y se centra en la transferencia de tokens...

Preserved Block y su rol en la verificación de invariantes Un invariante es una propiedad que siempre debe cumplirse después de que se despliega un smart contract y a lo largo de toda su ejecución. A primera vista,...

Uso de “requireInvariant" en reglas e invariantes Hasta ahora, hemos escrito una regla para verificar comportamientos específicos o un invariante para verificar propiedades que siempre deben cumplirse a lo largo del...

Reglas de Mint y Burn para ERC-721 Introducción ERC-721 es el estándar de Ethereum para tokens no fungibles, ampliamente utilizado para representar la propiedad digital. Como cualquier forma de propiedad, gira en torno a la oferta...

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

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