Halmos v0.3.0: Enhanced Bug Detection and Performance Improvements

Halmos, a symbolic testing tool designed for EVM smart contracts, has launched its latest version, v0.3.0, which focuses on practical bug detection and performance improvements. This update marks a significant advancement in the tool's capabilities, enhancing its effectiveness beyond formal verification, according to a16z crypto.

Stateful Invariant Testing

The most notable addition in this release is the support for stateful invariant testing, a highly requested feature. This allows Halmos to automatically identify target contracts and functions, explore possible states, and assert invariants, thereby identifying potential failures efficiently. Users can initiate this testing by prefixing tests with invariant_, enabling the tool to explore various state sequences up to a specified depth.

Coverage Reports and Visualization Tools

Halmos v0.3.0 also offers the ability to output coverage information in the lcov format, which can be visualized using tools like VSCode's Coverage Gutters extension. Furthermore, the inclusion of flamegraph support allows users to visualize sequences of calls during invariant testing, providing a clear view of the paths explored by the tool.

Performance and Solver Enhancements

Significant performance improvements have been made to the EVM interpreter loop, achieving up to 32x faster execution. The tool now supports a wider array of SMT solvers, simplifying their integration by automatically configuring them for optimal use. Yices has been introduced as the default solver due to its superior speed compared to previous options.

Additional Features

Halmos v0.3.0 introduces support for solx, an experimental Solidity compiler, and extends its functionality with new cheatcodes for environment variable manipulation. Progress indicators have also been added, providing real-time feedback on the tool's operations during long sessions.

These enhancements solidify Halmos's position as a robust tool for smart contract testing, offering developers improved capabilities for ensuring contract reliability and security.