¡Aspectos destacados de la versión 0.3.0 de Halmos! (recordatorio rápido: halmos es una herramienta de prueba simbólica para el código de bytes EVM que interactúa muy bien con los proyectos de fundición y admite múltiples solucionadores SMT) 1. (Finalmente) agregamos soporte para pruebas invariantes con estado

2. informes de cobertura (simplemente ejecute con --coverage), luego genhtml el resultado o visualícelo en VSCode

3. Gráficos de llama Un poco extraño, pero una forma interesante de visualizar una campaña de pruebas invariantes. Simplemente ejecute con --flamegraph

5. Mejor soporte para solucionadores before: --solver-command "yices-smt2 --smt2-model-format" Después: --solver yices before: --solver-command "bitwuzla --produce-models --abstraction" Después: --solver bitwuzla-abs

6. La amistad terminó con z3, yices es el solucionador predeterminado ahora (por lo tanto, ni siquiera necesita decir '--solver yices' para disfrutar de los beneficios)

7. Soporte de Solx Si no sabe qué es Solx, @PatrickAlphaC tiene todo lo que necesita.

8. Se agregaron códigos de trucos ENV* y aleatorios*, los 3 millones. ¡Gracias @Jayakumar2812 por la contribución!

9. Indicadores de progreso fríos del futuro

¡Eso es todo! Consíguelo ahora: Instalación de la herramienta UV --Python 3.13 halmos