những điểm nổi bật của phiên bản halmos v0.3.0! (lời nhắc nhanh: halmos là một công cụ kiểm tra biểu tượng cho mã bytecode EVM, tương tác tốt với các dự án foundry và hỗ trợ nhiều bộ giải SMT) 1. chúng tôi (cuối cùng) đã thêm hỗ trợ cho việc kiểm tra bất biến có trạng thái

2. báo cáo độ bao phủ (chỉ cần chạy với --coverage), sau đó hoặc là genhtml kết quả hoặc trực quan hóa nó trong VSCode

3. flamegraphs Có vẻ hơi kỳ lạ, nhưng là một cách thú vị để hình dung một chiến dịch kiểm tra bất biến. Chỉ cần chạy với --flamegraph

5. hỗ trợ giải pháp tốt hơn trước: --solver-command "yices-smt2 --smt2-model-format" sau: --solver yices trước: --solver-command "bitwuzla --produce-models --abstraction" sau: --solver bitwuzla-abs

6. tình bạn đã kết thúc với z3, yices giờ là trình giải mặc định (nên bạn thậm chí không cần phải nói `--solver yices` để tận hưởng những lợi ích)

7. hỗ trợ solx nếu bạn không biết solx là gì, @PatrickAlphaC sẽ giúp bạn

8. đã thêm env* và random* cheatcodes, tất cả 3 triệu cái. Cảm ơn @Jayakumar2812 vì sự đóng góp!

9. các chỉ báo tiến trình tuyệt vời từ tương lai

Đó là tất cả! Nhận ngay bây giờ: uv tool install --python 3.13 halmos