Syscalls in Starknet In Solidity, low-level operations like reading/writing to storage, contract to contract calls, or sending messages are performed directly through inline assembly using Yul...

Solana nativo: Comprobaciones de seguridad esenciales En nuestros tutoriales anteriores sobre Solana nativo, omitimos las comprobaciones de seguridad para mantener los ejemplos breves y centrados en los temas principales. En este tutorial, cubriremos...

Introducción a los Storage Hooks y Ghosts A menudo resulta necesario inspeccionar los cambios en ubicaciones de almacenamiento específicas para demostrar que una propiedad o invariante se cumple, especialmente cuando el almacenamiento no...

Uso de Sload Hooks con Storage Mappings Introducción En el capítulo anterior, demostramos que los hooks son necesarios para verificar propiedades que involucran cambios en los valores de los mappings. El hook monitorea...

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

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

Introducción a los Invariantes en Certora Hasta ahora, nos hemos enfocado en verificar el comportamiento de métodos individuales o secuencias de métodos — asegurando que una llamada de función específica o un conjunto de llamadas,...

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

Verificar formalmente WETH de Solady Introducción ETH, ampliamente utilizado en DeFi para swaps, provisión de liquidez, staking y colateral, necesita una versión compatible con ERC-20 para que los protocolos puedan interactuar con él a través de...

Bucles en CVL: explosión de caminos y desenrollado de bucles Los bucles son una de las construcciones de programación más comunes, pero sigue siendo difícil razonar sobre ellos en la verificación formal. Mientras que un bucle en Solidity...

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