¡Destacados de la versión halmos v0.3.0! (recordatorio rápido: halmos es una herramienta de prueba simbólica para bytecode EVM que se integra bien con proyectos de foundry y admite múltiples solucionadores SMT) 1. (finalmente) añadimos soporte para pruebas de invariantes con estado.

2. informes de cobertura (simplemente ejecuta con --coverage), luego genera el HTML del resultado o visualízalo en VSCode

3. gráficos de llamas es un poco raro, pero es una forma interesante de visualizar una campaña de pruebas invariantes. Simplemente ejecuta con --flamegraph

5. mejor soporte para solucionadores antes: --solver-command "yices-smt2 --smt2-model-format" despues: --solver yices antes: --solver-command "bitwuzla --produce-models --abstraction" despues: --solver bitwuzla-abs

6. la amistad terminó con z3, yices es el solucionador predeterminado ahora (así que ni siquiera necesitas decir `--solver yices` para disfrutar de los beneficios)

7. soporte de solx si no sabes qué es solx, @PatrickAlphaC te lo explica

8. se añadieron los trucos env* y random*, los 3 millones de ellos. ¡Gracias @Jayakumar2812 por la contribución!

9. indicadores de progreso geniales del futuro

¡Eso es! Consíguelo ahora: uv tool install --python 3.13 halmos