Un invariante es una propiedad que siempre debe cumplirse después de que un smart contract es desplegado y durante toda su ejecución. A primera vista, verificar un invariante puede parecer sencillo: asumir que el invariante se cumple antes de la llamada a una función, ejecutar la función y confirmar que se sigue cumpliendo después.
En la práctica, este proceso rara vez es tan simple. El Certora Prover opera en un mundo simbólico donde explora todos los estados posibles de un contrato, no solo aquellos que ocurrirían de manera realista en un sistema desplegado. Esta exploración exhaustiva y simbólica es fundamental en su diseño; es lo que le permite al Prover encontrar errores en escenarios que los desarrolladores podrían nunca considerar.
Sin embargo, no todos los estados simbólicos que explora el Prover son estados válidos o alcanzables dentro del contexto de la lógica de negocio del contrato. Sin orientación adicional, el Prover puede comenzar o razonar sobre estados “imposibles” o condiciones que nunca podrían surgir en una ejecución real en la blockchain. Cuando esto sucede, el Prover podría señalar una violación incluso si el contrato en sí es correcto, simplemente porque el análisis comenzó desde una suposición inválida.
Para prevenir este tipo de violaciones falsas, CVL proporciona el preserved block, un mecanismo que nos permite especificar suposiciones adicionales sobre el comportamiento realista del contrato. Estas suposiciones ayudan al Prover a centrarse en rutas de ejecución válidas y relevantes, descartando estados que son lógica o contextualmente imposibles.
En este capítulo, exploraremos el rol de los preserved blocks en la verificación formal. Discutiremos por qué son necesarios, cómo escribirlos en CVL y cómo ayudan a asegurar que los invariantes se verifiquen solo bajo condiciones realistas. También aplicaremos este concepto a un ejemplo práctico al verificar que, en el contrato WETH, el balance de ETH del contrato siempre iguale o supere el suministro total de sus tokens.
Para entender su rol más claramente, primero revisemos cómo el Prover verifica si una función preserva un invariante, y por qué este proceso a veces puede fallar.
Por qué los invariantes necesitan suposiciones adicionales
Como sabemos, al verificar invariantes, el Prover sigue un proceso de razonamiento estructurado similar a la inducción matemática:
- Comprobación del estado inicial (Caso base): El Prover primero verifica que el invariante se cumple inmediatamente después de que termina de ejecutarse el constructor del contrato. Esto establece el invariante como verdadero en el punto de partida.
- Suposición (Pre-estado): Para cada función pública y externa, el Prover asume que el invariante se cumple antes de que la función se ejecute.
- Ejecución simbólica y comprobación del post-estado: Luego, ejecuta simbólicamente la función a través de todos los inputs y flujos de control posibles, y verifica que el invariante se sigue cumpliendo después.
Si el invariante satisface todas estas comprobaciones, se considera preservado para todas las ejecuciones del contrato. Pero aquí radica la dificultad: el Prover no se restringe a rutas de ejecución realistas. También explora estados altamente improbables, e incluso imposibles.
Por ejemplo, mientras verifica el invariante ERC-20 “la suma de los balances de todas las cuentas siempre debe ser igual al suministro total del token,” el Prover puede explorar una ruta de ejecución donde el contrato termina llamando a sus propias funciones. En la práctica, esta situación nunca ocurre, ya que las funciones de ERC-20 como transfer están diseñadas para ser llamadas solo por usuarios externos u otros contratos. Sin embargo, debido a que el Prover explora sistemáticamente a todos los posibles llamadores, también considera trazas donde el contrato invoca sus propias funciones.
Tales autollamadas pueden producir escenarios absurdos donde los balances y el suministro total de tokens parecen inconsistentes, llevando al Prover a reportar una violación incluso cuando ninguna ejecución real podría desencadenarla. Estos son ejemplos clásicos de falsas violaciones: el invariante parece roto solo porque el Prover ha razonado sobre estados que no pueden ocurrir en la realidad.
Aquí es donde entran los preserved blocks. Los preserved blocks nos permiten introducir suposiciones adicionales durante la verificación de invariantes, guiando al Prover a ignorar estados imposibles o irrelevantes y centrarse únicamente en los realistas.
Ahora que entendemos por qué los preserved blocks son necesarios, pasemos a ver cómo se escriben en CVL.
¿Cómo definir un Preserved Block?
Un preserved block es una estructura especial en CVL que nos permite añadir suposiciones adicionales al probar un invariante. Piénsalo como si le dieras al Prover una pequeña “pista” sobre cómo se comporta el sistema en realidad, para que no pierda tiempo explorando escenarios imposibles.
Definimos un preserved block justo después de la expresión del invariante, usando la palabra clave preserved. La forma más simple se ve así:
invariant invariant_name()
invariant_expression
{
preserved {
// assumptions about the invariant
}
}
A veces, no queremos que un preserved block se aplique en todas partes — solo para una función en particular, o solo con ciertos detalles del entorno (como msg.sender o msg.value). En ese caso, podemos extender la sintaxis con la firma opcional de una función y una cláusula opcional with (para acceder al entorno de la transacción):
invariant invariant_name(param_1, param_2,...)
invariant_expression;
{
preserved functionName(type arg, ...) with (env e) {
// additional assumptions applicable only for this particular function
}
}
Tanto los preserved blocks genéricos como los específicos de funciones se aplican durante el paso de inducción de la comprobación del invariante. Se ejecutan después de que se asume que el invariante se cumple en el pre-estado, pero antes de que el método correspondiente se ejecute simbólicamente, asegurando que el Prover comience cada paso de inducción desde un estado que sea matemáticamente válido y contextualmente realista.
Hasta ahora, los preserved blocks determinan las suposiciones bajo las cuales se analiza cada función relevante. En algunos casos, sin embargo, también podríamos querer restringir contra qué funciones se verifica el invariante en primer lugar. CVL proporciona un filter block, escrito como filtered { … }, para este propósito. (Puedes leer más sobre filter block en este enlace )
invariant invariant_name()
invariant_expression;
filtered {
// restrict which functions are checked
}
{
preserved functionName(type arg, ...) with (env e) {
// assumptions or requireInvariant statements
}
}
Cuando hay un filter block presente, el invariante se verifica solo contra las funciones incluidas en el filtro, y cualquier preserved block se aplica dentro de ese conjunto restringido. Por esta razón, el preserved block se escribe después del filter block.
Un filter block restringe contra qué funciones se verifica el invariante. Luego, un preserved block genérico (preserved with (env e) { ... }) se aplica a cada función dentro de ese conjunto filtrado. Un preserved block específico de la función (preserved functionName(…) with (env e) { ... }) se aplica solo cuando el Prover está verificando dicha función nombrada. Si la función nombrada no está incluida en el filtro, ese preserved block no tiene efecto.
En resumen, los filtros reducen dónde se aplica un invariante, y los preserved blocks describen qué debe seguir cumpliéndose cuando esas funciones se ejecutan. Usados en conjunto, le dan al Prover un camino claro para verificar invariantes sin distraerse por estados irrelevantes o imposibles.
En la práctica, sin embargo, los preserved blocks son generalmente preferidos sobre los filter blocks cuando un invariante falla debido a una ejecución simbólica poco realista. Ambos mecanismos restringen el espacio de búsqueda del Prover y deben ser usados con cuidado para evitar debilitar una prueba, pero los filtros son más riesgosos porque eliminan funciones enteras de la comprobación del invariante.
Los preserved blocks son usualmente más seguros porque restringen las suposiciones sobre el estado o el entorno de ejecución en lugar de excluir comportamientos por completo. Como resultado, son más adecuados para descartar estados imposibles asegurando que el invariante se siga verificando contra toda la funcionalidad relevante del contrato.
Ahora que hemos cubierto la teoría y la sintaxis, veamos cómo funcionan los preserved blocks en la práctica aplicándolos a un contrato real: WETH de Solady.
Poniéndolo todo junto: Verificando un invariante de WETH
Para poner todo en contexto, verifiquemos un invariante del contrato WETH de Solady — una implementación de ERC-20 que representa Ether (ETH) en una proporción 1:1 con los tokens WETH. Una propiedad clave de este contrato es que su balance de ETH siempre debe ser mayor o igual al número total de tokens WETH en circulación.
Definiendo nuestro invariante de WETH
Para verificar este invariante, sigue los pasos a continuación:
- Dentro de tu directorio del proyecto Certora, crea un nuevo archivo llamado
ERC20.solen el subdirectoriocontracts, y copia este código de Solady en él. - Crea otro archivo llamado
WETH.solen el mismo subdirectoriocontracts, y copia este código en él. - En el subdirectorio
specs, crea un nuevo archivo llamadoweth.spec. - Dentro de
weth.spec, define el invariantetokenIntegrity()de la siguiente manera:
invariant tokenIntegrity()
nativeBalances[currentContract] >= totalSupply();
Nota: En CVL, nativeBalances es un mapping de los balances del token nativo — por ejemplo, ETH en Ethereum. El balance de una dirección a se puede expresar usando nativeBalances[a]. El identificador currentContract se refiere al contrato principal que se está verificando. Por lo tanto, nativeBalances[currentContract] representa el balance de token nativo del contrato que se está verificando.
- Añade un methods block que incluya la firma de la función de
totalSupply():
methods {
function totalSupply() external returns (uint256) envfree;
}
invariant tokenIntegrity()
nativeBalances[currentContract] >= totalSupply();
- En el subdirectorio
confs, crea un archivo de configuración llamadoweth.conf:
{
"files": [
"contracts/WETH.sol:WETH"
],
"verify": "WETH:specs/weth.spec",
"optimistic_loop" : true,
"msg": "Check WETH contract integrity"
}
Ejecutando la verificación
Una vez que hayas ejecutado todos los pasos anteriores, ejecuta el comando certoraRun confs/weth.conf para verificar nuestra especificación y ver un resultado similar a la imagen a continuación:
El resultado anterior de nuestra ejecución de verificación muestra que el invariante tokenIntegrity falló porque el Prover encontró un escenario donde el balance de ETH del contrato podría ser menor que el suministro total reportado.
Entendiendo la violación
Nuestro informe de análisis detallado encuentra que nuestro invariante tokenIntegrity ha pasado la “Base de inducción: Después del constructor” ✅, lo que significa que la propiedad se cumple inmediatamente después del despliegue. Sin embargo, falló durante el “Paso de inducción: después de la ejecución de un método externo (non-view/pure)” ❌, lo que indica que, aunque el invariante comienza siendo válido, no se cumple consistentemente después de ciertas llamadas a funciones que modifican el estado.
Para entender la causa de la violación, necesitamos analizar las trazas de llamadas de las funciones que fallan.
Empecemos con la función deposit().
Entendiendo la violación en la llamada deposit()
Nuestro análisis de la traza de la llamada de la función deposit() revela algo inusual: tanto el remitente como el receptor son el propio contrato (WETH).
Este escenario — donde el contrato llama a su propia función deposit() — es un caso absurdo desde un punto de vista práctico, ya que el contrato WETH no contiene ninguna ruta de código que pueda llamar a deposit() directa o indirectamente. Aunque el Prover identifica esto correctamente como una interacción teóricamente posible, podemos decirle explícitamente que ignore dichos casos a través del bloque preserved.
Entendiendo la violación de la llamada receive()
La función receive() en un contrato Solidity es una función especial que se ejecuta automáticamente cuando el contrato recibe Ether con la calldata vacía. Un contrato puede definir solo una función de este tipo, y debe tener el siguiente formato:
receive() external payable { ... }
La función receive() no puede recibir argumentos, no puede devolver valores y se activa en transferencias de ETH simples (como a través de .send, .transfer, o una transferencia en bruto de ETH).
En la implementación de WETH, la función receive() simplemente reenvía las llamadas a la función deposit():
// @dev Equivalent to `deposit()`.
receive() external payable virtual {
deposit();
}
Debido a esto, cualquier ruta de ejecución poco realista que rompa deposit() también puede romper receive(). El Prover trata receive() como un punto de entrada externo más, por lo que puede asumir simbólicamente que el contrato llama a su propia función receive().
Esto es exactamente lo que ocurrió en la traza que falla: al igual que con deposit(), el Prover escogió una ruta donde tanto el remitente como el receptor son el propio contrato (WETH), lo que lleva a un escenario imposible de autollamada que no ocurre en una ejecución real, pero que hace que el invariante falle simbólicamente.
Entendiendo la violación de la llamada a withdraw()
La traza de la llamada para withdraw() revela un problema causado por el Prover al probar un escenario tremendamente irreal. Para entender por qué falla, analicemos la traza de la llamada paso a paso, usando los valores exactos que usó el Prover.
La comprobación del pre-estado (Estado Global #1)
Durante la comprobación del pre-estado, el Prover asume que el invariante se cumple antes de que la función se ejecute. En este punto — capturado como Estado Global #1 — establece un entorno simbólico que representa las posibles condiciones iniciales antes de la ejecución simbólica de la función withdraw().
En este estado, el balance de ETH del contrato se establece en 2^256 − 3, mientras que el suministro total del token es solo 2.
Esto significa que el contrato comienza en un estado imposible — contiene una gran cantidad de ETH pero tiene un suministro total de token de solo 2. Ningún despliegue en el mundo real podría alcanzar tal condición, pero como no restringimos el estado inicial, el Prover fue libre de elegir valores arbitrarios.
En este punto, nuestro invariante se cumple porque:
2^256 − 3 ≥ 2 ✅
Ejecución simbólica de withdraw() (Estado Global #2)
A continuación, el Prover ejecuta simbólicamente la función withdraw():
Aquí, el que hace la llamada (0x8200) intenta retirar 2^256 − 6. La función withdraw() llama a la función interna _burn(from, amount). En una ejecución real, _burn() se revertiría inmediatamente si amount > balanceOf(from).
Sin embargo, el Prover razona simbólicamente. Cuando llega a la comprobación if (amount > balanceOf(from)), trata a balanceOf(0x8200) como una variable simbólica no acotada. Para explorar un camino en el que no se revierta la ejecución, debe asumir un valor para este balance que sea lo suficientemente grande como para pasar la comprobación.
Podemos encontrar este valor asumido observando las operaciones _burn debajo de Estado Global #3. La traza muestra un patrón clásico de “leer-modificar-escribir” en un único slot de almacenamiento (el balance del llamador):
Esto es lo que esto nos dice:
- El Prover carga el balance del que llama. Para continuar, asume que el balance es
2^256 - 2. - Luego almacena el nuevo balance (
0x4) después de la resta.
Podemos confirmar esto con matemáticas simples:
Precall Balance of 0x8200 = 2^256
Withdrawal Amount = 2^256 - 6
Postcall Balance of 0x8200 should be = (2^256 - 2) - (2^256 - 6) = 4
El resultado calculado 4 coincide perfectamente con el valor de Store 0x4.
El Underflow aritmético (Estado Global #3)
Una vez que _burn() actualiza el balance de WETH del que llama, actualiza el suministro total de WETH.
En este punto, totalSupply cambia de 2 a 8 porque 2 − (2^256 − 6) produce un underflow en uint256 y envuelve en módulo 2^256.
Nota: En las versiones de Solidity ≥0.8.0, la aritmética normal como totalSupply -= amount revertiría en caso de underflow. Sin embargo, esto no ocurre cuando el contrato utiliza un bloque unchecked o realiza la operación en inline assembly, ya que ambos siguen las semánticas aritméticas de bajo nivel donde los valores envuelven en módulo 2^256.
La transferencia de ETH no resuelta y AUTO-Havoc (Estado Global #5)
Después de que _burn() se completa, withdraw() intenta transferir el ETH al que hizo la llamada usando un call de bajo nivel:
call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)
Antes de la llamada a withdraw(), el contrato WETH contenía 2^256 − 3 wei. Una llamada exitosa a withdraw() resultará en la transferencia de 2^256 − 6 wei al que llama y debería disminuir el balance de ETH del contrato de 2^256 − 3 a 3.
Si miramos la traza para el Estado Global #5, vemos que el Prover realiza este cálculo correctamente al principio:
Sin embargo, el Prover no se detiene ahí. La llamada se hace a una dirección externa y desconocida (el caller()). El Prover no puede determinar el comportamiento de este destinatario (es decir, la función fallback del que llama).
Cuando el Prover se enfrenta a estas llamadas externas no resueltas, aplica automáticamente un resumen de AUTO-havoc.
Bajo AUTO-havoc, el Prover asume que la llamada externa es exitosa pero puede modificar arbitrariamente las variables de estado relacionadas con la llamada. Hace esto porque carece de un modelo concreto del código del destinatario.
En la traza de la llamada, vemos que esto ocurre inmediatamente después del cálculo correcto:
Este havoc sobrescribe el balance calculado. En el siguiente estado (Estado Global #6), el balance del contrato es:
Esto significa que el Prover ignoró el resultado calculado (3) y asignó un valor arbitrario (5) como parte del resumen del havoc. Este valor con havoc es el que se utilizará en la comprobación del post-estado.
El Post-Estado y el fallo del invariante (Estado Global #7)
Después de que la función withdraw se completa, el Prover verifica el invariante en el post-estado:
nativeBalances[currentContract] >= totalSupply()
En este punto, los valores simbólicos son:
WETH.balance = 0x5(Establecido por AUTO-havoc)WETH.totalSupply() = 0x8(Corrompido por el underflow)
Así que el invariante se evalúa a:
5 >= 8 ❌ (false)
El Prover concluye que el invariante fue violado.
La causa raíz
Esta violación es un clásico falso positivo. No ocurrió debido a una falla lógica en la implementación de withdraw() del contrato WETH. En su lugar, resultó del razonamiento simbólico sub-restringido del Prover:
- Toda la ruta de ejecución solo fue posible porque el Prover asumió un pre-estado imposible donde
balanceOf(msg.sender)era (2^256 - 2) drásticamente mayor quetotalSupply(2). - Esta suposición poco realista, permitida por una variable simbólica no restringida, provocó directamente un underflow aritmético en la variable
totalSupply, corrompiéndola de 2 a 8.
El paso auto-havoc también contribuyó a los valores finales, pero el estado ya estaba irremediablemente afectado por el underflow.
Arreglando falsas violaciones usando Preserved Blocks
Ahora que está claro que el Prover señaló violaciones no por una falla en el contrato WETH, sino porque exploró estados simbólicos que nunca pueden ocurrir en una ejecución real, nuestro próximo paso es guiar de nuevo al Prover hacia un comportamiento realista.
Hacemos esto añadiendo preserved blocks, los cuales introducen suposiciones adicionales entre la comprobación del pre-estado y la ejecución simbólica. Estas suposiciones previenen que el Prover entre en rutas de ejecución imposibles, como autoinvocaciones del contrato o balances de tokens absurdos.
Arreglando la violación en deposit() y receive()
Ambas violaciones fueron causadas por el Prover al asumir autollamadas, donde el contrato WETH fue modelado como su propio llamador. Esto es imposible en la ejecución real pero válido en la ejecución simbólica a menos que se restrinja.
Arreglamos esto añadiendo un preserved block que descarta cualquier escenario donde el contrato llama a sus propias funciones:
methods {
function totalSupply() external returns (uint256) envfree;
}
invariant tokenIntegrity()
nativeBalances[currentContract] >= totalSupply()
{
preserved with(env e) {
require e.msg.sender != currentContract;
}
}
Esta única suposición elimina todas las trazas de autollamadas, eliminando inmediatamente los falsos positivos en tanto en deposit() como en receive() (reportado como receiveOrFallback() en la interfaz del Prover).
Con el problema de las autollamadas resuelto para deposit() y receive(), ahora podemos pasar a la segunda fuente de falsas violaciones: las suposiciones simbólicas poco realistas dentro de withdraw().
Arreglando la violación de withdraw()
El fallo en withdraw() fue causado por algo distinto: el Prover asumió que balanceOf(msg.sender) podía ser arbitrariamente grande, incluso mayor que el suministro total. Esto forzó a _burn() a ejecutarse por un camino que debería revertirse, desencadenando un underflow y corrompiendo totalSupply.
Para prevenir esto, añadimos un preserved block específicamente para withdraw():
methods {
function totalSupply() external returns (uint256) envfree;
//we also added the signature of balanceOf()
function balanceOf(address) external returns(uint256) envfree;
}
invariant tokenIntegrity()
nativeBalances[currentContract] >= totalSupply()
{
// Generic Block
preserved with (env e) {
require e.msg.sender != currentContract;
}
// Function-Specific Block
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}
En la especificación actualizada de arriba, la línea require balanceOf(e.msg.sender) <= totalSupply(); instruye al Prover a ignorar cualquier ruta de ejecución donde el balance de tokens de un usuario excede el suministro total.
Juntos, estos preserved blocks eliminan cada ruta de ejecución poco realista que previamente causaba una falsa violación. Con estas restricciones en su lugar, ahora podemos volver a ejecutar el Prover para comprobar si el invariante se cumple bajo suposiciones realistas.
Volviendo a ejecutar la verificación
Después de aplicar ambas soluciones, ejecuta el Prover de nuevo y abre el enlace de resultados de verificación para ver una salida similar a la imagen que se muestra a continuación.
Esta vez, el Prover confirma que el invariante tokenIntegrity se cumple en todas las fases de verificación, pasando tanto la base de inducción como el paso de inducción.
El informe muestra que todas las funciones relevantes — incluyendo deposit(), withdraw(), transfer() y approve() — ahora preservan el invariante.
En este punto, el invariante se verifica exitosamente y la especificación es correcta. Sin embargo, podemos simplificarla aún más. Ambas suposiciones que añadimos anteriormente comparten la misma estructura y no dependen de ningún argumento de función, lo que significa que podemos consolidarlas en un solo preserved block más limpio.
Una especificación más limpia y unificada
En nuestro caso, ambas suposiciones que añadimos anteriormente comparten una propiedad importante:
“Dependen únicamente del entorno de la transacción (env) y del estado global del contrato. No dependen de los parámetros de ninguna función en particular.”
Esto significa que son verdades globales sobre el contrato:
- El contrato nunca se llama a sí mismo.
- El balance de un usuario nunca excede el suministro total.
Ya que ninguna condición depende de los argumentos de una función, ambas pueden ser colocadas de manera segura dentro de un único preserved block genérico, como se muestra a continuación:
methods {
function totalSupply() external returns (uint256) envfree;
function balanceOf(address) external returns (uint256) envfree;
}
invariant tokenIntegrity()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
require balanceOf(e.msg.sender) <= totalSupply();
}
}
Cuando ejecutamos el Prover usando este bloque combinado, la especificación es aceptada sin errores y el invariante se cumple en todas las fases de verificación, como se muestra en la imagen a continuación:
Constructor Preserved Blocks (Suposiciones del paso base)
Hasta ahora, hemos discutido los preserved blocks como una forma de restringir al Prover durante el paso de inducción en la verificación del invariante — es decir, al verificar que las funciones públicas y externas preservan un invariante asumiendo que ya se cumplía de antemano.
A partir de la versión 8.5.1 del Prover, CVL también soporta constructor preserved blocks, los cuales se aplican al paso base de la verificación del invariante.
Durante el paso base, el Prover ejecuta simbólicamente el constructor para verificar que el invariante se cumple inmediatamente después del despliegue. El almacenamiento del contrato principal (currentContract) es inicializado en cero, pero en escenarios con múltiples contratos, los demás contratos en la escena de verificación inician en estados simbólicos arbitrarios.
Este es un cambio respecto a versiones anteriores del Prover, donde se asumía que el almacenamiento de todos los contratos estaba en cero — correspondiendo al despliegue fresco de todo el sistema a la vez. El comportamiento actual permite un modelado más realista de sistemas desplegados, pero también significa que la verificación del paso base podría comenzar desde estados que nunca surgirían en un despliegue real.
Cuando un invariante depende de relaciones con estos contratos externos, el entorno simbólico puede violar suposiciones que se cumplirían en la práctica, causando que el paso base falle por razones puramente simbólicas. Los constructor preserved blocks nos permiten reintroducir estas suposiciones explícitamente, asegurando que el paso base refleje un contexto de despliegue realista.
La sintaxis refleja la de otros preserved blocks pero con un alcance específico para el constructor:
preserved constructor() with (env e) {
require e.block.timestamp != 0;
}
Este bloque se aplica solo al paso base y no tiene efecto en el paso de inducción o en la verificación individual de funciones.
En este capítulo, las falsas violaciones en el caso de estudio de WETH surgen durante el paso de inducción, por lo que se resuelven utilizando preserved blocks genéricos y a nivel de función. Los constructor preserved blocks son más útiles cuando un invariante falla inmediatamente después del despliegue debido a suposiciones poco realistas sobre el entorno simbólico inicial.
Conclusión
Los preserved blocks son una herramienta poderosa para refinar la verificación de invariantes en CVL. Al restringir al Prover a suposiciones realistas — tanto durante la ejecución de las funciones como, cuando es necesario, durante el despliegue — eliminan los falsos positivos a la vez que preservan la solidez de la prueba.
A través del caso de estudio de WETH, vimos cómo los preserved blocks elegidos cuidadosamente pueden alejar al Prover de estados simbólicos imposibles y guiarlo hacia ejecuciones significativas, asegurando que los invariantes se verifiquen bajo condiciones que reflejan con precisión el comportamiento del mundo real.
Este artículo es parte de una serie sobre verificación formal usando el Certora Prover