Solana nativo: Entrada y ejecución de programas A lo largo de esta serie, hemos utilizado el framework Anchor para construir programas de Solana. Este tutorial te enseña cómo escribirlos en Rust nativo sin...

Los programas on-chain de Switchboard no pueden acceder directamente a los datos off-chain. Dependen de oráculos para incorporar información como precios de activos, resultados de eventos o respuestas de API. Sin estos oráculos,...

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

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

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

Verificando un Invariante Usando Ghost y Hook En cualquier implementación correcta de ERC20, la suma de todos los balances de las cuentas debe ser siempre igual al suministro total de tokens. Esta propiedad siempre debería mantenerse verdadera...

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

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

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

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

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

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