Uri KirsteinProver version 7.3.0 is out! This update aims to enhance your user experience and address some minor bugs reported by our users.
New Web Features
Jump to Spec
Quickly locate rule definitions or assertion messages within your spec file by clicking the new icon in the Rules, Rule Call Resolution, or Global Call Resolution tab items
Real-time insights
Stay informed with the new Live Statistics tab, providing key metrics on path count, non-linear operations, and memory/storage complexity before job completion. These metrics guide simplification strategies to optimize Prover performance.
Job configurations tab
Explore the new Configuration tab to quickly access the exact settings used for your verification job
Prover Updates
- Easy access to immutables
Access immutable variables directly, even if they are private. Read more | Example - Advanced rule selection
Enhance filtering flexibility with wildcard (*) support in --rule or utilize
--exclude_rule for seamless exclusion. Read more - Reason about blobhash
Verify advanced specifications with Prover's new support for blobhash instruction and hooks. Read more - Preliminary support of transient storage
Preliminary support for tload and tstore operations in inline-assembly Solidity, along with ALL_TLOAD and ALL_TSTORE hooks. Read more | Example - Dispatch-list summarization
Enhance contract behavior modeling with dispatch-list summarization, enabling precise representation of smart contract actions for statically unresolved calls. Read more | Example - Precise bitwise operations
Fine-tune modeling by using --precise_bitwise_ops to model bitwise operations precisely with the tradeoff of lowering mathint accuracy. Read more | Example - Local compilation checks
Speed up development with --compilation_steps_only, enabling local compilation and syntax validation of spec files without server connection. Read more
Access these updates by ensuring your software is up-to-date with the latest version. To upgrade to v7.3.0, simply run pip install --upgrade certora-cli.
