Halmos v0.3.0: Detección Mejorada de Errores y Optimización de Rendimiento

Joerg Hiller
15 de julio de 2025 05:59

Halmos v0.3.0 introduce pruebas de invariantes con estado, mejoras de rendimiento y soporte ampliado para solucionadores, avanzando significativamente en la detección de errores en contratos inteligentes de EVM.

Halmos, una herramienta de prueba simbólica diseñada para contratos inteligentes de EVM, ha lanzado su versión más reciente, v0.3.0, que se centra en la detección práctica de errores y mejoras de rendimiento. Esta actualización marca un avance significativo en las capacidades de la herramienta, mejorando su eficacia más allá de la verificación formal, según a16z crypto.

Pruebas de Invariantes con Estado

La adición más notable en esta versión es el soporte para pruebas de invariantes con estado, una característica muy solicitada. Esto permite a Halmos identificar automáticamente contratos y funciones objetivo, explorar estados posibles y afirmar invariantes, identificando así posibles fallos de manera eficiente. Los usuarios pueden iniciar estas pruebas prefijando los tests con invariant_, lo que permite a la herramienta explorar varias secuencias de estados hasta una profundidad especificada.

Informes de Cobertura y Herramientas de Visualización

Halmos v0.3.0 también ofrece la capacidad de generar información de cobertura en formato lcov, que puede visualizarse con herramientas como la extensión Coverage Gutters de VSCode. Además, la inclusión de soporte para flamegraph permite a los usuarios visualizar secuencias de llamadas durante las pruebas de invariantes, proporcionando una visión clara de las rutas exploradas por la herramienta.

Mejoras de Rendimiento y Solucionadores

Se han realizado mejoras significativas en el rendimiento del bucle del intérprete EVM, logrando una ejecución hasta 32 veces más rápida. La herramienta ahora admite una gama más amplia de solucionadores SMT, simplificando su integración al configurarlos automáticamente para un uso óptimo. Yices se ha introducido como el solucionador predeterminado debido a su velocidad superior en comparación con opciones anteriores.

Características Adicionales

Halmos v0.3.0 introduce soporte para solx, un compilador experimental de Solidity, y amplía su funcionalidad con nuevos cheatcodes para la manipulación de variables de entorno. También se han añadido indicadores de progreso, proporcionando retroalimentación en tiempo real sobre las operaciones de la herramienta durante sesiones largas.

Estas mejoras consolidan la posición de Halmos como una herramienta robusta para pruebas de contratos inteligentes, ofreciendo a los desarrolladores capacidades mejoradas para garantizar la fiabilidad y seguridad de los contratos.

• halmos
• evm
• contratos inteligentes

Traducido por CryptoHawk9